Reasoner examples with gkc

Example 1:

Input:

father(john,pete).
father(pete,mark).

-father(john,X).

% 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 output:

proof:

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

Example 2:

Input:

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

proof:

 1: [in,axiom] -father(john,X). 
 2: [in,axiom] father(john,pete). 
 3: [mp, 1, 2,fromaxiom] false

Example 3: Call as

</pree>
Input:
<pre>

Relevant 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 : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output:

Example : Call as

</pree>
Input:
<pre>

Relevant output: