# leanTAP , a Prolog prover for Classical Logic

**URL:** <https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930>\
**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:** 20\
**Page:** 3

<div class="post-metadata">

**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, 1:58pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/99 "2022-02-07T13:58:26Z")

</div>

> [@anon95304481](#):
>
> prenex normal form

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.

---

<div class="post-metadata">

**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, 2:15pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/101 "2022-02-07T14:15:00Z")

</div>

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

> Not at all. It is all/some/all/some at the root.  
> Introducing Skolemfunctions or Herbrandfunctions comes later.

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)))).

```prolog
% ?- 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.

---

<div class="post-metadata">

**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, 2:18pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/103 "2022-02-07T14:18:01Z")

</div>

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

---

<div class="post-metadata">

**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, 2:20pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/104 "2022-02-07T14:20:39Z")

</div>

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

---

<div class="post-metadata">

**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, 2:23pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/105 "2022-02-07T14:23:35Z")

</div>

> [@anon95304481](#):
>
> Its very simple “all quantifiers pushed out”.

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

---

<div class="post-metadata">

**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, 2:31pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/108 "2022-02-07T14:31:20Z")

</div>

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

---

<div class="post-metadata">

**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, 2:40pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/111 "2022-02-07T14:40:10Z")

</div>

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

---

<div class="post-metadata">

**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, 2:44pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/113 "2022-02-07T14:44:46Z")

</div>

> [@anon95304481](#):
>
> Its not performed on the fly, during LK proof seach.  
> nnf\_pure.pl is a preprocessing step. Whats wrong with you?

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

---

<div class="post-metadata">

**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, 2:45pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/114 "2022-02-07T14:45:25Z")

</div>

You may omit only the outermost universal quants

so for example

```prolog
% 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

```prolog
% 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

---

<div class="post-metadata">

**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, 2:59pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/117 "2022-02-07T14:59:25Z")

</div>

Read the code… it is as clear as day

---

<div class="post-metadata">

**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, 3:14pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/119 "2022-02-07T15:14:01Z")

</div>

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:

> [@anon95304481](#):
>
> With structural Herbrandization and no Prenex you  
> can get shorter Herbandfunctions

is false

---

<div class="post-metadata">

**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, 3:20pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/122 "2022-02-07T15:20:53Z")

</div>

> [@logicmoo](#):
>
> NNF predicate _requires all_ forms to start from PNF

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

---

<div class="post-metadata">

**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, 3:22pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/123 "2022-02-07T15:22:00Z")

</div>

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.

---

<div class="post-metadata">

**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, 3:35pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/125 "2022-02-07T15:35:35Z")

</div>

> [@anon95304481](#):
>
> Not at all. Can you make an example?

You already made one

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

```

---

<div class="post-metadata">

**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, 3:59pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/127 "2022-02-07T15:59:07Z")

</div>

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.

```prolog
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.

---

<div class="post-metadata">

**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, 4:15pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/130 "2022-02-07T16:15:50Z")

</div>

> [@anon95304481](#):
>
> How do you want to get past `(?[X]:F)` without changing ` FreeV` to `[X|FreeV]` ?  
> There is no clause that allows that.

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.

---

<div class="post-metadata">

**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, 4:41pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/133 "2022-02-07T16:41:44Z")

</div>

take the formatully …

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

```

We want `M` as part of `sk666/1`

```prolog
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

---

<div class="post-metadata">

**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, 4:45pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/135 "2022-02-07T16:45:41Z")

</div>

It depends… if you go with

> [@logicmoo](#):
>
> ```prolog
> exists(H, 
> man(M)=> heart(H) & has(H,M))
> 
> ```

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

---

<div class="post-metadata">

**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, 4:48pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/137 "2022-02-07T16:48:31Z")

</div>

> [@anon95304481](#):
>
> ` nnf(~ ![M]:(man(M) => ?[H]:(heart(H) & has(H,M))), F).`

now omit the PNF-ification and see if it still works

` nnf(~ (man(M) => ?[H]:(heart(H) & has(H,M))), F).`

---

<div class="post-metadata">

**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:02pm UTC](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930/140 "2022-02-07T17:02:41Z")

</div>

> [@anon95304481](#):
>
> It is more made or leanTap and not for Prolog.

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.

[Previous page](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930.md?page=2)

[Next page](https://swi-prolog.discourse.group/t/leantap-a-prolog-prover-for-classical-logic/4930.md?page=4)