leanTAP , a Prolog prover for Classical Logic

Nice to know
95

I used prenex normal form in a loose way. More worse I don’t know the definition of the nnf yet. Seeing the short codes of leanTAP I took it by guess that nnf is the internal form that leanTAP handle.

Currently, my preprocessor convert to the “nnf” in my sense like this. I am afraid I did a big mistake here, but so far I met no problem.

% ?- negation_normal_form(a; all(x, p(x)), X), numbervars(X).
%@ X =  (a;all(A, p(A))).
% ?- negation_normal_form(a; all(x, some(y, p(x, y))), X), numbervars(X).
%@ X =  (a;all(A, p(A, sk5(A)))).

EDIT. NNF is the smallest set built from literal, all, and, or ?

97

I supposed that nnf is the form built up from literal, and, or, all by the standard induction, and in fact, leanTAP accepts them (generously ? ) including Skolem functions.

% ?- negation_normal_form(-all(x, some(y, p(x)->p(y))), Fml),
% leanTAP(Fml, [], [], [], 5),
% numbervars(Fml).
%@ Fml = all(A,  (p(sk9), -p(A))) .

As an “ancient technologist”, I am confused with your comment, very sorry for that.

99

Is prenex normal form (PNF) is of the form all(x1, all(x2, …, all(xn, F)…)), where F is quantifier free ? If so, a PNF seems almost a set of clauses. Anyway, it is clear that the leanTAP accepts not only PNF but also non PNF. Also I agree in that moving up quantifier is not necessary, but I have no evidence.

101

Yes, I know the famous rules, but my preprocessor ignore them because of simplicity.

[quote=“j4n_bur53, post:100, topic:4930”]
Not at all. It is all/some/all/some at the root.
Introducing Skolemfunctions or Herbrandfunctions comes later.
[/quote

How about some/all/some/all/some at the root. For me there is no reason to reject this form. My preprocessor accepts closed formulas. some(x, all(y, p(y) → (p(x)->p(y)))).

% ?- negation_normal_form(-some(x, all(y, p(y) -> (p(x)->p(y)))), Fml),
% leanTAP(Fml, [], [], [], 5),
% numbervars(Fml).
%@ Fml = all(A,  (p(sk10(A)), p(A), -p(sk10(A)))) ;

I know only LK, but often I feel as if you talked on tableau, which I am not familiar.

103

I believe that prenix normal form is merely where the quantifiers on all variables are explicitly stated… ( Plus all skolems have been deskolemized back )

104

So, some(x, all(y, p(x, y))) is safely prenex normal form. Thank.

105

EDIT.
Yes, each free variable is universally quantified at root in default reading.

108

Sorry, I was in a hurry. BTW do you have a counter example
for my post ? I will appreciate for that.

111

I agree that skolemization may be performed on the fly depending on runtime formula, eg. preserving scope information.

113

Are you talking about preprocessing to “NNF” ? If so, I have nothing to add.

114

You may omit only the outermost universal quants

so for example

% there exists one thing that is worshipped by all men"
some(g, all(m,  man(m) => worship(m, g))) 
% this is skolemized to a constant

verses

% all men worship something
all(m, some(g, man(m) => worship(m, g)))
% this is skolemized to a function taking one universal var

The very safest way is to ensure before converting to NNF that the quantifiers are all present… that why Jens (and everyone else’s, ROK’s, Stickel’s, etc) NNF predicate requires all forms to start from PNF …

I assume this is why @kuniaki.mukai is confirming what PNF is

1 Like
117

Read the code… it is as clear as day

119

Submitting Prenix forms to the nnf convertor will not lengthen it. It will return the same results as long as they have equivalent meanings.

This statement:

is false

122

If the quantifiers are inward, thus accidently duplicated, then Beckert’s nnf (who Jens copied that code from) returns the wrong results.

123

I am afraid for more confusion, but I would like to believe
it is useful for you and readers. It belongs to “ancient technology.”

For every closed formula F, there exists a closed formula G,
such that

  1. G has no existential quantifier.
  2. F and G are model thoretically equivalent:
    a model of F can be extended to that of G.
    a model of G is also a model of F.

I am not sure it is related to “prenex normal form” in this thread,
again I am sorry for possible more confusion. I lost the source, but it is folklore.

125

You already made one

?- nnf((![X]:p(X) => ![Y]:p(Y)), F).
F = (?[_0]: ~p(_0) | p(s1)).
127

I’ll make my point and just leave it at that

What the clause below is meant to do is pick up explicitly quantified universal variables and collects them into the FreeV. This is what allows them to be used in the scope of skolemization.

nnf((?[X]:F),FreeV,(?[X]:NNF),Paths,I,I1) :- !,
    nnf(F,[X|FreeV],NNF,Paths,I,I1).

If a variable is not picked up this way, then when skolemization happens further down, it will miss the universal variable.

This is by design to allow more versatility to how we the nnf/6 predicate.

The reliable way to use nnf/6 is that you dont let any implicit quantification to happen… (thus, you use explicit quantification as what PNF demands) If you are doing implicit quantification, you do it at your own peril. PNF doesn’t mean quantifiers are merely moved outward… (It can mean that, but not all always) But what it does mean is that the quantifiers are vetted to be as outward as legally required in order to not change ethe meaning of the sentence. We do this in order to ensure that skolem function that nnf creates contains all the required universals that are needed within the scope of the existential.

130

You dont get past it … You want FreeV to to change to [X|FreeV] … this is what passes X into the scope to be used later.

133

take the formatully …

all(M,
  exists(H, 
     man(M)=> heart(H) & has(H,M)))

We want M as part of sk666/1

heart( sk666(M)):- man(M).
has(M, sk666(M)):- man(M).

So that if we have 10 men in the database we will yield 10 hearts from the database

135

It depends… if you go with

And the H is missing from the construction… then it would be wrong