Reasoner examples with gkc
Sisukord
Get the reasoner
Two ways to get the reasoner: Either download pre-compiled:
- Media:gkc.zip zipped gkc.exe for windows
- Media:gkc-mac.tar.gz tar-gzipped gkc for OS X (64 bit, compiled for mac os mojave using clang, NOT statically compiled, i.e. may require ok core libs)
- release v0.1-beta: from the assets block at the end get the gkc.zip for Windows and unzip or get the gkc executable for Linux
or clone the https://github.com/tammet/gkc or take source from https://github.com/tammet/gkc/releases/tag/v0.1-beta and compile yourself. Instructions in README.md:
- call compile.sh on Linux (needs gcc or clang)
- compile.bat on windows (needs visual C community edition command line cl)
- modified compile.sh on OS X: if it does not compile unmodified, remove the -static flag from compile.sh and then try again. Tested using clang on mac os mojave with the -static flag removed.
You could also try out an old classic prover Otter which actually works OK on windows even though it is really old.
Use the reasoner
Call it like this from the command line (you may rename gkc_01 to gkc or use as-is and for the newer gkc version you may write -prove instead of lrunreasoner or drop this command altogether):
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
About input and output in the following examples
All the words starting with capital letters like X are variables, others like john are constants.
Minus sign is negation, i.e. "-father ..." means "not father ..."
Vertical bar | is logical or.
Each fact / rule is terminated by a period .
Percentage sign is a line comment.
Output proof consists of numbered steps: each step is either a used input fact / rule or a derived fact / rule.
The [in,axiom] means that this fact/rule was given in input.
The [mp, 1, 2, fromaxiom] means that this fact / rule was derived by modus ponens (i.e. the resolution rule) from previous steps 1 and 2. Ignore the "fromaxiom" piece of information. More concretely, the first literals of both were cut off and the rest were glued together.
The [mp, 8.1, 5, fromaxiom] means that the second literal in the clause at proof step 8 was cut off with the first literal of the clause at proof step 5. I.e. literals in a clause are numbered 0, 1, 2, etc and the number 0 is not added to the step number.
The [=, 1, 2.0.2, 3, fromaxiom] means that the clause at step 1 was used to replace a subterm of clause at step 2 using equality and then a direct contradiction of the result with the step 3 clause was found.
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 "ans" 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
