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
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"],
["-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.