now omit the PNF-ification and see if it still works
nnf(~ (man(M) => ?[H]:(heart(H) & has(H,M))), F).
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).
I see. Sorry I guess it was @fuchs that is converting
English->DRS->FOL->Prolog
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
You are welcom.
seems interesting. I bite a little bit DRS (Hans Kamp?). It sounds it is making constant progress.
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
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.
% ?- 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)))))).
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.
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.
- literals are NNF. ex. like(a, b), -like(a, b)
- if A, B are literal then (A, B) and ( A; B) are NNF
- if A is NNF and x is a variable then all(x, A) and some(x, A) are NNF.
- 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
- (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)
Thanks, but I also said.
“- (like(a, b) ; like(b, a))” is not NNF.
“-” is negation operater here.
Thank you again. Now I am pretty sure that my tentative definition is exactly match.
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.
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
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.
% ?- 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).
Should be. You seem already know such better different ways. For now, I am satisfied with knowing NNF.
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.
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.
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.
Congratulation ! It is always good to hear research progress.