Reasoner examples with gkc 2020
Sisukord
Get the reasoner
Two ways to get the gkc reasoner from its github repo releases, either download latest release pre-compiled:
- gkc.exe for windows
- gkc for linux
- Media:gkc-mac.tar.gz tar-gzipped older version of gkc for OS X (64 bit, compiled for mac os mojave using clang, NOT statically compiled, i.e. may require ok core libs)
or clone the gkc repo or take source from the latest release 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.
Use the reasoner
Call it like this from the command line:
gkc problemfilename
For example, copy-paste the input in the following examples to a file example.txt and run
gkc example.txt
You may want to send output to a file in a standard way like this:
gkc example.txt > out.txt
Output and tuning the prover
By default the prover automatically selects a number of strategies to run one-by one and outputs a lot of statistics and detailed information. The important part is a block which looks like
result: proof found % SZS status Unsatisfiable for n12.txt. answer: $ans(pete). % SZS output start CNFRefutation for n12.txt 1: [in, axiom] father(john,pete). 2: [in, axiom] -ancestor(john,X) | $ans(X). 3: [in, axiom] ancestor(X,Y) | -father(X,Y). 4: [mp, 2, 3, fromaxiom] -father(john,X) | $ans(X). 5: [mp, 1, 4, fromaxiom] $ans(pete). % SZS output end CNFRefutation for n12.txt
It is a good idea to tell the prover the exact strategy and output level by writing a small json strategy file strat.txt with the recommended content:
{
"print_level": 10,
"max_seconds": 1,
"strategy":["query_focus"],
"query_preference": 1
}
and then call the prover like this to make it use the strategy file:
gkc example.txt strat.txt
In the following examples we will skip the irrelevant part of output and the details of the output are taken from an older gkc version, with slight differences.
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.
The [simp, 1, 2,fromaxiom] means the same as the [mp,...] above, just a specially simple case.
Telling gkc what is actually the question clause in input
Gkc does not know which clause is a question: this is ok, but it is bad for efficiency in case of large clause sets.
There is a simple way to tell gkc that some clause is indeed a question and gkc should heavily focus on that clause.
Instead of writing your negated question like
-father(john,pete).
write it with this wrapping (observe double parentheses at the end):
fof(q1,negated_conjecture, -father(john,pete)).
and then gkc knows that this clause should get priority in search. The "q1" in the example is just a freely choosable name for the clause, while "negated_conjecture" tells gkc that this is a negated question.
More generally, gkc can also read a more complex syntax for clauses and full nested formulas, as given in the TPTP technical manual, which is a really hard read, look for "fof" formulas, or better yet, see this example.
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 "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:
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:
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:
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:
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:
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:
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
