Reasoner examples with gkc
Get the reasoner
Two ways to get the reasoner: Either download pre-compiled:
- Media:gkc_01.zip gkc_01.exe for windows
- gkc release for Linux: download gkc_01 from assets.
Or clone the https://github.com/tammet/gkc and compile yourself (instructions in README.md)
Use the reasoner
Call it like this from the command line (you may rename gkc_01 to gkc or use as-is):
gkc lrunreasoner problemfilename
For example, copy-paste the input in the following to a file example.txt and run
gkc lrunreasoner example.txt
Here lrunreasoner is a command to gkc.
You may want to send output to a file in a standard way like this:
gkc lrunreasoner example.txt > out.txt
Example 1:
A trivial example.
Input:
father(john,pete). father(pete,mark). -father(john,pete). % what this means: % let us want to prove a & b => a % if we look for contradiction, then we should % try to find contradiction from % -(a & b => a) % which is equivalent to % a & b & -a
Relevant part of output:
proof: 1: [in,axiom] -father(john,pete). 2: [in,axiom] father(john,pete). 3: [simp, 1, 2,fromaxiom] false
Example 2
Like example 1, but we want to find a concrete person as an answer: we use the special "answer" predicate for this. Observe the "found pure answer: ans(pete). " line in the output stemming from this answer predicate.
Input:
father(john,pete). father(pete,mark). -father(john,X) | ans(X).
Relevant part of output:
found pure answer: ans(pete). Proof found. proof: 1: [in,axiom] -father(john,X) | ans(X). 2: [in,axiom] father(john,pete). 3: [mp, 1, 2,fromaxiom] false
Example 3
Now with a grandfather rule added and asking for a grandchild of John.
Input:
father(john,pete). father(pete,mark). % equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z). -father(X,Y) | -father(Y,Z) | grandfather(X,Z). -grandfather(john,X) | ans(X).
Relevant part of output:
found pure answer: ans(mark). Proof found. proof: 1: [in,axiom] -grandfather(john,X) | ans(X). 2: [in,axiom] grandfather(X,Y) | -father(Z,Y) | -father(X,Z). 3: [in,axiom] father(pete,mark). 4: [mp, 2.1, 3,fromaxiom] -father(X,pete) | grandfather(X,mark). 5: [in,axiom] father(john,pete). 6: [mp, 4, 5,fromaxiom] grandfather(john,mark). 7: [mp, 1, 6,fromaxiom] false
Example 4
Let us make it unclear which sons pete actually has:
Input:
father(john,pete). % either the first or a second or both facts are true: father(pete,mark) | father(pete,mickey). % equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z). -father(X,Y) | -father(Y,Z) | grandfather(X,Z). -grandfather(john,X) | ans(X).
Relevant part of output:
found pure answer: ans(mickey) | ans(mark). Proof found. proof: 1: [in,axiom] -grandfather(john,X) | ans(X). 2: [in,axiom] grandfather(X,Y) | -father(Z,Y) | -father(X,Z). 3: [in,axiom] father(pete,mark) | father(pete,mickey). 4: [mp, 2.1, 3.1,fromaxiom] father(pete,mark) | -father(X,pete) | grandfather(X,mickey). 5: [in,axiom] father(john,pete). 6: [mp, 4.1, 5,fromaxiom] grandfather(john,mickey) | father(pete,mark). 7: [mp, 1, 6,fromaxiom] father(pete,mark) | ans(mickey). 8: [mp, 7, 2.1,fromaxiom] ans(mickey) | -father(X,pete) | grandfather(X,mark). 9: [mp, 8.1, 5,fromaxiom] grandfather(john,mark) | ans(mickey). 10: [mp, 9, 1,fromaxiom] false
Example 5
Adding an ancestor rule and looking for ancestors of mark.
Input:
father(john,pete). father(pete,mark). % equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z). -father(X,Y) | -father(Y,Z) | grandfather(X,Z). -ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z). -father(X,Y) | ancestor(X,Y). -ancestor(X,mark) | ans(X).
Relevant output:
found pure answer: ans(john). Proof found. proof: 1: [in,axiom] -ancestor(X,mark) | ans(X). 2: [in,axiom] ancestor(X,Y) | -father(X,Y). 3: [in,axiom] father(pete,mark). 4: [mp, 2.1, 3,fromaxiom] ancestor(pete,mark). 5: [in,axiom] ancestor(X,Y) | -ancestor(Z,Y) | -ancestor(X,Z). 6: [mp, 4, 5.1,fromaxiom] -ancestor(X,pete) | ancestor(X,mark). 7: [in,axiom] father(john,pete). 8: [mp, 2.1, 7,fromaxiom] ancestor(john,pete). 9: [mp, 6, 8,fromaxiom] ancestor(john,mark). 10: [mp, 1, 9,fromaxiom] false
Example 6
Reformulate the whole thing with equalities and functions! Notice that the proof does not use equalities, just functions.
Input:
%father(john,pete). father(john)=pete. %father(pete,mark). father(pete)=mark. % equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z). %-father(X,Y) | -father(Y,Z) | grandfather(X,Z). grandfather(father(father(X)),X). -ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z). ancestor(father(X),X). -ancestor(X,mark) | ans(X).
Relevant output:
found pure answer: ans(father(mark)). Proof found. proof: 1: [in,axiom] -ancestor(X,mark) | ans(X). 2: [in,axiom] ancestor(father(X),X). 3: [mp, 1, 2,fromaxiom] false
Example 7
Ask for the grandfather in the context of equalities and functions. Notice that the proof does not use equalities, just functions.
Input:
%father(john,pete). father(john)=pete. %father(pete,mark). father(pete)=mark. % equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z). %-father(X,Y) | -father(Y,Z) | grandfather(X,Z). grandfather(father(father(X)),X). -ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z). -grandfather(X,mark) | ans(X).
Relevant output:
found pure answer: ans(father(father(mark))). Proof found. proof: 1: [in,axiom] -grandfather(X,mark) | ans(X). 2: [in,axiom] grandfather(father(father(X)),X). 3: [mp, 1, 2,fromaxiom] false
Example 8
Ask if the father of the father of john is mark. Here the proof actually does use equalities.
Input:
%father(john,pete). father(john) = pete. %father(pete,mark). father(pete) = mark. % equivalent to (father(X,Y) & father(Y,Z)) => grandfather(X,Z). %-father(X,Y) | -father(Y,Z) | grandfather(X,Z). grandfather(father(father(X)),X). -ancestor(X,Y) | -ancestor(Y,Z) | ancestor(X,Z). father(father(john)) != mark.
Relevant output:
Proof found. proof: 1: [in,axiom] =(father(john),pete). 2: [in,axiom] -=(father(father(john)),mark). 3: [in,axiom] =(father(pete),mark). 4: [=, 1, 2.0.2, 3,fromaxiom] false