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.
  • cskb_jan23.tar.xz : in JS format for the GK reasoner, 5 GB unpacked.
  • cskb_jan23_jsonl.tar.xz : in JSONL format, recommended if you are not planning to use GK.

Datasets built from the hypernym and hyponym relations of Wordnet:

• gk_name_number.txt : a mapping of Wordnet synsets to class numbers
• gk_taxonomy_packed.txt : packed topologically sorted class taxonomies

Examples

Examples for default logic:

• trivial.js and gk output : a trivial example without defaults or confidences
• penguin.js and gk output : a classic example of default rules and taxonomies
• penguin2.js and gk output : deeper taxonomy branches for penguin
• penguin3.js and gk output : penguin2.js version to be called with the -defaults key (see tutorial)
• penguin4.js and gk output, search outline trace. : modified penguin2.js, this time asking whether a grandfather of a penguin can fly. Rules added for nested terms like [["penguin", "?:X1"], "<=>" ,["penguin", ["father","?:X1"]]],: something is a bird/penguin if and only if its father is a bird/penguin.
• nixon.js and gk output : contradictory default rules
• people_room.js and gk output : describing a situation-event chain with default rules
• classify.js and gk output : confidences and default rules for simple classification
• kingqueen.js and gk output : handling similarities, call with the -similarities to use gk_similarity.txt (see tutorial)

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.

• quasi_babyhair.js and gk output, search outline trace. Do babys have hair? Both negative and positive evidence was found with a similar confidence, sub-proofs were invalidated.
• quasi_birdfly.js and gk output, search outline trace. Do birds fly? No subproofs were invalidated and no negative evidence found.
• quasi_penguinfly.js and gk output, search outline trace. Do penguins fly? A positive subproof was found (since penguins are birds) and invalidated, then a search for the negative evidence was performed, which was not invalidated, hence the answer is "false".
• cskb_ethanol.js and search outline trace. Does ethanol affect the nervous system? Uses facts from both Quasimodo and ConceptNet.
• cskb_beverage.js and search outline trace. Do alcoholic beverages affect the nervous system? Uses Quasimodo and similarities. This search requires more time (use -seconds 100).

Examples for confidences without default logic:

• rulemult.js and gk output : basic multiplication of confidences
• cumulate.js and gk output : basic cumulation of confidences
• socialsmoking.js and gk output : smoking confidences and rules
• socialsmoking2.js and gk output : smoking confidences and rules, another version
• near.js and gk output : a chain of confidences with transitivity
• near2.js and gk output : like near.js, but the chain is a constructed term
• steam.js and gk output : classic Schubert's steamroller puzzle with confidences added, run with -confidence 0 to remove limit
• dreadbury.js and gk output : classic Dreadbury mansion puzzle with confidences added, run with -confidence 0 to remove limit

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"],
  ["-capability","?:U","?: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(b1).
penguin(p1).

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.

The

• clingo 5.4.0: basic birds (ok), with function symbols (does not terminate), with 1000 constants (8 seconds), with 2000 constants (1 minute 40 seconds)
• dlv 2.1.1: basic birds (ok), with function symbols (does not terminate), with 1000 constants (7 seconds), with 2000 constants (1 minute)
• s(CASP) 0.21.10.09: basic birds (ok), with function symbols (does not terminate), with a transitivity rule (does not terminate),
• gk: basic birds (ok), with function symbols (0.4 seconds), with 1000 constants (0.3 seconds), with 2000 constants (0.3 seconds) with 100.000 constants (5 seconds)

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.