# leanTAP , a Prolog prover for Classical Logic **URL:** \ **Category:** Nice to know\ **Created:** [January 23, 2022, 11:24am UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930 "2022-01-23T11:24:12Z")\ **Posts on this page:** 18\ **Page:** 4
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 5:16pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/142 "2022-02-07T17:16:03Z")
> [@logicmoo](#): > > Aha, this whole time I was _assuming_ @kuniaki.mukai was writting a canonicalizer so that authorial logic statements could be converted into a prolog program or into a file for s(CASP). If it is only for short stints of theorem proving, then leanTAP is fine. Assuming kuniaki.mukai is the unique name, it is not me, but some other nice guy who is familiar with s(CASP), but I am not (sad). ---
**Author:** ![logicmoo](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/logicmoo/32/193_2.png) [@logicmoo](https://swi-prolog.discourse.group/u/logicmoo)\ **Post date:** [February 7, 2022, 5:23pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/143 "2022-02-07T17:23:29Z")
I see. Sorry I guess it was @fuchs that is converting English-\>DRS-\>FOL-\>Prolog > [@fuchs](#): > > for Attempto Controlled English (ACE). In my project we are converting English-\>DRS-\>FOL-\>Prolog But over the next few weeks seeing if English-\>DRS-\>FOL-\>s(CASP) will work out even better ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 5:29pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/144 "2022-02-07T17:29:12Z")
You are welcom. > [@logicmoo](#): > > English-\>DRS-\>FOL-\>Prolog/s(CASP) seems interesting. I bite a little bit DRS (Hans Kamp?). It sounds it is making constant progress. ---
**Author:** ![logicmoo](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/logicmoo/32/193_2.png) [@logicmoo](https://swi-prolog.discourse.group/u/logicmoo)\ **Post date:** [February 7, 2022, 5:34pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/146 "2022-02-07T17:34:38Z")
> [@kuniaki.mukai](#): > > Hans Kamp? Correct. In LOGICMOO we are adding time, beliefs and other modalities to translate. So far Prolog works out… but I still have to learn in s(CASP) will have nifty was of handling existential quantifiers… Prolog makes existential quantifiers a tricky thing ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 5:40pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/147 "2022-02-07T17:40:34Z")
> [@anon95304481](#): > > The same problem more readable with Unicode: > > (∀upau ∧ ∀vqbcv) → (∃x∀spxs ∧ ∃y∃z∀tqyzt) is valid. I run leanTAP for this formula in bounded depth-first search (BFS) mode plus varlimit. Only two skolem symbols are created. Thank you for the formula, sorry for disturbing. ```prolog % ?- F = -((all(u, p(a, u)), all(v, q(b,c, v))) -> % (some(x, all(s, p(x, s))), some(y, some(z, all(t, q(y, z, t)))))), % negation_normal_form(F, Fml), % bfs_prove(Fml, 3, 10), % numbervars(Fml). %@ F = - (all(u, p(a, u)), all(v, q(b, c, v))->some(x, all(s, p(x, s))), some(y, some(z, all(t, q(y, z, t))))), %@ Fml = ((all(A, p(a, A)), all(B, q(b, c, B))), (all(C, -p(C, sk24(C)));all(D, all(E, -q(D, E, sk25(E, D)))))). ``` ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 6:10pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/149 "2022-02-07T18:10:11Z")
I will keep my (own?) definition of “nnf” as far as no trouble occurs. Of course I can imagine troubles with big arity of skolem functions. I hope I am flexible to try to find a way for fixing. To be honest, despite of your explanations and references, still I can not imagine situations in which skolem functions are not good. I am extremely lazy to read papers. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 6:39pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/151 "2022-02-07T18:39:34Z")
There is one thing which I want to be clear first. Is the tentative rough definition of NNF is correct ? EDIT: Defintion of NNF. A term A is NNF if one of conditions holds. 1. literals are NNF. ex. like(a, b), -like(a, b) 2. if A, B are literal then (A, B) and ( A; B) are NNF 3. if A is NNF and x is a variable then all(x, A) and some(x, A) are NNF. 4. otherwise, A is not NNF. Remark: some(x, like(a, x)) is NNF. `-` (like(a, b) ; like(b, a))" is not NNF. This definition matches with Wikipedia, thanks B.Jan ---
**Author:** ![logicmoo](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/logicmoo/32/193_2.png) [@logicmoo](https://swi-prolog.discourse.group/u/logicmoo)\ **Post date:** [February 7, 2022, 6:45pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/153 "2022-02-07T18:45:11Z")
`- (like(a, b) ; like(b, a))` is not NNF since the negation is not moved inward the NNF form is `-like(a, b) & -like(b, a)` ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 6:48pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/154 "2022-02-07T18:48:04Z")
Thanks, but I also said. “- (like(a, b) ; like(b, a))” is not NNF. “-” is negation operater here. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 6:57pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/156 "2022-02-07T18:57:50Z")
> [@anon95304481](#): > > Once again please read the wikipedia page. Thank you again. Now I am pretty sure that my tentative definition is exactly match. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 7:09pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/158 "2022-02-07T19:09:07Z")
> [@anon95304481](#): > > b. if A is NNF and x is a variable then some(x, A) is NNF. Thanks again. leanTAP has no clause for some(x, p(x)), so guessed nnf (as leanTAP process internally) has not some(-,-). In summary nnf is the form in which negation operator appears only in literals. That’s all. Thanks. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 7:21pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/160 "2022-02-07T19:21:03Z")
I will check it later if source is available. leanTAP sounds having power of processing LK directly even with two sided sequents. For now I am little bit tired, but surely come back to such powerful leanTAP which is unknown to me ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 7:49pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/162 "2022-02-07T19:49:11Z")
Now I am sure about NNF(negation normal form), here is codes for the `negetion_normal_form`. Some codes are for clausal form for resolution in the future. This is polished version of my old codes 30 years ago and nothing interest for readers, I am afraid. ```prolog % ?- negation_normal_form(-(a=:=b), P). negation_normal_form(F, P):- intern(F, I), neg_normal(I, N), rename_vars(N, [], N0), skolem(N0, [], P). % ?- cnf(a, P). % ?- cnf(all(x, p(x,x))->all(y,p(y,y)), P). % ?- cnf(a;a, P). % ?- cnf(a; -a, P). cnf(F, C):- negation_normal_form(F, P), normal_boole_cnf(P, C0), rm_tautology(C0, C). % ?- intern((a,b), X), neg_normal(X, Y), rename_vars(Y, [], U), skolem(U, [], V). % ?- rename_vars(some(a, p(a, b)), [], U). % ?- rename_vars(some(a, all(b, -p(a, b)-> -q(a, c))), [], U). % ?- rename_vars(some(a, all(b, -p(a, b))); some(a, all(b, -p(a, b))), [], U). % ?- rename_vars(some(a, all(b, -p(a, b))); some(a, all(b, -p(a, c))), [], U). % ?- rename_vars(some(a, all(b, -p(a, b))); some(a, all(b, -p(a, b))), [], U). q_assoc(X, Assoc, Y):- member(U-V, Assoc), X==U, !, Y = V. q_assoc(X, _, X). % q_subst(Assoc, A, A0):- (var(A); atom(A)), !, q_assoc(A, Assoc, A0). q_subst(Assoc, A, A0):- A=..[F|As], maplist(q_subst(Assoc), As, Bs), A0 =..[F|Bs]. % rename_vars(X, Assoc, X0):- ( var(X); atom(X)), !, q_assoc(X, Assoc, X0). rename_vars(some(X, B), Assoc, some(X0, B0)):-!, rename_vars(B, [X-X0|Assoc], B0). rename_vars(all(X, B), Assoc, all(X0, B0)):-!, rename_vars(B, [X-X0|Assoc], B0). rename_vars((A, B), Assoc, (A0, B0)):-!, rename_vars(A, Assoc, A0), rename_vars(B, Assoc, B0). rename_vars((A; B), Assoc, (A0; B0)):-!, rename_vars(A, Assoc, A0), rename_vars(B, Assoc, B0). rename_vars(A, Assoc, A0):- q_subst(Assoc, A, A0). % ?- neg_normal(- (a, b), X). % ?- neg_normal(-(-(X)), Y). % ?- neg_normal(- - -X, Y). % ?- neg_normal(X, Y). % ?- neg_normal(some(X, -(all(A, -(Y)))), U). neg_normal(X, X) :- var(X), !. neg_normal(- X, - X):- var(X), !. neg_normal(- (-X), Z):-!, neg_normal(X, Z). neg_normal(- (X;Y), Z):-!, neg_normal((-X, -Y), Z). neg_normal(- (X,Y), Z):-!, neg_normal((-X; -Y), Z). neg_normal(- (X->Y), Z):-!, neg_normal(- ( -X; Y), Z). neg_normal(- (X=:=Y), Z):-!, neg_normal(- ((X->Y), (Y->X)), Z). neg_normal(- all(X,Y), some(X,A1)):-!, neg_normal(-Y, A1). neg_normal(- some(X,Y), all(X,A1)):-!, neg_normal(-Y, A1). neg_normal(X;Y, A1;A2):-!, neg_normal(X,A1), neg_normal(Y,A2). neg_normal((X,Y), (A1,A2)):-!, neg_normal(X,A1), neg_normal(Y, A2). neg_normal(X=:=Y, Z):-!, neg_normal(((X->Y), (Y->X)), Z). neg_normal(X->Y, Z):-!, neg_normal((-X; Y), Z). neg_normal(all(X, Y), all(X, Z)):-!, neg_normal(Y, Z). neg_normal(some(X, Y), some(X, Z)):-!, neg_normal(Y, Z). neg_normal(X, X). % ?- skolem(some(A, p(A)), [], X). % ?- skolem(some(X, some(A, p(A, X))), [], R). % ?- skolem(all(A, some(X, some(Y, p(A, X, Y)))); all(A1, some(X1, some(Y1, p(A1, X1, Y1)))), [], P). skolem(some(X, B), P, B0):-!, gensym(sk, SK), X =..[SK|P], skolem(B, P, B0). skolem(all(X, B), P, all(X, B0)):-!, skolem(B, [X|P], B0). skolem((X, Y), P, (X0, Y0)):-!, skolem(X, P, X0), skolem(Y, P, Y0). skolem((X; Y), P, (X0; Y0)):-!, skolem(X, P, X0), skolem(Y, P, Y0). skolem(X, _, X). % ?- extern(all(X, some(Y, love(X,Y); love(Y,X))), A), print(A). canonical_op(C, D, Cs, E):- member(M, Cs), memberchk(C, M), member(D, E), memberchk(D, M). % connectives([[(,), (*), (&), and], [(;), + , '|', or], [(\+), (~), not, -], [(->), imply, =>], [<-], [iff, <->, (=:=), <=>, <-->], [every, all, forall], [some, exists, ex] ]). % ?- write((a, b| c,d)). internal_op([(,), (;), (-), ->, =:=, all, some]). % ?- internal_op(and, X). internal_op(C, D):- connectives(Cs), internal_op(E), canonical_op(C, D, Cs, E). % external_op([(,), (;), (-), ->, =:=, all, some]). % ?- external_op((or), X). external_op(C, D):- connectives(Cs), external_op(E), canonical_op(C, D, Cs, E). % ?- intern(some(x, all(y, a(x, y))), R). % ?- intern(some(x, p(x)->q(x)), R). % ?- intern(x=y, R). % ?- intern((a,b), R). % ?- intern(and(a,b), R). % ?- intern(or(a,b), R). % ?- intern(a =:= b, R). % ?- intern(-(a =:= b), R). % ?- negation_normal_form(-(a =:= b), R). % ?- intern(or(a,b), R), extern(R, E). % ?- extern(imply(a,imply(b,c)), R), extern(R, E). intern(X, X):- var(X), !. intern(X->Y, Z):-!, intern((-(X); Y), Z). intern(X=:=Y, Z):-!, intern(((X->Y), (Y->X)), Z). intern(X, Y):- X =..[F|As], internal_op(F, G), !, maplist(intern, As, Bs), Y =..[G|Bs]. intern(X, X). % extern(X, X):- var(X), !. extern(X, Y):- X =..[F|As], external_op(F, G), !, maplist(extern, As, Bs), Y =..[G|Bs]. extern(X, X). ``` ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 10:49pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/164 "2022-02-07T22:49:21Z")
Should be. You seem already know such better different ways. For now, I am satisfied with knowing NNF. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 7, 2022, 11:19pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/166 "2022-02-07T23:19:43Z")
I did use the last one for some other purpose for myself. It is surprising to hear that such simple rewriting is useful. I thought much different wild ways of idea by analogy of equational theory or introducing special engines for quotient algebra. I should stop dreaming illusions now. Thanks. Surely I will try later the hint. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 10, 2022, 4:32am UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/170 "2022-02-10T04:32:16Z")
Giving this url link is only what I can do now, though you may read already. It is Tamura’s paper on linear logic programming, which, I believe, well known but I have not read yet. > **[asc97.pdf](https://tamura70.gitlab.io/papers/pdf/asc97.pdf)** > > 63.66 KB ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 10, 2022, 1:38pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/173 "2022-02-10T13:38:06Z")
> [@anon95304481](#): > > But I guess there are nevertheless some formula classes where upper bounds can be estimated. Interesting. In leanTAP , `VarLim` is most strange parameter for me. Although at first sight, it seemed an ad hoc parameter, but I realized it is crucial. For some pel test (the pel46?), I found VarLim = 44 to pass. I did it by tracing the case with a large VarLim and found it “loops” around 44. I wondered how estimate beforehand in a formal way. According to leanTAP codes, it seems to bound the number on contraction rules for universally quantified formula, though I’m not sure, but impression. I have no way than waiting your research further. I vaguely remember about a proof on the Herbrand theorem, in which a canonical model, interpretation tree, and Koenig’s lemma (countable version of choice axiom ?) are used. Details are not in my memory, but only impression that quite simple and clear. You seem to give warning that things are not so simple. I am looking forward to hear about “mystery” of VarLim. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [February 10, 2022, 5:08pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/176 "2022-02-10T17:08:06Z")
> [@anon95304481](#): > > Now I have obtained a new result, leanTap is not really needed, > leanSeq could also do? I was using negation normal form with leanSeq, > and now leanSeq is also extremly fast. Maybe because of some indexing? Congratulation ! It is always good to hear research progress. [Previous page](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930.md?page=3)