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

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 .

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