A commonsense reasoner

Gk is a commonsense reasoner for logic enhanced with default rules and confidences. It is in active development. Gk is built on top of a confidence-handling reasoner confer (paper), which is built on top of a high-performance classical logic reasoner gkc (paper).

  • Download gk_07.gz : statically linked linux executable of gk version 0.7. No dependencies.
  • Read the gk tutorial.

Knowledge graphs

The following knowledge graphs are built from Conceptnet, WebChild, Aristo TupleKB, Quasimodo, Ascent++, UnCommonSense, ATOMIC 2020 and ATOMIC 10x. The graphs use the json-ld-logic syntax (paper) and can be handled by the gk system.

  • Original triple knowledge graphs converted to logic by mapping each relation to a predicate. Contains mostly taxonomy and inferences from taxonomy; ATOMIC parts also contain rules about events in Neo-Davidsonian encoding. Total 18M+ rules.

Datasets built from the hypernym and hyponym relations of Wordnet:


Examples for default logic:

Examples using Quasimodo and ConceptNet:

The following have been run on the full knowledge base (ca 2 million rules/facts) by first reading the knowledge into shared memory (10GB allocated) along with the Wordnet taxonomy datasets ./gk -seconds 120 -mbsize 10000 -readkb quasi/full.js conceptnet/full.js defkb/rules3.js defkb/similarity.js -defaults and then running gk on this memory base along wit the question for one second ./gk -usekb problemfile -seconds 1 The search outlines are produced by adding the -print 12 key. Examples for confidences without default logic:

Examples for interesting default rule aspects

Finding suitable methods and encoding of priorities for default rules is non-obvious. Consider the following commonsense observation: birds and airplanes without wings cannot fly. This can be generalized to a plausible rule: if a class has a component used for some capability, then an instance of the class without this component does not have this capability. We can write this as a clause in json-ld-logic:

[["-hasa", "?:O", "?:C"], ["-usedfor", "?:U", "?:O"], ["-be","?:C","?:I"], ["hasa", "?:O", "?:I"],

Without a selection of suitable priorities and / or differentiation between rules for class and instance, the rule above does not always lead to expected results. Consider an example for flying and wings, where the usage of wings and the flying capability of birds come directly from the translation of conceptnet and quasi_full above. We assume that an arbitrary bird_constant does not have wings and we want to prove that it cannot fly.
  • demo/partcapability1.js and gk output, search outline trace. Here the birds having wings and birds having a capability to fly have the same priority, leading to unstable results: the proof is found or not found, depending on the depth of the validation tree, which depends on the time allocated.
  • demo/partcapability2.js and gk output, search outline trace. Here the birds having wings is given a priority over birds having a capability to fly, leading to a stable result: the proof is always found.
  • demo/partcapability3.js and gk output, search outline trace. Here the birds having wings is split into two versions: the rule for a class does not have an exception, while the rule for an instance does have an exception. The priorities are as in the first example partcapability1. This again leads to a stable result: the proof is always found.

Comparison with the ASP approach

Other systems able to handle default reasoning typically use the Answer Set Programming (ASP) approach, which instantiates first order problems to a large propositional formula. The ASP approach works well in cases where the input rules do not contain function symbols and do not contain a large number of constants.

Gk is able to function without such limitations. We take the simplest "birds fly, but penguins do not" problem, here in the s(CASP) Prolog syntax:

bird(X) :- penguin(X).
flies(X) :- bird(X), not -flies(X).
-flies(X) :- penguin(X). 

flies(b1) ?
and modify it by adding (a) rules with function symbols in the head (b) a transitive rule and a large number of constants. None of the leading default-rule-capable ASP systems clingo, dlv or s(CASP) can handle such problems, even though they do allow function symbols to be used and set no strict limits on the number of constants in the input file.

The following are example inputs for all of them and gk, encoding the same problems. The systems were run on a laptop with a 10-th generation i7 processor. The versions with constants are slightly different for each ASP system: some of the rules had to be commented out to make the system terminate. The s(CASP) system does not terminate when a transitivity axiom is added, even with a small number of constants. Gk typically spends ca half of the time it is given even if not needed, hence we ran the small examples with the time limit -seconds 1 and the 100k example with -seconds 10.

We note that all the ASP systems here are excellent when used for the restricted classes they are designed for. Full first order logic is not their focus.


Technology, authors, contact

Gk is written in C by Tanel Tammet (tanel.tammet at taltech.ee) and is based on the conventional first order logic reasoner gkc by the same author. The gkc prover uses the whitedb shared memory database written by Tanel Tammet and Priit Järv for internal datastructures.

The knowledge graphs are built by Priit Järv (priit.jarv1 at taltech.ee).

The theoretical ideas behind gk and the knowledge graph conversions come from Tanel Tammet, Dirk Draheim and Priit Järv from Tallinn University of Technology.