Reasoner examples with gkc 2020 - Redigeerimiste ajalugu

Tammet: /* About input and output in the following examples */

2020-02-28T18:46:04Z

About input and output in the following examples

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 20:46
90. rida:		90. rida:

	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 [=, 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 ==		== Telling gkc what is actually the question clause in input ==

Tammet: /* Telling gkc what is actually the question clause in input */

2020-02-28T12:26:31Z

Telling gkc what is actually the question clause in input

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 14:26
106. rida:		106. rida:
	<pre>		<pre>
	fof(q1,negated_conjecture,		fof(q1,negated_conjecture,
	-father(john,pete).		-father(john,pete)).
	</pre>		</pre>

Tammet: /* Telling gkc what is actually the question clause in input */

2020-02-28T12:26:07Z

Telling gkc what is actually the question clause in input

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 14:26
93. rida:		93. rida:
	== Telling gkc what is actually the question clause in input ==		== Telling gkc what is actually the question clause in input ==

	Gkc does not know which clause is a question: this is bad for		Gkc does not know which clause is a question: this is ok,
	efficiency in case of large clause sets.		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		There is a simple way to tell gkc that some clause is indeed a question

Tammet: /* Telling gkc what is actually the question clause in input */

2020-02-28T12:25:28Z

Telling gkc what is actually the question clause in input

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 14:25
105. rida:		105. rida:
	write it with this wrapping (observe double parentheses at the end):		write it with this wrapping (observe double parentheses at the end):
	<pre>		<pre>
	fof(q,negated_conjecture,		fof(q1,negated_conjecture,
	-father(john,pete).		-father(john,pete).
	</pre>		</pre>

	and then gkc knows that this clause should get priority in search.		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		More generally, gkc can also read a more complex syntax for clauses and

Tammet – 28. veebruar 2020, kell 12:23

2020-02-28T12:23:50Z

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 14:23
90. rida:		90. rida:

	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 [=, 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 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(q,negated_conjecture,
			-father(john,pete).
			</pre>

			and then gkc knows that this clause should get priority in search.

			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: ==		== Example 1: ==

Tammet: /* Output and tuning the prover */

2020-02-28T08:10:38Z

Output and tuning the prover

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 10:10
66. rida:		66. rida:
	</pre>		</pre>

	In the following examples we will skip the irrelevant part of output.		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 ==		== About input and output in the following examples ==

Tammet – 28. veebruar 2020, kell 08:09

2020-02-28T08:09:30Z

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 10:09
121. rida:		121. rida:
	== Example 2 ==		== 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.		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:		Input:
132. rida:		132. rida:
	Relevant part of output:		Relevant part of output:
	<pre>		<pre>
	~~found pure~~ answer: ans(pete).		answer: $ans(pete).
	Proof found.		Proof found.

154. rida:		154. rida:
	-father(X,Y) \| -father(Y,Z) \| grandfather(X,Z).		-father(X,Y) \| -father(Y,Z) \| grandfather(X,Z).

	-grandfather(john,X) \| ans(X).		-grandfather(john,X) \| $ans(X).
	</pre>		</pre>
	Relevant part of output:		Relevant part of output:
	<pre>		<pre>
	~~found pure~~ answer: $ans(mark).		answer: $ans(mark).
	Proof found.		Proof found.

191. rida:		191. rida:
	Relevant part of output:		Relevant part of output:
	<pre>		<pre>
	~~found pure~~ answer: $ans(mickey) \| $ans(mark).		answer: $ans(mickey) \| $ans(mark).
	Proof found.		Proof found.

227. rida:		227. rida:
	Relevant output:		Relevant output:
	<pre>		<pre>
	~~found pure~~ answer: $ans(john).		answer: $ans(john).
	Proof found.		Proof found.

	proof:		proof:

	1: [in,axiom] -ancestor(X,mark) \| ans(X).		1: [in,axiom] -ancestor(X,mark) \| $ans(X).
	2: [in,axiom] ancestor(X,Y) \| -father(X,Y).		2: [in,axiom] ancestor(X,Y) \| -father(X,Y).
	3: [in,axiom] father(pete,mark).		3: [in,axiom] father(pete,mark).
264. rida:		264. rida:
	ancestor(father(X),X).		ancestor(father(X),X).

	-ancestor(X,mark) \| ans(X).		-ancestor(X,mark) \| $ans(X).
	</pre>		</pre>
	Relevant output:		Relevant output:
	<pre>		<pre>
	~~found pure~~ answer: ans(father(mark)).		answer: $ans(father(mark)).
	Proof found.		Proof found.

	proof:		proof:

	1: [in,axiom] -ancestor(X,mark) \| ans(X).		1: [in,axiom] -ancestor(X,mark) \| $ans(X).
	2: [in,axiom] ancestor(father(X),X).		2: [in,axiom] ancestor(father(X),X).
	3: [mp, 1, 2,fromaxiom] false		3: [mp, 1, 2,fromaxiom] false
298. rida:		298. rida:
	-ancestor(X,Y) \| -ancestor(Y,Z) \| ancestor(X,Z).		-ancestor(X,Y) \| -ancestor(Y,Z) \| ancestor(X,Z).

	-grandfather(X,mark) \| ans(X).		-grandfather(X,mark) \| $ans(X).
	</pre>		</pre>
	Relevant output:		Relevant output:
	<pre>		<pre>
	~~found pure~~ answer: ans(father(father(mark))).		answer: $ans(father(father(mark))).
	Proof found.		Proof found.

	proof:		proof:

	1: [in,axiom] -grandfather(X,mark) \| ans(X).		1: [in,axiom] -grandfather(X,mark) \| $ans(X).
	2: [in,axiom] grandfather(father(father(X)),X).		2: [in,axiom] grandfather(father(father(X)),X).
	3: [mp, 1, 2,fromaxiom] false		3: [mp, 1, 2,fromaxiom] false

Tammet – 28. veebruar 2020, kell 08:07

2020-02-28T08:07:07Z

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 10:07
121. rida:		121. rida:
	== Example 2 ==		== 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.		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:		Input:
128. rida:		128. rida:
	father(pete,mark).		father(pete,mark).

	-father(john,X) \| ans(X).		-father(john,X) \| $ans(X).
	</pre>		</pre>
	Relevant part of output:		Relevant part of output:
137. rida:		137. rida:
	proof:		proof:

	1: [in,axiom] -father(john,X) \| ans(X).		1: [in,axiom] -father(john,X) \| $ans(X).
	2: [in,axiom] father(john,pete).		2: [in,axiom] father(john,pete).
	3: [mp, 1, 2,fromaxiom] false		3: [mp, 1, 2,fromaxiom] false
158. rida:		158. rida:
	Relevant part of output:		Relevant part of output:
	<pre>		<pre>
	found pure answer: ans(mark).		found pure answer: $ans(mark).
	Proof found.		Proof found.

	proof:		proof:

	1: [in,axiom] -grandfather(john,X) \| ans(X).		1: [in,axiom] -grandfather(john,X) \| $ans(X).
	2: [in,axiom] grandfather(X,Y) \| -father(Z,Y) \| -father(X,Z).		2: [in,axiom] grandfather(X,Y) \| -father(Z,Y) \| -father(X,Z).
	3: [in,axiom] father(pete,mark).		3: [in,axiom] father(pete,mark).
187. rida:		187. rida:


	-grandfather(john,X) \| ans(X).		-grandfather(john,X) \| $ans(X).
	</pre>		</pre>
	Relevant part of output:		Relevant part of output:
	<pre>		<pre>
	found pure answer: ans(mickey) \| ans(mark).		found pure answer: $ans(mickey) \| $ans(mark).
	Proof found.		Proof found.

	proof:		proof:

	1: [in,axiom] -grandfather(john,X) \| ans(X).		1: [in,axiom] -grandfather(john,X) \| $ans(X).
	2: [in,axiom] grandfather(X,Y) \| -father(Z,Y) \| -father(X,Z).		2: [in,axiom] grandfather(X,Y) \| -father(Z,Y) \| -father(X,Z).
	3: [in,axiom] father(pete,mark) \| father(pete,mickey).		3: [in,axiom] father(pete,mark) \| father(pete,mickey).
202. rida:		202. rida:
	5: [in,axiom] father(john,pete).		5: [in,axiom] father(john,pete).
	6: [mp, 4.1, 5,fromaxiom] grandfather(john,mickey) \| father(pete,mark).		6: [mp, 4.1, 5,fromaxiom] grandfather(john,mickey) \| father(pete,mark).
	7: [mp, 1, 6,fromaxiom] father(pete,mark) \| ans(mickey).		7: [mp, 1, 6,fromaxiom] father(pete,mark) \| $ans(mickey).
	8: [mp, 7, 2.1,fromaxiom] ans(mickey) \| -father(X,pete) \| grandfather(X,mark).		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).		9: [mp, 8.1, 5,fromaxiom] grandfather(john,mark) \| $ans(mickey).
	10: [mp, 9, 1,fromaxiom] false		10: [mp, 9, 1,fromaxiom] false
	</pre>		</pre>
223. rida:		223. rida:
	-father(X,Y) \| ancestor(X,Y).		-father(X,Y) \| ancestor(X,Y).

	-ancestor(X,mark) \| ans(X).		-ancestor(X,mark) \| $ans(X).
	</pre>		</pre>
	Relevant output:		Relevant output:
	<pre>		<pre>
	found pure answer: ans(john).		found pure answer: $ans(john).
	Proof found.		Proof found.

Tammet: /* Use the reasoner */

2020-02-28T08:04:35Z

Use the reasoner

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 10:04
18. rida:		18. rida:
	</pre>		</pre>

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

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

	~~Here lrunreasoner is a command to gkc.~~

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

Tammet: /* Get the reasoner */

2020-02-28T08:03:46Z

Get the reasoner

←Vanem redaktsioon		Redaktsioon: 28. veebruar 2020, kell 10:03
1. rida:		1. rida:
	== Get the reasoner ==		== Get the reasoner ==

	Two ways to get the reasoner from its [https://github.com/tammet/gkc github repo] releases, either download latest release pre-compiled:		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.exe gkc.exe for windows]
	* [https://github.com/tammet/gkc/releases/download/v0.4.1/gkc gkc for linux]		* [https://github.com/tammet/gkc/releases/download/v0.4.1/gkc gkc for linux]
9. rida:		9. rida:
	* compile.bat on windows (needs visual C community edition command line cl)		* 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.		* 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 ==		== Use the reasoner ==