Lehekülje Reasoner examples with gkc 2020 lähteteksti vaatamine

== Get the reasoner ==

Two ways to get the gkc reasoner from its [https://github.com/tammet/gkc github repo] releases, either download latest release pre-compiled:
* [https://github.com/tammet/gkc/releases/download/v0.4.1/gkc.exe gkc.exe for windows]
* [https://github.com/tammet/gkc/releases/download/v0.4.1/gkc 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 [https://github.com/tammet/gkc gkc repo] or take source from [https://github.com/tammet/gkc/releases/tag/v0.4.1 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:

<pre>
gkc problemfilename
</pre>

For example, copy-paste the input in the following examples to a file example.txt and run

<pre>
gkc example.txt
</pre>

You may want to send output to a file in a standard way like this:

<pre>
gkc example.txt > out.txt
</pre>

== 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
<pre>
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
</pre>

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:
<pre>
{
  "print_level": 10,     
  "max_seconds": 1,
  "strategy":["query_focus"],
  "query_preference": 1
}  
</pre>

and then call the prover like this to make it use the strategy file:

<pre>
gkc example.txt strat.txt
</pre>

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.

== 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
<pre>
-father(john,pete).
</pre>
write it with this wrapping (observe double parentheses at the end):
<pre>
fof(q1,negated_conjecture,
-father(john,pete)).
</pre>

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 [http://tptp.org/TPTP/TR/TPTPTR.shtml#FormulaeSection TPTP technical manual], which is a really hard read, look for "fof" formulas, or better yet, see [http://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN000+1.p this example].

== Example 1: ==

A trivial example.

Input:
<pre>
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
</pre>
Relevant part of output:
<pre>
proof:

 1: [in,axiom] -father(john,pete). 
 2: [in,axiom] father(john,pete). 
 3: [simp, 1, 2,fromaxiom] false
</pre>


== 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:
<pre>
father(john,pete).
father(pete,mark).

-father(john,X) | $ans(X).
</pre>
Relevant part of output:
<pre>
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
</pre>

== Example 3 ==

Now with a grandfather rule added and asking for a grandchild of John.

Input:
<pre>
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).
</pre>
Relevant part of output:
<pre>
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
</pre>

== Example 4 ==

Let us make it unclear which sons pete actually has:

Input:
<pre>
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).
</pre>
Relevant part of output:
<pre>
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
</pre>

== Example 5 ==

Adding an ancestor rule and looking for ancestors of mark.

Input:
<pre>
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).
</pre>
Relevant output:
<pre>
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
</pre>

== Example 6 ==

Reformulate the whole thing with equalities and functions! 
Notice that the proof does not use equalities, just functions.

Input:
<pre>
%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).
</pre>
Relevant output:
<pre>
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
</pre>


== Example 7 ==

Ask for the grandfather in the context of equalities and functions.
Notice that the proof does not use equalities, just functions.

Input:
<pre>
%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).
</pre>
Relevant output:
<pre>
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
</pre>


== Example 8 ==

Ask if the father of the father of john is mark.
Here the proof actually does use equalities.

Input:
<pre>
%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.
</pre>
Relevant output:
<pre>
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
</pre>