old theorem provers dont die, you just wish they did

[R Kym Horsell]

Looking at this real dusty deck code from David Plaisted 1987.

In this TP horn clauses are written in what looks like Prolog
and the prover interprets them.

The comments are the bottom of the code seem to have little relationship
with what the TP spits out whenever I ran it.

It says 500 cpu sec 1128 TP inferences in ~1987.

The output from the run "now" gets 40782 inferences but only 19 sec cpu.

It might be my fault because I can never help tinkering with code
and I dont always write comments to let myself know I did it.

I have the source for the hacked TP somewhere but -- again -- it's
badly hacked over the past few decades so you'd be taking your life
in your hands to even look at it.

"Original" setup for the IVT:
*************************************************************************
% The intermediate value theorem: If f(a) =< 0 and f(b) >= 0 and
% a =< b and f is continuous then there exists a value X such that
% f(X) = 0. Here p(X,Y) means X =< Y. Also, l is the least
% upper bound of {X : X =< b, f(X) =< 0}.

p(a, b).
p(f(a), 0).
p(0, f(b)).

p(l, X) :-. ((p(g(X), X) :- p(g(X), b)) :- p(f(g(X)), 0)).
% p(l, X) :- not(p(g(X), b)).
% p(l, X) :- not(p(f(g(X)), 0)).
% p(l, X) :- p(g(X), X).

p(g(X), b) :- not(p(l, X)).
p(f(g(X)), 0) :- not(p(l, X)).
not(p(g(X), X)) :- not(p(l, X)).

p(X, l) :- and([p(X, b), p(f(X), 0)]).

not(p(f(X), 0)) :- and([p(X, b), not(p(X, l))]).

% not(p(X, b)) :- not(p(X, l)), p(f(X), 0).

not(p(k(k(X)), X)) :- smallf(X).
not(p(X, h(h(X)))) :- largef(X).

% p(0, f(X)) :- and([p(k(k(X)), X), inrange(X)]).
% p(f(X), 0) :- and([p(X, h(h(X))), inrange(X)]).

p(0, f(X)) :- and([inrange(X), p(k(k(X)), X)]).
p(f(X), 0) :- and([inrange(X), p(X, h(h(X)))]).

p(f(X), 0) :- and([inrange(X), hrange(X,Y), p(f(Y), 0)]).

p(0, f(X)) :- and([inrange(X), krange(X,Y), p(0, f(Y))]).

not(p(f(Y), 0)) :- and([largef(X), hrange(X,Y)]).

not(p(0, f(Y))) :- and([smallf(X), krange(X,Y)]).

inrange(X) :-- and([p(a,X),p(X,b)]).

% smallf(X) :- and([inrange(X),not(p(0, f(X)))]).
% largef(X) :- and([inrange(X),not(p(f(X), 0))]).

% hrange(X,Y) :- and([p(Y, X), not(p(Y, h(h(X))))]).
% krange(X,Y) :- and([p(X, Y), not(p(k(k(X)), Y))]).

smallf(X) :-- and([not(p(0, f(X))),inrange(X)]).
largef(X) :-- and([not(p(f(X), 0)),inrange(X)]).

hrange(X,Y) :-- and([not(p(Y, h(h(X)))),p(Y, X)]).
krange(X,Y) :-- and([not(p(k(k(X)), Y)),p(X, Y)]).

p(Y, h(h(X))) :- and([largef(X), p(Y, X), p(f(Y), 0)]).

p(k(k(X)), Y) :- and([smallf(X), p(X, Y), p(0, f(Y))]).

% p(Y, h(h(X))) :- p(f(Y), 0), not(p(f(X), 0)), p(Y, X), p(a, X), p(X, b).
% p(k(k(X)), Y) :- p(0, f(Y)), not(p(0, f(X))), p(X, Y), p(a, X), p(X, b).

% instructions to the prover to derive facts of a certain form, then fail

small(X) :-- (not(p(f(Y), 0)):- not(p(f(X), 0))), fail.

small(X) :-- (not(p(f(Y), 0)):- not(p(f(X), 0))),
(p(f(Y), 0) :- not(p(f(X), 0))). % the easy part

big(X) :-- (not(p(0, f(Y))):- not(p(0, f(X)))), fail.

big(X) :-- (not(p(0, f(Y))):- not(p(0, f(X)))),
(p(0, f(Y)) :- not(p(0, f(X)))).

false :-- small(X), fail.

% the theorem

false :-- small(X), big(X).

and([X|Y]) :-- X, and(Y).
and([]).

p(X, X).

% transposes of transitivity axiom

p(X, Z) :- prolog(var(X)), p(Y, Z), p(X, Y).
p(X, Z) :- prolog(nonvar(X)), p(X, Y), p(Y, Z).

% not(p(X,Y)) :- p(Y, Z), not(p(X, Z)).
% not(p(Y, Z)) :- p(X, Y), not(p(X, Z)).

p(X, Y) :- not(p(Y, X)).

% denseness of the reals
% use contrapositives for these axioms

not(p(X, q(q(Y, X)))) :- not(p(X, Y)).
not(p(q(q(X, Y)), X)) :- not(p(Y, X)).

% p(X, Y) :- p(X, q(q(Y, X))).
% p(Y, X) :- p(q(q(X, Y)), X).

% Proved Dec. 30 1986 size 5 312 seconds 1128 inferences with flags as
% follows:

%:- assert(b_only),
% proof_trace,
% assert(nosplits), assert(nosave(and(_))),
% assert(nosize),
% assert(maxsize),
% try(imv).

% and big_subgoal modified as follows:

% big_subgoal((L :- B), SIZE) :-
% \+ top_connective(L),
% ( (length(B,Len), Len > 3) ;
% (flatsize2(L,FS), FS > 11) ;
% (member(X,B), flatsize(X,FX),
% FX > 11)), !.

% newly_solved(0,id(1),(false:-[]))

% proof found
% false:-lemma((small(l):-[])),(big(l):-
% lemma((not p(0,f(q(q(l,k(k(l)))))):-[not p(0,f(l))])),
% (p(0,f(q(q(l,k(k(l)))))):-
% (not p(f(q(q(l,k(k(l))))),0):-
% (and([p(q(q(l,k(k(l)))),b),not p(q(q(l,k(k(l)))),l)]):-
% lemma((p(q(q(l,k(k(l)))),b):-[not p(0,f(l))])),
% (and([not p(q(q(l,k(k(l)))),l)]):-
% lemma((not p(q(q(l,k(k(l)))),l):-[not p(0,f(l))])),and([]))))))
% size of proof 5

% 311.633 cpu seconds used
% 1128 inferences done

% proved later in 285 seconds, size 5, 1128 inferences after a
% minor bug was fixed

% The current version of the prover requires proof_size_multiplier(0)
% and solution_size_multiplier(0.125) to get this one and even then
% takes over 500 seconds for some reason

% New Examples for C Prolog Theorem Prover
% Note -- some times and number of inferences may differ
% Each example must be in a separate file

% Dave Plaisted
% University of North Carolina at Chapel Hill
% April 29, 1987
*************************************************************************

And now running it using whatever old version of SWI on likely long-dead
underpowered x86 I had at the time:
*************************************************************************
For a trace of the proof type proof_trace.
To turn this off, type proof_untrace.
t25
p(a, b)
p(f(a), 0)
p(0, f(b))
p(l, _G180):-. ((p(g(_G180), _G180):-p(g(_G180), b)):-p(f(g(_G180)), 0))
p(g(_G304), b):-not(p(l, _G304))
p(f(g(_G427)), 0):-not(p(l, _G427))
not(p(g(_G566), _G566)):-not(p(l, _G566))
p(_G717, l):-and([p(_G717, b), p(f(_G717), 0)])
not(p(f(_G835), 0)):-and([p(_G835, b), not(p(_G835, l))])
not(p(k(k(_G985)), _G985)):-smallf(_G985)
not(p(_G1149, h(h(_G1149)))):-largef(_G1149)
p(0, f(_G1313)):-and([inrange(_G1313), p(k(k(_G1313)), _G1313)])
p(f(_G1448), 0):-and([inrange(_G1448), p(_G1448, h(h(_G1448)))])
p(f(_G1583), 0):-and([inrange(_G1583), hrange(_G1583, _G1594), p(f(_G1594), 0)])
p(0, f(_G1722)):-and([inrange(_G1722), krange(_G1722, _G1733), p(0, f(_G1733))])
not(p(f(_G1861), 0)):-and([largef(_G1868), hrange(_G1868, _G1861)])
not(p(0, f(_G2008))):-and([smallf(_G2015), krange(_G2015, _G2008)])
inrange(_G2155):--and([p(a, _G2155), p(_G2155, b)])
smallf(_G2239):--and([not(p(0, f(_G2239))), inrange(_G2239)])
largef(_G2326):--and([not(p(f(_G2326), 0)), inrange(_G2326)])
hrange(_G2413, _G2414):--and([not(p(_G2414, h(h(_G2413)))), p(_G2414, _G2413)])
krange(_G2517, _G2518):--and([not(p(k(k(_G2517)), _G2518)), p(_G2517, _G2518)])
p(_G2625, h(h(_G2621))):-and([largef(_G2621), p(_G2625, _G2621), p(f(_G2625), 0)])
p(k(k(_G2776)), _G2781):-and([smallf(_G2776), p(_G2776, _G2781), p(0, f(_G2781))])
small(_G2931):-- (not(p(f(_G2933), 0)):-not(p(f(_G2931), 0))), fail
small(_G3045):-- (not(p(f(_G3047), 0)):-not(p(f(_G3045), 0))), (p(f(_G3047), 0):-not(p(f(_G3045), 0)))
big(_G3174):-- (not(p(0, f(_G3176))):-not(p(0, f(_G3174)))), fail
big(_G3288):-- (not(p(0, f(_G3290))):-not(p(0, f(_G3288)))), (p(0, f(_G3290)):-not(p(0, f(_G3288))))
false:--small(_G3417), fail
false:--small(_G3507), big(_G3507)
and([_G3599|_G3600]):--_G3599, and(_G3600)
and([])
p(_G3780, _G3780)
p(_G3903, _G3904):-prolog(var(_G3903)), p(_G3910, _G3904), p(_G3903, _G3910)
p(_G4056, _G4057):-prolog(nonvar(_G4056)), p(_G4056, _G4064), p(_G4064, _G4057)
p(_G4209, _G4210):-not(p(_G4210, _G4209))
not(p(_G4317, q(q(_G4316, _G4317)))):-not(p(_G4317, _G4316))
not(p(q(q(_G4497, _G4498)), _G4497)):-not(p(_G4498, _G4497))

nosave(and(_G4732)) is asserted
b_only is asserted
nosize is asserted
maxsize is asserted
nosplits is asserted
solution_size_mult(0.1) is asserted
proof_size_mult(0.4) is asserted
.
.
.
.
proof found
false:-lemma((small(l):-[])), (big(l):-assume(not(p(0, f(l))), lemma((not(p(0, f(h(h(k(k(l))))))):-[not(p(0, f(l)))]))), assume(not(p(0, f(l))), lemma((p(0, f(h(h(k(k(l)))))):-[not(p(0, f(l)))]))))
size of proof 11

19.82 cpu seconds used
40782 inferences done
*************************************************************************

--
[No Lockdown States:]
A handful of US states -- Arkansas, Iowa, Nebraska, North
Dakota, and South Dakota -- presently have no lock-down rules.
The doubling time for active cases of covid19 is observably faster
in the nolockdown states than for those that do have a lock-down.

State Doubling time for #active cases (days)
nolockdown 5.00
California 5.89
New.Jersey 5.90
New.York 5.94
Texas 6.64

Comparison of doubling times:
Starting with 100 active cases each doubling rate produces:
day NoLockdown Cal NJ NY TX
10 399.99 324.40 323.75 321.20 284.02
20 1599.99 1052.38 1048.19 1031.73 806.70
30 6399.99 3413.97 3393.60 3314.00 2291.26
40 25599.99 11075.06 10987.05 10644.81 6507.79
50 102399.99 35927.98 35571.45 34191.84 18483.83
60 409599.99 116551.93 115165.39 109826.47 52498.94
^ ~4x Cal,NJ,NY
~8x TX

[j4n bur53]

It begs the question whether resolution theorem
proving can be useful where terms need to be invented.
You can try a more simpler example, for example

try proving Cantors theorem:

A proper subset P(A)

A proof would need to invent diagonalization. But
since resolution theorem proving doesn't know
anything about set theory, you need

set theory formalized as well. And these axiom
must drive the search process for the term to
be invented. I dont know how Plaisted was

supposed to prove the IMT, was the invented
term {X : X =< b, f(X) =< 0} given? Modern
proof assistants like Isabello/HOL, Coq, etc..

are that successful because they are hybrid
between automated theorem and manual theorem
proving. The underlying semi-automation can

be somehow modelled by a human oracle. Also often
they replace set theory by higher order logic,
which better in inventing term. Solving the

problem of an infinite search space for the
term to be invented by better and interactive
tools. But why I am interested in monadic first

order logic is the fact that with some modding
of the resolution theorem prover this search space
seems to be nevertheless bounded, from case to

case finite. I guess IMT cannot be formalized in
monadic first order logic. But some things from
semantic web would be approachable, like

description logic, where Olcotts bachelor example
might also fall in.

R Kym Horsell schrieb:

[R Kym Horsell]

j4n bur53 <janb...@fastmail.fm> wrote:
> It begs the question whether resolution theorem
> proving can be useful where terms need to be invented.
> You can try a more simpler example, for example
>
> try proving Cantors theorem:
>
> A proper subset P(A)
>
> A proof would need to invent diagonalization. But
> since resolution theorem proving doesn't know
> anything about set theory, you need

...

There are an infinite number of proofs and "half" of them
do it another way.

With my skeptical hat on --
there is nothing much to "creativity" but generate and test.

Sure, a human brain may be able to do quantum computing or
some of its trickier variations that can solve at least some undeciable
problems but it seems unlikely anything more than trial and error is needed.

[Mostowski Collapse]

> there is nothing much to "creativity" but generate and test.

Well there is, unification. There is also
partially higher order unification and
other kinds of unification.

Resolution theorem proving already deploys
term unification. But how about other types
of unification?

CLP(*) has also a unfication aspect.

[Mostowski Collapse]

And then there is even more, like QE,
quantifier elimination, which somehow
also invents terms.

[Mostowski Collapse]

I would like to understand this prover,
it seems its kind of Prolog with tabling:

Optimizing Proof Search in Model Elimination
John Harrison
Publication: CADE-13: Proceedings of the 13th International Conference on
Automated Deduction: Automated DeductionAugust 1996 Pages 313–327
https://www.cl.cam.ac.uk/~jrh13/papers/me.html

It is supposed to be the same approach as
Isabelle/HOLs "meson" proof strategy. It was
used to prove a couple of things in Aristoteles

term logic here:

Aristotle's Assertoric Syllogistic
Angeliki Koutsoukou-Argyraki - 2019-10-08
https://www.isa-afp.org/entries/Aristotles_Assertoric_Syllogistic.html

But maybe, since we only prove things and
dont disprove things, an ordinary resolution
theorem prover would also do.

Damned, why was I blinded by finite model property?

[Mostowski Collapse]

The link:
https://www.cl.cam.ac.uk/~jrh13/papers/me.html

Features a good old postscript file. Here
on a mac you can just double click it, to
open it. The theorem prover is

described as after Stickel after Pleisted.

[R Kym Horsell]

Mostowski Collapse <burs...@gmail.com> wrote:
> I would like to understand this prover,
> it seems its kind of Prolog with tabling:
>
> Optimizing Proof Search in Model Elimination
> John Harrison
> Publication: CADE-13: Proceedings of the 13th International Conference on

> Automated Deduction: Automated DeductionAugust 1996 Pages 313-327

> https://www.cl.cam.ac.uk/~jrh13/papers/me.html
>
> It is supposed to be the same approach as
> Isabelle/HOLs "meson" proof strategy. It was
> used to prove a couple of things in Aristoteles
>
> term logic here:
>
> Aristotle's Assertoric Syllogistic
> Angeliki Koutsoukou-Argyraki - 2019-10-08
> https://www.isa-afp.org/entries/Aristotles_Assertoric_Syllogistic.html
>
> But maybe, since we only prove things and
> dont disprove things, an ordinary resolution
> theorem prover would also do.
>
> Damned, why was I blinded by finite model property?

...

Maybe gut instinct. :)

Finite models/countermodels are easy to easy to find and easy to
explain to the customer.

An super intelligent solution that incrementally achieves all the goals
in parallel may take 1 step less than the dumb solution but you will
never be able to explain it to the average director so you will not be paid.

Obviously Darwin takes over at this point.

[Mostowski Collapse]

My current director is Mr. Corona:

The Secret of the Dancing
https://www.youtube.com/watch?v=CgcAx0Tef3g

He approves on anything I am doing.

But finite model property, in the case
of monadic first order logic, would come
into play if we disprove something:

"If L is finitely axiomatizable (and has a
recursive set of recursive rules) and has
the finite model property, then it is decidable."

But we wouldn't need it to prove something.
Since resolution theorem proving is complete,
and if |- A, then resolution theorem proving

should find it. Aristotle's Assertoric
Syllogistic document contains only demonstrations
of |- A, no demonstration of |/- A.

[Mostowski Collapse]

Without finite model property or some
other property, the sublogic of FOL
would be only semi-decidabke.

[Mostowski Collapse]

The rabbits plague in australia is quite
interesting. And one virus used is characterized:

"Myxoma virus has multiple methods
that it utilizes to evade the immune system."
https://en.wikipedia.org/wiki/Myxoma_virus

SARS-Cov-2 is said to utilize some
modulation of the innate immune system.

Am Sonntag, 19. April 2020 16:27:15 UTC+2 schrieb Kym Horsell:

[R Kym Horsell]

Mostowski Collapse <burs...@gmail.com> wrote:
> The rabbits plague in australia is quite
> interesting. And one virus used is characterized:
>
> "Myxoma virus has multiple methods
> that it utilizes to evade the immune system."
> https://en.wikipedia.org/wiki/Myxoma_virus

Calicivirus (RHDV) was intro'd in 1996.
They also used to mixture of Calici and Myxo for a while.
In 2017 the K5 variant was intro'd.

Each time the rabbit virus changes it seems domestic cats are
also affected. Owners are supposed to get their pet
vaccinated against Calici each year because immunity doesnt last.

There is some evidence that SARS2 may also have such a problem,
at least with some people. If so, it is likely to be an
annual thing and the idea of "immunity certificates"
to get people back to work if they have antibodies at some point
will have a definite lifetime.

> SARS-Cov-2 is said to utilize some
> modulation of the innate immune system.

...

The nastier viruses get to play the lymphocytes like puppets.
Covid19 and flu in some people becomes a problem because they can
cause a very large immune response ("cytokine storms")
that does more harm to the patient than good.

Viruses can also mostly escape the immune system by hiding
in the brain or spine and HIV can hide inside the immune system
itself (inside certain T-cells). Which means the virus can't be
cleared. People can have the antibodies and the virus as well.

Which is why some people are interested in developing a treatment
for coronaviruses -- an "antibiotic for viruses" -- rather than a
fire-and-forget vaccine which has been tricky up to this point
to obtain anyway.

[Mostowski Collapse]

The innate immune system is intra cellular.
For antibodies to be produced the humoral

immune system must get active. But if COVID-19
shows antibodies only after 10 days, and

the lung fails after 9 days. Well, well, ...

[R Kym Horsell]

Mostowski Collapse <burs...@gmail.com> wrote:
> The innate immune system is intra cellular.

This was the long-held belief. But it's been discovered
recently (2019 I think) some immune activity can
target virus inside some cells.

> For antibodies to be produced the humoral
> immune system must get active. But if COVID-19
> shows antibodies only after 10 days, and
> the lung fails after 9 days. Well, well, ...

...

[Mostowski Collapse]

Well I mixed up two dimensions. The
ortogonale dimensions are:

innate/adaptive

cellular/humoral

The innate immune system and the adaptive immune
system each comprise both humoral and cell-mediated
components.
https://en.wikipedia.org/wiki/Cell-mediated_immunity

There are SARS-Cov-1 studies that say

modulation of the innate immune system

happens. See also:

Mechanisms of Severe Acute Respiratory Syndrome
Pathogenesis and Innate Immunomodulation
Microbiol Mol Biol Rev. 2008 Dec; 72(4): 672–685.
https://www.ncbi.nlm.nih.gov/pmc/articles/PMC2593566/

Maybe this also applies to SARS-Cov-2.

[Mostowski Collapse]

Here are lists of ongoing research:

Impfstoffe zum Schutz vor Covid-19, der neuen Coronavirus-Infektion
- 13. April 2020
https://www.vfa.de/de/arzneimittel-forschung/woran-wir-forschen/impfstoffe-zum-schutz-vor-coronavirus-2019-ncov

DRAFT landscape of COVID-19 candidate vaccines
- 20 March 2020
https://www.who.int/blueprint/priority-diseases/key-action/novel-coronavirus-landscape-ncov.pdf

[Mostowski Collapse]

In these notes, some propositonal provers are burried:

Computational Logic Notes
http://www.barrywatson.se/cl/

How about a prover that can also do FOL?

[Mostowski Collapse]

Do I need to combine skolemization with something?
But resolution says propositional only?

[R Kym Horsell]

Mostowski Collapse <burs...@gmail.com> wrote:
> Do I need to combine skolemization with something?

Didnt your dealer tell you nebba nebba nebba mix your drugs? ;)
In the old tree methods you dont *need* Skolem.

[Mostowski Collapse]

The usual resultion theorem proving need skolemization,
there is a section about skolemization:

Skolem Form
All of the existential quantifiers in the
PNF are replaced by Skolem functions.
http://www.barrywatson.se/cl/cl_skolem_form.html

But the his resolution is only propositional,

Resolution (propositional)
Resolution is a single rule refutation technique for
deciding the satisfiability of propositional formulas
in clausal form.
http://www.barrywatson.se/cl/cl_resolution_propositional.html

Its also a similarly inefficient search for
a new resolvent like in Markus Triskas code,
at least this could be replaced by something

more realistic and non-naive. A little resolution
search engine that has then plugable search strategies
should be able to demonstrate:
- unit resolution
- input resolution

[Mostowski Collapse]

input resolution could then be used to show
what Prolog ows to resolution theorem proving,
where it comes from.

Didn't write Bob Kowalski a book about
all that, which is a classic?

Chapter 8.
The Connection Graph Proof Procedure
Logic for Problem Solving - 1979
https://www.researchgate.net/publication/277669992

[Mostowski Collapse]

Oh, there is a revisited version. Probably
the original with an appendix paper:

Logic for Problem Solving, Revisited (Englisch)
Taschenbuch – 18. November 2014
von Thom Frühwirth (Herausgeber), Robert Kowalski (Autor)
https://www.amazon.de/Logic-Problem-Solving-Revisited-Fr%C3%BChwirth/dp/3837036294

But where is an accompanying code repository?
Maybe I am too stupid to find it. But anyhow,
what are these guys thinking, a book and

no advertising of a code repository?
Thats not modern.

[R Kym Horsell]

Mostowski Collapse <burs...@gmail.com> wrote:
> Oh, there is a revisited version. Probably
> the original with an appendix paper:
>
> Logic for Problem Solving, Revisited (Englisch)

> Taschenbuch - 18. November 2014
> von Thom Fr"uhwirth (Herausgeber), Robert Kowalski (Autor)

> https://www.amazon.de/Logic-Problem-Solving-Revisited-Fr%C3%BChwirth/dp/3837036294
>
> But where is an accompanying code repository?
> Maybe I am too stupid to find it. But anyhow,
> what are these guys thinking, a book and
>
> no advertising of a code repository?
> Thats not modern.

github is modern.

<https://github.com/search?l=Prolog&q=theorem+prover&type=Repositories>

[Mostowski Collapse]

There are like 22 hits.

And which one is a resolution
theorem prover for FOL?

[Mostowski Collapse]

New player in town:

OpenAI takes metamath to a next level - Polu, 2020
https://cdn.openai.com/openai_proof_assistant_tutorial.pdf