This web page is about leanTAP, and via this one, you can get the source code. To run leanTAP with SWI-Prolog, the code must be slightly changed as it is explained here. .
Melvin Fitting published leanTAP Revisited, a paper containing source code in Prolog of another provers made from leanTAP.
By adding small stuff, I made the leanTAP for full FOL prover, though this is a first version in a hurry which probably has small bugs or fatal bugs. For me, lean TAP looks exactly one-sided LK. Once I wrote a (toy) ordered linear ancestoral resolution prover with iterated deepening method around 1993 which is still buried in library(pac/util/fol.pl), which uses prenex normal form via skolemization. With such a little experience, leanTAP is very exiting paper for me. Thanks.
% ?- lk((-p, -(-p))).
% ?- lk((p->p)).
% ?- lk(-(p->p)).
% ?- lk(all(X, -p(X) -> -(-p(X)))).
% ?- lk(all(X, p(X) -> -(-p(X)))).
% ?- lk(some(X, (p(X); q(X))) -> (some(Y, p(Y); some(Z, q(Z))))).
% ?- lk(all(X, p(X)) -> -(some(Y, -p(Y)))).
lk(E):- lk(-E, 10).
%
lk(E, L):- lk_left(E, [], [], [], L).
% borrowed from leanTAP
prove(E, A, B, C, D):- lk_left(E, A, B, C, D).
%
lk_left((E,F), A, B, C, D) :- !,
lk_left(E, [F|A], B, C, D).
lk_left((E;F), A, B, C, D) :- !,
lk_left(E, A, B, C, D),
lk_left(F, A, B, C, D).
lk_left((E->F), A, B, C, D) :- !,
lk_left((-E; F), A, B, C, D).
lk_left(all(I,J), A, B, C, D) :- !,
\+length(C,D),
copy_term((I,J,C), (G,F,C)),
append(A, [all(I,J)], E),
lk_left(F, E, B, [G|C],D).
lk_left(some(I,J), A, B, C, D) :- !,
copy_term((I,J,C), (G,F,C)),
numbervars(G),
lk_left(F, A, B, C, D).
lk_left(-E, A, B, C, D):- one_step_negate(E, E0), !,
lk_left(E0, A, B, C, D).
lk_left(A, _, [C|D], _, _) :-
( (A = -(B);-(A) = B) ->
( unify_with_occurs_check(B, C)
; lk_left(A, [], D, _, _)
)
).
lk_left(A, [E|F], B, C, D) :- lk_left(E, F, [A|B], C, D).
%
one_step_negate(-E, E).
one_step_negate((E;F), (-E, -F)).
one_step_negate((E,F), (-E; -F)).
one_step_negate((E->F), (E, -F)).
one_step_negate(all(I, J), some(I, -J)).
one_step_negate(some(I, J), all(I, -J)).Interestingly, at about the same time that leanTAP was developed by Beckert and Posegga Manthey and Bry developed the theorem prover Satchmo that like leanTAP consists of a few lines of Prolog and is equally powerful.
Here is a link to a paper that gives further details:
SATCHMO: A Theorem Prover Implemented in Prolog
R. Manthey, François Bry
Published in CADE 23 May 1988
Satchmo is a theorem prover consisting of just a few short and simple Prolog programs. Prolog may be used for representing problem clauses as well. SATCHMO is based on a model-generation paradigm. It is refutation-complete if used in a level-saturation manner. The paper provides a thorough report on experiences with SATCHMO. A considerable amount of problems could be solved with surprising efficiency.
After investigating leanTAP we decided to use Satchmo as the basis for our theorem prover RACE for Attempto Controlled English (ACE). See Attempto Tools and Resources.
Thanks for comment. In fact, I remember the name SACHIMO among other theorem provers based on Prolog technology, though I did not pay attention to them. Perhaps because I was rather getting more interested into proof assistant system like COQ, though only being interested; I can’t not use COQ yet. BTW, I happened to listen to an French visitor talk, in which
he touched that an engine of COQ is prolog-like unification, and that he planned to push further such direction.
Thanks. In fact, I thought exist-left of LK by numbervars would be most controversial point. I will enjoy to check in more detail.
I have no idea on it. I am busy on fixing basic operations on ZDD. However I feel there is room to extend the current ZDD structure of mine for ZDD for full FOL. For that, I know it might be best for me to ask ZDD experts (in Japan ?), but I am too shy to do so.
As you commented, Skolemization seems to fix, though the current fix is ad hoc. I don’t understand why the simple numbervars/1 does not work in spite of seemingly faithful implementation of eigen variable of exists_left rule of LK. I will try numbervars/3 for avoiding generated number possible conflict. Anyway Skolemization seems not expensive for leanTAP.
% ?- lk((some(Y,p(Y))->all(X,p(X)))).
%@ false.
lk_left(some(I,J), A, B, C, D) :- !,
copy_term((I,J,C), (G,F,C)),
adhoc_numbervars_as_skolemize(C, G),
lk_left(F, A, B, C, D).
adhoc_numbervars_as_skolemize(C, G):- gensym(sk, SKF),
G=..[SKF|C].
numbervars/3 seems to work, which fits my intuition of the role of eigen variable of exist-left of LK. Anyway I am sure for nothing, but just interesting. I would like to take time. Your analysis is useful, though I am not sure I understand correctly. Thanks.
I could not find yet a false positive example for numbervars/3 use. It would be too lucky if numbervars/3 works as my naive understanding exist-left rule of LK. Also I wish find the counter example to go to so called more safe skolemization.
EDIT: For me, it seems not difficult to prove the equivalence between 1 and 2 by way of induction on structure of formulae.
numbervars/3 succeeds with “provable” for F.I added iterative deepening feature to leanTAP.
% ?- lk(some(Y, p(Y)) -> some(X, some(Z, p(X); q(Z)))).
%@ depth_limit_info=12
%@ true .
% ?- lk(some(X, p(X)) -> some(X, some(Z, p(X); q(Z)))).
%@ depth_limit_info=12
%@ true .
% ?- lk(p(a) -> some(X, some(Y, p(X); q(Y)))).
%@ depth_limit_info=11
%@ true .
(Nothing of Relevance here)
Sorry. I thought it is clear without source. demorgan/3 below
is a renamed predicate for readability. iterated_deepening should be clear, which is a wrapper for call_with_depth_limit/4
lk(E):- lk(E, 10, 10, 10).
%
lk(E, L, D, N):- iterated_deepening(lk_left(-E, [], [], [], L, 0), D, N, R),
writeln(depth_limit_info = R).
%
lk(E, L):- lk_left(-E, [], [], [], L, 0).
% Borrowed from leanTAP.
lk_left((E,F), A, B, C, D, N) :-!,
lk_left(E, [F|A], B, C, D, N).
lk_left((E;F), A, B, C, D, N) :-!,
lk_left(E, A, B, C, D, N),
lk_left(F, A, B, C, D, N).
lk_left((E->F), A, B, C, D, N) :-!,
lk_left((-E; F), A, B, C, D, N).
lk_left(all(I,J), A, B, C, D, N) :-!,
\+length(C,D),
copy_term((I,J,C), (G,F,C)),
append(A, [all(I,J)], E),
lk_left(F, E, B, [G|C], D, N).
lk_left(some(I,J), A, B, C, D, N) :-!,
copy_term((I,J,C), (G,F,C)),
numbervars(G, N, N0),
lk_left(F, A, B, C, D, N0).
lk_left(-E, A, B, C, D, N):- demorgan(E, E0), !,
lk_left(E0, A, B, C, D, N).
lk_left(A, _, [C|D], _, _, N) :-
( (A = -(B); -(A) = B) ->
( unify_with_occurs_check(B, C)
; lk_left(A, [], D, _, _, N)
)
).
lk_left(A, [E|F], B, C, D, N) :- lk_left(E, F, [A|B], C, D, N).
%
demorgan(-E, E).
demorgan((E;F), (-E, -F)).
demorgan((E,F), (-E; -F)).
demorgan((E->F), (E, -F)).
demorgan(all(I, J), some(I, -J)).
demorgan(some(I, J), all(I, -J)).
I will keep your comment in mind. Also I have found a name of a researcher in the link who, I heard, was a student of Martin-Loef P, which is impressive for me. Anyway I regret to say I could not follow details of contents, but seems interested works are ongoing.
Thank you nice counter example !! I am ashamed, but thank you.
"For iterative deepening I didn’t use some library, but simply:
A nice counter example !! I am ashamed, but thank you. "
Also, I was not sure that the number of bound variables can be used as a measure on depth of proof trees. I was afraid of possible unlimited depth branch irrelevant to the current number of bound variables.
I confused constructing a goal formula from axioms with
finding a proof tree with given a goal. LK rule in the literature
is explained as rule for the former, that is, from leaves to root.
For example, take variable condition of eigen variables. Skolemization is natural because in all(x, exist(y, p(y, x))), y is dependent to x, so y in p(y, x) is not “free” in this sense. But in the rule of exist-left rule, variable condition says simply it is applicable when y does not appear free in the lower sequent.
That said, however still I am not convinced, what is a real source of my confusion ?
EDIT: On proof finding, I have noticed that upper sequent may not keep validity when it contains constant variables generated numbervars, but on the contrary it does always keep validity when skolem functions are used. This is my tentative answer to my question.
Anyway I wrote back codes from numbervars to the skolemzation, which gave the right answer so far.
I have tried to check the root of proof wrong finding by numbervars. The unification and numbervars are the only “rules” that are not allowed as LK rule. All the others are LK admissible rules. So my confusion might be just a confusion between object variables and meta-variables (Prolog variables). I am not convinced but possible.
--------------------------------------------------------LK Axiom
p($VAR(1), $VAR(0)), -p($VAR(1), $VAR(0)) =>
------------------------------------------------[X := $VAR(1), Y := $VAR(0) by Prolog unification]
p(X, $VAR(0)), -p($VAR(1), Y) =>
-------------------------------------------- [some: $VAR(1) by numbervars]
p(X, $VAR(0)), some(x, -p(x, Y) =>
-------------------------------------------------
p(X, $VAR(0)), -all(x, p(x, Y) =>
--------------------------------------------------- [all: y -> Y]
p(X, $VAR(0)), all(y, -all(x, p(x, y)) =>
-----------------------------------------------------
p(X, $VAR(0)), -some(y, all(x, p(x, y)) =>
-----------------------------------------------------[some: y->$VAR(0) by bumbervars]
some(y, p(X, y)), -some(y, all(x, p(x, y)) =>
-------------------------------------------------------- [all: x -> X]
all(x, some(y, p(x,y)), -some(y, all(x, p(x, y)) =>
Thank you for your detailed diagnosis. Now you teach me that
naive numbervars approach simply may violate the side condition of eigen variable condition, which is simply, I think, the root !
What is really nice about this paper is that it is a step by step explanation with simple prolog examples – which makes it much more accessible than papers heavy in formalism – even short ones (papers and formalism).
It would be great if this paper could become part of a swish example …
Dan
I have written codes from scratch to get prenex normal form for using the leanTAP. I use call_with_depth_limit/3 because otherwise it does’t terminate for a valid formula e.g. (some(x, (p(x)-> all(y, p(y)))), which, I checked that it is provable in NK by hand. I feel fine that finally I got an handy small calculator in my hand. I regret to have no time to go into more details.
%
prove(P):- prenex_normal_form(-P, PNF),
itr_depth_prove(PNF, 2, 4).
itr_depth_prove(PNF, D, V):-
call_with_depth_limit(leanTAP(PNF, [], [], [], V), D, R),
( R == depth_limit_exceeded ->
D0 is 2*D,
V0 is V+10,
itr_depth_prove(PNF, D0, V0)
; true
).
% This exactly the leanTAP in the abstract of the paper.
leanTAP((E,F), A, B, C, D) :-!,
leanTAP(E, [F|A], B, C, D).
leanTAP((E;F), A, B, C, D) :-!,
leanTAP(E, A, B, C, D),
leanTAP(F, A, B, C, D).
leanTAP(all(I,J), A, B, C, D) :-!,
\+length(C,D),
copy_term((I,J,C), (G,F,C)),
append(A, [all(I,J)], E),
leanTAP(F, E, B, [G|C], D).
leanTAP(A, _, [C|D], _, _) :-
( (A = -(B); -(A) = B) ->
( unify_with_occurs_check(B, C)
; leanTAP(A, [], D, _, _)
)
).
leanTAP(A, [E|F], B, C, D) :- leanTAP(E, F, [A|B], C, D).
No at all, but I use “prenex_normal_form” simply as the internal form for the leanTAP codes allows as internal form. Below are sample queries. My purpose was to use that short leanTAP codes as a pocket but full FOL prover without changing the codes. For that, negation operators are moved to inner most by deMorgan, universal quantifiers are NOT moved, but existential quantifiers are skolemized.
% ?- prenex_normal_form(a, P).
%@ P = a.
% ?- prenex_normal_form(or(a,b), P).
%@ P = (a;b).
% ?- prenex_normal_form(some(a, p(a)), P).
%@ P = p(sk50).
% ?- prenex_normal_form(some(a, p(a)->p(a)), P).
%@ P = (-p(sk51);p(sk51)).
% ?- prenex_normal_form(some(a, all(b, p(a,b)->p(a,b))), P).
%@ P = all(_A, (-p(sk52, _A);p(sk52, _A))).
% ?- prenex_normal_form(all(a, some(b, p(a,b))), P).
%@ P = all(_A, p(_A, sk53(_A))).
% ?- prenex_normal_form(not(some(a, all(b, p(a,b)))), P).
%@ P = all(_A, -p(_A, sk54(_A))).
prenex_normal_form(F, P):- intern(F, I),
neg_normal(I, N),
rename_vars(N, [], N0),
skolem(N0, [], P).
I can easily guess that nowadays, my codes is a student home work level, and more worse I find myself I have no goal, but just enjoying prolog coding because of surprisingly short codes of leanTAP.