Its a pitty that there is no simple leanTap=, i.e. leanTap= with
equality. My take is only a few lines, splitting (subst) into (subst1)
and (subst2) and can run in the browser.

On the other hand I read:

The completion-based method for mixed E-unification we
have described, has been implemented as part of the
tableau-based theorem prover 3TAP [3]. The implementation
consists of about 2500 lines of code, written in Quintus Prolog.
Besides the possibility to prove theorems from predicate logic
with equality, the E-unification module can be used “stand alone”
to solve simultaneous mixed E-unification problems.
https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf

I don’t know how to run 2500 lines of code in the browser.
And I don’t need some first order equality that would even
deploy some term order, as is popular in certain term

rewriting and Knuth Bendix. One interesting test case is this
one, that works in the browser:

?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\
f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
% Wall 60 ms, gc 0 ms, 1171000 lips

Thanks to McCarthys trick its quite fast. On monday it still took
me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
tool can do the same, but interestingly he gets a longer proof with

more (subst) applications. See also this ticket:

Does the tree tool search shortest proofs? #11
https://github.com/wo/tpg/issues/11

Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1:
> I did the barber paradox always wrong!
> The biconditional makes it so much easier.
>
> 1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
> 2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
> 3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
> 4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
> 5. ¬¬s(a, a) (F∧2 4)
> 6. ¬s(a, a) (F∧1 4)
> 7. s(a, a) (F¬ 5)
> ✓ (ax 6, 7)
> 4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
> 5. ¬s(a, a) (T∨2 4)
> 6. s(a, a) (T∨1 4)
> ✓ (ax 5, 6)
>
> See also:
>
> Biconditional Support for Maslovs Method
> https://twitter.com/dogelogch/status/1483455561031106563
>
> Biconditional Support for Maslovs Method
> https://www.facebook.com/groups/dogelog

See also my blog post on medium.com:

McCarthys Trick for First Order Equality
https://twitter.com/dogelogch/status/1484032442717585409

McCarthys Trick for First Order Equality
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:03:24 UTC+1:
> Its a pitty that there is no simple leanTap=, i.e. leanTap= with
> equality. My take is only a few lines, splitting (subst) into (subst1)
> and (subst2) and can run in the browser.
>
> On the other hand I read:
>
> The completion-based method for mixed E-unification we
> have described, has been implemented as part of the
> tableau-based theorem prover 3TAP [3]. The implementation
> consists of about 2500 lines of code, written in Quintus Prolog.
> Besides the possibility to prove theorems from predicate logic
> with equality, the E-unification module can be used “stand alone”
> to solve simultaneous mixed E-unification problems.
> https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf
>
> I don’t know how to run 2500 lines of code in the browser.
> And I don’t need some first order equality that would even
> deploy some term order, as is popular in certain term
>
> rewriting and Knuth Bendix. One interesting test case is this
> one, that works in the browser:
>
> ?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\
> f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
> % Wall 60 ms, gc 0 ms, 1171000 lips
>
> Thanks to McCarthys trick its quite fast. On monday it still took
> me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
> tool can do the same, but interestingly he gets a longer proof with
>
> more (subst) applications. See also this ticket:
>
> Does the tree tool search shortest proofs? #11
> https://github.com/wo/tpg/issues/11
> Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1:
> > I did the barber paradox always wrong!
> > The biconditional makes it so much easier.
> >
> > 1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
> > 2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
> > 3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
> > 4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
> > 5. ¬¬s(a, a) (F∧2 4)
> > 6. ¬s(a, a) (F∧1 4)
> > 7. s(a, a) (F¬ 5)
> > ✓ (ax 6, 7)
> > 4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
> > 5. ¬s(a, a) (T∨2 4)
> > 6. s(a, a) (T∨1 4)
> > ✓ (ax 5, 6)
> >
> > See also:
> >
> > Biconditional Support for Maslovs Method
> > https://twitter.com/dogelogch/status/1483455561031106563
> >
> > Biconditional Support for Maslovs Method
> > https://www.facebook.com/groups/dogelog

Here is a poket McCarthy for propositional logic only.
It can also do Joseph Vidal-Rossets antisequent (asq):

:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional

prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).

prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).

prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.

/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).

provable(F,P):-
prove([]>[F],P).

member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).

Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:06:05 UTC+1:
> See also my blog post on medium.com:
>
> McCarthys Trick for First Order Equality
> https://twitter.com/dogelogch/status/1484032442717585409
>
> McCarthys Trick for First Order Equality
> https://www.facebook.com/groups/dogelog

Why does Jens Otten automatic reordering preprocessing
give some bang? Now I get for Pelletier problem 71:

/* Joseph Vidal-Rossets LeanSeq, from his web site */
?- test.
% 54,202,362 inferences, 4.969 CPU in 5.017 seconds
(99% CPU, 10908954 Lips)
true.
https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html

/* My McCarthy */
?- test2.
% 8,814,592 inferences, 1.099 CPU in 1.123 seconds
(98% CPU, 8019776 Lips)
true.

I think this is because rbicond is more symmetric,
in my new McCarthy it is now:

prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).

On the other hand Joseph Vidal-Rossets LeanSeq
has the following rbicond rule:

prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).

But this works only for Pelletier problem 71.
The rule is still quite static, and doesn't

do any reordering.

Mostowski Collapse schrieb:
> Here is a poket McCarthy for propositional logic only.
> It can also do Joseph Vidal-Rossets antisequent (asq):
>
> :- op( 500, fy, ~). % negation
> :- op(1000, xfy, &). % conjunction
> :- op(1100, xfy, '|'). % disjunction
> :- op(1110, xfy, =>). % conditional
> :- op(1120, xfy, <=>). % biconditional
>
> prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
> prove(G>[~A,B|D],P).
> prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
> prove(G>[A,B|D],P).
> /* double negation */
> prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
> prove(G>[A|D],P).
> prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
> prove(G>[~A,~B|D],P).
>
> prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
> prove(G>[~A,B|D],P1),
> prove(G>[A,~B|D], P2).
> prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
> prove(G>[~A,~B|D],P1),
> prove(G>[A,B|D],P2).
> prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
> prove(G>[A|D],P1),
> prove(G>[~B|D],P2).
> prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
> prove(G>[A|D],P1),
> prove(G>[B|D],P2).
> prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
> prove(G>[~A|D],P1),
> prove(G>[~B|D],P2).
>
> prove(G>[A|D], ax(G>[A|D], A)):-
> member(B,G), A==B, !.
>
> /* next */
> prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
> prove([A|G]>D,P).
> prove(G>[A|D], lneg(G>[A|D], P)) :- !,
> prove([~A|G]>D,P).
> prove(G>[], asq(G>[], asq)).
>
> provable(F,P):-
> prove([]>[F],P).
>
> member(E, [E|_]).
> member(E, [_|Xs]) :-
> member(E, Xs).

There is a bug in nff_pure.pl by Jens Otten. This here:

Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,

Should read, so that it runs in a wider variety of Prolog systems:

Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,

And we can now try Pelletier problem 71, and it doesn’t work:

% 88,652,639 inferences, 13.734 CPU in 13.999 seconds
(98% CPU, 6454800 Lips)
ERROR: Stack limit (1.0Gb) exceeded

Strange...

Mostowski Collapse schrieb:
> Why does Jens Otten automatic reordering preprocessing
> give some bang? Now I get for Pelletier problem 71:
>
> /* Joseph Vidal-Rossets LeanSeq, from his web site */
> ?- test.
> % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
> (99% CPU, 10908954 Lips)
> true.
> https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
>
>
> /* My McCarthy */
> ?- test2.
> % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
> (98% CPU, 8019776 Lips)
> true.
>
> I think this is because rbicond is more symmetric,
> in my new McCarthy it is now:
>
> prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
>         prove(G>[~A,B|D],P1),
>         prove(G>[A,~B|D], P2).
>
> On the other hand Joseph Vidal-Rossets LeanSeq
> has the following rbicond rule:
>
> prove(G>D, rbicond(G>D,P1,P2)):-
>         select((A<=>B),D,D1),!,
>         prove([A|G]>[B|D1],P1),
>         prove([B|G]>[A|D1], P2).
>
> But this works only for Pelletier problem 71.
> The rule is still quite static, and doesn't
>
> do any reordering.
>
> Mostowski Collapse schrieb:
>> Here is a poket McCarthy for propositional logic only.
>> It can also do Joseph Vidal-Rossets antisequent (asq):
>> :- op( 500, fy, ~).     % negation
>> :- op(1000, xfy, &).    % conjunction
>> :- op(1100, xfy, '|').  % disjunction
>> :- op(1110, xfy, =>).   % conditional
>> :- op(1120, xfy, <=>).  % biconditional
>>
>> prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
>>         prove(G>[~A,B|D],P).
>> prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
>>         prove(G>[A,B|D],P).
>> /* double negation */
>> prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
>>         prove(G>[A|D],P).
>> prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
>>         prove(G>[~A,~B|D],P).
>>
>> prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
>>         prove(G>[~A,B|D],P1),
>>         prove(G>[A,~B|D], P2).
>> prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
>>         prove(G>[~A,~B|D],P1),
>>         prove(G>[A,B|D],P2).
>> prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
>>         prove(G>[A|D],P1),
>>         prove(G>[~B|D],P2).
>> prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
>>         prove(G>[A|D],P1),
>>         prove(G>[B|D],P2).
>> prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
>>         prove(G>[~A|D],P1),
>>         prove(G>[~B|D],P2).
>>
>> prove(G>[A|D], ax(G>[A|D], A)):-
>>         member(B,G), A==B, !.
>>
>> /* next */
>> prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
>>         prove([A|G]>D,P).
>> prove(G>[A|D], lneg(G>[A|D], P)) :- !,
>>         prove([~A|G]>D,P).
>> prove(G>[], asq(G>[], asq)).
>>
>> provable(F,P):-
>>         prove([]>[F],P).
>>
>> member(E, [E|_]).
>> member(E, [_|Xs]) :-
>>    member(E, Xs).

If I paste my poket McCarthy into Joseph Vidal-Rossets web
page, I can reproduce the example from page 7 of this paper:

leanTAP Revisited
Melvin Fitting - March 13, 1997
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf

Simply use this here:
?- provable(((~p & q) | p), Proof).

The red color shows where the proof tree ends in Γ |- .
Joseph Vidal-Rosset could make a fork of his website,
that provides poket McCarthy directly for experimentation,

also using better proof tree lables. My own web site
does not yet show some red color. Thats a little too
early. First need to get my head around model finding

from tableaux for the non-propositional case...

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1:
> There is a bug in nff_pure.pl by Jens Otten. This here:
>
> Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
> Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
>
> Should read, so that it runs in a wider variety of Prolog systems:
>
> Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
> Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,
>
> And we can now try Pelletier problem 71, and it doesn’t work:
>
> % 88,652,639 inferences, 13.734 CPU in 13.999 seconds
> (98% CPU, 6454800 Lips)
> ERROR: Stack limit (1.0Gb) exceeded
>
> Strange...
>
> Mostowski Collapse schrieb:
> > Why does Jens Otten automatic reordering preprocessing
> > give some bang? Now I get for Pelletier problem 71:
> >
> > /* Joseph Vidal-Rossets LeanSeq, from his web site */
> > ?- test.
> > % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
> > (99% CPU, 10908954 Lips)
> > true.
> > https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
> >
> >
> > /* My McCarthy */
> > ?- test2.
> > % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
> > (98% CPU, 8019776 Lips)
> > true.
> >
> > I think this is because rbicond is more symmetric,
> > in my new McCarthy it is now:
> >
> > prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
> > prove(G>[~A,B|D],P1),
> > prove(G>[A,~B|D], P2).
> >
> > On the other hand Joseph Vidal-Rossets LeanSeq
> > has the following rbicond rule:
> >
> > prove(G>D, rbicond(G>D,P1,P2)):-
> > select((A<=>B),D,D1),!,
> > prove([A|G]>[B|D1],P1),
> > prove([B|G]>[A|D1], P2).
> >
> > But this works only for Pelletier problem 71.
> > The rule is still quite static, and doesn't
> >
> > do any reordering.
> >
> > Mostowski Collapse schrieb:
> >> Here is a poket McCarthy for propositional logic only.
> >> It can also do Joseph Vidal-Rossets antisequent (asq):
> >> :- op( 500, fy, ~). % negation
> >> :- op(1000, xfy, &). % conjunction
> >> :- op(1100, xfy, '|'). % disjunction
> >> :- op(1110, xfy, =>). % conditional
> >> :- op(1120, xfy, <=>). % biconditional
> >>
> >> prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
> >> prove(G>[~A,B|D],P).
> >> prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
> >> prove(G>[A,B|D],P).
> >> /* double negation */
> >> prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
> >> prove(G>[A|D],P).
> >> prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
> >> prove(G>[~A,~B|D],P).
> >>
> >> prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
> >> prove(G>[~A,B|D],P1),
> >> prove(G>[A,~B|D], P2).
> >> prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
> >> prove(G>[~A,~B|D],P1),
> >> prove(G>[A,B|D],P2).
> >> prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
> >> prove(G>[A|D],P1),
> >> prove(G>[~B|D],P2).
> >> prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
> >> prove(G>[A|D],P1),
> >> prove(G>[B|D],P2).
> >> prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
> >> prove(G>[~A|D],P1),
> >> prove(G>[~B|D],P2).
> >>
> >> prove(G>[A|D], ax(G>[A|D], A)):-
> >> member(B,G), A==B, !.
> >>
> >> /* next */
> >> prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
> >> prove([A|G]>D,P).
> >> prove(G>[A|D], lneg(G>[A|D], P)) :- !,
> >> prove([~A|G]>D,P).
> >> prove(G>[], asq(G>[], asq)).
> >>
> >> provable(F,P):-
> >> prove([]>[F],P).
> >>
> >> member(E, [E|_]).
> >> member(E, [_|Xs]) :-
> >> member(E, Xs).

This one is much shorter, 6 pages code by Triska, 2015:
Prolog implementation of the Knuth-Bendix completion procedure
https://www.metalevel.at/trs/

But is it lean? Something shorter maybe?

Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:03:24 UTC+1:
> The completion-based method for mixed E-unification we
> have described, has been implemented as part of the
> tableau-based theorem prover 3TAP [3]. The implementation
> consists of about 2500 lines of code, written in Quintus Prolog.
> Besides the possibility to prove theorems from predicate logic
> with equality, the E-unification module can be used “stand alone”
> to solve simultaneous mixed E-unification problems.
> https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf

Melvin Fitting uses the anti-sequents in a semantic completeness
argument. This then explains how validity proving is relatated to SAT
solving. Actually to be precise, validity is UNSAT. For randomized

algorithms there are complexity results for (SAT, ε-UNSAT). But these
results only appeared in recent years.

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 16:54:35 UTC+1:
> If I paste my poket McCarthy into Joseph Vidal-Rossets web
> page, I can reproduce the example from page 7 of this paper:
>
> leanTAP Revisited
> Melvin Fitting - March 13, 1997
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf
>
> Simply use this here:
> ?- provable(((~p & q) | p), Proof).
>
> The red color shows where the proof tree ends in Γ |- .
> Joseph Vidal-Rosset could make a fork of his website,
> that provides poket McCarthy directly for experimentation,
>
> also using better proof tree lables. My own web site
> does not yet show some red color. Thats a little too
> early. First need to get my head around model finding
>
> from tableaux for the non-propositional case...
> Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1:
> > There is a bug in nff_pure.pl by Jens Otten. This here:
> >
> > Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
> > Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
> >
> > Should read, so that it runs in a wider variety of Prolog systems:
> >
> > Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
> > Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,
> >
> > And we can now try Pelletier problem 71, and it doesn’t work:
> >
> > % 88,652,639 inferences, 13.734 CPU in 13.999 seconds
> > (98% CPU, 6454800 Lips)
> > ERROR: Stack limit (1.0Gb) exceeded
> >
> > Strange...
> >
> > Mostowski Collapse schrieb:
> > > Why does Jens Otten automatic reordering preprocessing
> > > give some bang? Now I get for Pelletier problem 71:
> > >
> > > /* Joseph Vidal-Rossets LeanSeq, from his web site */
> > > ?- test.
> > > % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
> > > (99% CPU, 10908954 Lips)
> > > true.
> > > https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
> > >
> > >
> > > /* My McCarthy */
> > > ?- test2.
> > > % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
> > > (98% CPU, 8019776 Lips)
> > > true.
> > >
> > > I think this is because rbicond is more symmetric,
> > > in my new McCarthy it is now:
> > >
> > > prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
> > > prove(G>[~A,B|D],P1),
> > > prove(G>[A,~B|D], P2).
> > >
> > > On the other hand Joseph Vidal-Rossets LeanSeq
> > > has the following rbicond rule:
> > >
> > > prove(G>D, rbicond(G>D,P1,P2)):-
> > > select((A<=>B),D,D1),!,
> > > prove([A|G]>[B|D1],P1),
> > > prove([B|G]>[A|D1], P2).
> > >
> > > But this works only for Pelletier problem 71.
> > > The rule is still quite static, and doesn't
> > >
> > > do any reordering.
> > >
> > > Mostowski Collapse schrieb:
> > >> Here is a poket McCarthy for propositional logic only.
> > >> It can also do Joseph Vidal-Rossets antisequent (asq):
> > >> :- op( 500, fy, ~). % negation
> > >> :- op(1000, xfy, &). % conjunction
> > >> :- op(1100, xfy, '|'). % disjunction
> > >> :- op(1110, xfy, =>). % conditional
> > >> :- op(1120, xfy, <=>). % biconditional
> > >>
> > >> prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
> > >> prove(G>[~A,B|D],P).
> > >> prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
> > >> prove(G>[A,B|D],P).
> > >> /* double negation */
> > >> prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
> > >> prove(G>[A|D],P).
> > >> prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
> > >> prove(G>[~A,~B|D],P).
> > >>
> > >> prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
> > >> prove(G>[~A,B|D],P1),
> > >> prove(G>[A,~B|D], P2).
> > >> prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
> > >> prove(G>[~A,~B|D],P1),
> > >> prove(G>[A,B|D],P2).
> > >> prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
> > >> prove(G>[A|D],P1),
> > >> prove(G>[~B|D],P2).
> > >> prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
> > >> prove(G>[A|D],P1),
> > >> prove(G>[B|D],P2).
> > >> prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
> > >> prove(G>[~A|D],P1),
> > >> prove(G>[~B|D],P2).
> > >>
> > >> prove(G>[A|D], ax(G>[A|D], A)):-
> > >> member(B,G), A==B, !.
> > >>
> > >> /* next */
> > >> prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
> > >> prove([A|G]>D,P).
> > >> prove(G>[A|D], lneg(G>[A|D], P)) :- !,
> > >> prove([~A|G]>D,P).
> > >> prove(G>[], asq(G>[], asq)).
> > >>
> > >> provable(F,P):-
> > >> prove([]>[F],P).
> > >>
> > >> member(E, [E|_]).
> > >> member(E, [_|Xs]) :-
> > >> member(E, Xs).

Today a little show of what can go wrong: Question
was why does Jens Otten leanseq_v5.pl use this:

prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).

And not this:

prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).

The offending test case is this here:

∀y∃xFxy → ∃z∀tFzt is invalid.
Countermodel:
Domain: { 0, 1 }
F: { (0,0), (1,1) }
https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

I guess there is some literature that explains everything. On the
other hand some Prolog experimentation could maybe help
increase intuition. leanseq_v5.pl first, and I get, limiting the

depth to 10, it already takes quite some time with 10 in this
automated prover which doesn’t have much optimizations:

% leanseq_v5.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
iteration 3
iteration 4
iteration 5
iteration 6
iteration 7
iteration 8
iteration 9
iteration 10
false.

Now the faulty leanseq_v5f.pl, where the Skolem function
is replaced by only a Skolem constant:

% leanseq_v5f.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
true

Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:11:01 UTC+1:
> Today a little show of what can go wrong: Question
> was why does Jens Otten leanseq_v5.pl use this:
>
> prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
> copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
> J1 is J+1,
> prove(G > [A1|D1],FV,I,J1,K).
>
> And not this:
>
> prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
> copy_term((X:A,FV),(f_sk(J):A1,FV)),
> J1 is J+1,
> prove(G > [A1|D1],FV,I,J1,K).
>
> The offending test case is this here:
>
> ∀y∃xFxy → ∃z∀tFzt is invalid.
> Countermodel:
> Domain: { 0, 1 }
> F: { (0,0), (1,1) }
> https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

nyway, because nobody has time to wait for ZDD provide a model
finder or to wait that theorem prover has finished its infinitely many
iterations, to show that a formula isn’t provable.

I started publishing a counter model finder for my new Dogelog player.
This is a first beginning, more posts will follow.

Boole’s Method from 1847 in Dogelog Player
https://twitter.com/dogelogch/status/1487845636993134596

Boole’s Method from 1847 in Dogelog Player
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:15:08 UTC+1:
> I guess there is some literature that explains everything. On the
> other hand some Prolog experimentation could maybe help
> increase intuition. leanseq_v5.pl first, and I get, limiting the
>
> depth to 10, it already takes quite some time with 10 in this
> automated prover which doesn’t have much optimizations:
>
> % leanseq_v5.pl compiled 0.00 sec, 17 clauses
> ?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
> iteration 1
> iteration 2
> iteration 3
> iteration 4
> iteration 5
> iteration 6
> iteration 7
> iteration 8
> iteration 9
> iteration 10
> false.
>
> Now the faulty leanseq_v5f.pl, where the Skolem function
> is replaced by only a Skolem constant:
>
> % leanseq_v5f.pl compiled 0.00 sec, 17 clauses
> ?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
> iteration 1
> iteration 2
> true
> Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:11:01 UTC+1:
> > Today a little show of what can go wrong: Question
> > was why does Jens Otten leanseq_v5.pl use this:
> >
> > prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
> > copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
> > J1 is J+1,
> > prove(G > [A1|D1],FV,I,J1,K).
> >
> > And not this:
> >
> > prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
> > copy_term((X:A,FV),(f_sk(J):A1,FV)),
> > J1 is J+1,
> > prove(G > [A1|D1],FV,I,J1,K).
> >
> > The offending test case is this here:
> >
> > ∀y∃xFxy → ∃z∀tFzt is invalid.
> > Countermodel:
> > Domain: { 0, 1 }
> > F: { (0,0), (1,1) }
> > https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

You can run leanTap in Dogelog player in the browser. For the
simple problems among Pelletier 17-46 I get the following
results (100 iterations, browser was Chrome no async/await):

System Time
Tau Prolog 323’000
Dogelog Player 2’441
Formerly Jekejeke 811
SWI 299

Will post a link to a fork later. I want to compare different normal
forms, but still struggling with optimal way to compute prenex and
mini-scope. Too large design space, so slow progress.

The simple problems are:

17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44

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?

I used a leanSeq variant that saturates the literals before it tries the quantifier.
When I compare the two, there is not anymore much difference between leanSeq
and leanTap. Only the new leanSeq would allow easy proof extraction:

/* leanTap */
?- time((between(1,100,_), test(time), fail; true)).
% 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips)
true.

/* leanSeq+NNF+literal saturation */
?- time((between(1,100,_), test(time), fail; true)).
% 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips)
true.

The difference is only a factor of ca. 4. Not that bad. I used a simple
negation normal form without any reordering for both.

Mostowski Collapse schrieb am Dienstag, 8. Februar 2022 um 12:28:05 UTC+1:
> You can run leanTap in Dogelog player in the browser. For the
> simple problems among Pelletier 17-46 I get the following
> results (100 iterations, browser was Chrome no async/await):
>
> System Time
> Tau Prolog 323’000
> Dogelog Player 2’441
> Formerly Jekejeke 811
> SWI 299
>
> Will post a link to a fork later. I want to compare different normal
> forms, but still struggling with optimal way to compute prenex and
> mini-scope. Too large design space, so slow progress.
>
> The simple problems are:
>
> 17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44

Thats the code of the two provers. First leanTap you might easily recognize:

prove((A|B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim).
prove((A&B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,UnExp,Lits,FreeV,VarLim),
prove(B,UnExp,Lits,FreeV,VarLim).
prove((?[X]:Fml),UnExp,Lits,FreeV,VarLim) :- VarLim>0, !,
copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
append(UnExp,[(?[X]:Fml)],UnExp1),
VarLim2 is VarLim-1,
prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim2).
prove(Lit,_,Lits,_,_) :-
\+ Lit = (?_),
member(L,Lits), unify_with_occurs_check(Lit,L).
prove(Fml,[Next|UnExp],Lits,FreeV,VarLim) :-
opposite(Fml, Fml1),
prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim).

And here leanSeq, which expects NNF and does literal saturation:

prove((A|B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim,J,K).
prove((A&B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
prove(A,UnExp,Lits,FreeV,VarLim,J,H),
prove(B,UnExp,Lits,FreeV,VarLim,H,K).
prove((![X]:Fml),UnExp,Lits,FreeV,VarLim,J,K) :- !,
copy_term((X:Fml,FreeV),(h(J,FreeV):Fml1,FreeV)),
J1 is J+1,
prove(Fml1,UnExp,Lits,FreeV,VarLim,J1,K).
prove(Lit,_,Lits,_,_,J,J) :-
\+ Lit = (?_),
member(L,Lits),
unify_with_occurs_check(Lit,L).
prove(Fml,[Next|UnExp],Lits,FreeV,VarLim,J,K) :- !,
opposite(Fml, Fml1),
prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim,J,K).

% we are saturated
prove(Fml,[],Lits,FreeV,VarLim,J,K) :- VarLim>0, opposite(Fml, L),
member(H,[L|Lits]),
H = ~ (?_),
opposite(H,M),
block(M,[L|Lits],FreeV,VarLim,J,K).

% quantifier block
block((?[X]:Fml),Lits,FreeV,VarLim,J,K) :- !, VarLim>0,
copy_term((X:Fml,FreeV),(Y:Fml1,FreeV)),
VarLim2 is VarLim-1,
block(Fml1,Lits,[Y|FreeV],VarLim2,J,K).
block(Fml,Lits,FreeV,VarLim,J,K) :-
prove(Fml,[],Lits,FreeV,VarLim,J,K).

The new leanSeq has a little more backtracking in the handling of (?[X]:Fml),
block/6 is mitigating the problem a little bit. Overall the penality seems to be
not so high, measured by the simple Pelletier problems.

Mostowski Collapse schrieb am Donnerstag, 10. Februar 2022 um 17:27:55 UTC+1:
> 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?
>
> I used a leanSeq variant that saturates the literals before it tries the quantifier.
> When I compare the two, there is not anymore much difference between leanSeq
> and leanTap. Only the new leanSeq would allow easy proof extraction:
>
> /* leanTap */
> ?- time((between(1,100,_), test(time), fail; true)).
> % 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips)
> true.
>
> /* leanSeq+NNF+literal saturation */
> ?- time((between(1,100,_), test(time), fail; true)).
> % 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips)
> true.
>
> The difference is only a factor of ca. 4. Not that bad. I used a simple
> negation normal form without any reordering for both.
> Mostowski Collapse schrieb am Dienstag, 8. Februar 2022 um 12:28:05 UTC+1:
> > You can run leanTap in Dogelog player in the browser. For the
> > simple problems among Pelletier 17-46 I get the following
> > results (100 iterations, browser was Chrome no async/await):
> >
> > System Time
> > Tau Prolog 323’000
> > Dogelog Player 2’441
> > Formerly Jekejeke 811
> > SWI 299
> >
> > Will post a link to a fork later. I want to compare different normal
> > forms, but still struggling with optimal way to compute prenex and
> > mini-scope. Too large design space, so slow progress.
> >
> > The simple problems are:
> >
> > 17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44

Happy Birthday Jacques Herbrand

February 12th, 1908: French mathematician, worked in
math. logic and field theory, Jacques Herbrand, was born.
https://twitter.com/sc_k/status/9011037015

Lectures on Jacques Herbrand as a Logician
https://arxiv.org/abs/0902.4682

Now I managed to add first order equality to
leanTap. Here is a comparison:

leanSeq= vs leanTap= in Dogelog Player
https://twitter.com/dogelogch/status/1492869014267248641

leanSeq= vs leanTap= in Dogelog Player
https://www.facebook.com/groups/dogelog

Have Fun!

Mostowski Collapse schrieb am Samstag, 12. Februar 2022 um 14:02:24 UTC+1:
> Happy Birthday Jacques Herbrand
>
> February 12th, 1908: French mathematician, worked in
> math. logic and field theory, Jacques Herbrand, was born.
> https://twitter.com/sc_k/status/9011037015
>
> Lectures on Jacques Herbrand as a Logician
> https://arxiv.org/abs/0902.4682

The next step in proof assistants would be a theorem prover
with an inconsistent logic that when programs are extracted,
these programs will make Zucks metaverse collapse (or USA
think Russia is invading Ukraine, etc.. etc.. as you like)

Just like Jean Tinguely:

He then began to construct his first truly sophisticated kinetic
sculptures, which he termed métaméchaniques, or metamechanicals.
These were robotlike contraptions constructed of wire and sheet
metal, the constituent parts of which moved or spun at varying
speeds. Further innovations on Tinguely’s part in the mid- and
late 1950s led to a series of sculptures entitled “Machines à
peindre” (“Painting Machines”); these robotlike machines continuously
painted pictures of abstract patterns to the accompaniment of self-
produced sounds and noxious odours. The 8-foot-long “painting
machine” that Tinguely set up at the first Paris Biennale in 1959
produced some 40,000 different paintings for exhibition visitors
who inserted a coin in its slot.

Tinguely was meanwhile becoming obsessed with the concept of
destruction as a means of achieving the “dematerialization” of his
works of art. In 1960 he created a sensation with his first large self-
destroying sculpture, the 27-foot-high metamatic entitled “Homage
to New York,” whose public suicide he demonstrated at the Museum
of Modern Art in New York City. The event was a fiasco, with the
complicated assemblage of motors and wheels failing to operate
(i.e., destroy itself) properly; it had to be dispatched by city firemen
with axes after having started a fire. But Tinguely’s next two self-
destroying machines, entitled “Study for an End of the World,” performed
more successfully, detonating themselves with considerable
amounts of explosives.
https://www.britannica.com/biography/Jean-Tinguely#ref290920

A well suited candidate for such self destroing machines
is miniKanren. In the case of miniKanren, it does already
self destroy during theorem proving. I have no clue

what they are reporting here (in milliseconds):

Pelletier #34:
leanTap: 199'129.0
mKleanTap: 7'272.9
αleanTap: 8493.5
Near J.P., Byrd W.E., Friedman D.P. (2008) αleanTAP: A Declarative
Theorem Prover for First-Order Classical Logic. In: Garcia de la Banda
M., Pontelli E. (eds) Logic Programming. ICLP 2008. Lecture Notes in
Computer Science, vol 5366. Springer, Berlin, Heidelberg.
http://webyrd.net/alphaleantap/alphatap.pdf

Maybe they used a version with an unfavorable biconditional
realization or some other nonsense. In my fluffy Dogelog player
I get here and now on my slow MacOSX machine:

?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
<=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), tap, I)).
% Wall 1385 ms, gc 5 ms, 2342329 lips
I = 5.
http://www.xlog.ch/izytab/doclet/docs/18_live/32_bik2022/paste36/package.html

Anybody can reproduce the same result in his own
browser. It rather tells me that the miniKanren solutions
are uselessly slow...

Pelletier 34 has an errata, it says Problem # 34: The third
occurrence of 'P' should be 'Q'. This is in my TPTP form q(T).
Me thinks the formula is correct.

Its even a much less a challenge for leanSeq:

?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
<=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), seq, I)).
% Wall 29 ms, gc 1 ms, 1056620 lips
I = 2.

If I have time I will double check a proof tree...

Mostowski Collapse schrieb am Montag, 14. Februar 2022 um 18:35:36 UTC+1:
> with axes after having started a fire. But Tinguely’s next two self-
> destroying machines, entitled “Study for an End of the World,” performed
> more successfully, detonating themselves with considerable
> https://www.britannica.com/biography/Jean-Tinguely#ref290920

Probably something that would make Alain
Colmerauer happy. By way of EricGT on
SWI-Prolog discourse:

"Prolog broke into the top 20 again a few months ago
(should have captured it then for historical use).
As of June 2022 it is still at 20."
https://www.tiobe.com/tiobe-index/

I guess we can overtake Ruby, which is on 19,
if we provide some "Prolog on Rails". Anybody up to it?

Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:12:37 UTC+2:
> Probably something that would make Alain
> Colmerauer happy. By way of EricGT on
> SWI-Prolog discourse:
>
> "Prolog broke into the top 20 again a few months ago
> (should have captured it then for historical use).
> As of June 2022 it is still at 20."
> https://www.tiobe.com/tiobe-index/

(P.S.: The idea would be to provide and base the Rails
functionality in 100% Prolog programming language)

Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:36:49 UTC+2:
> I guess we can overtake Ruby, which is on 19,
> if we provide some "Prolog on Rails". Anybody up to it?
>
> Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:12:37 UTC+2:
> > Probably something that would make Alain
> > Colmerauer happy. By way of EricGT on
> > SWI-Prolog discourse:
> >
> > "Prolog broke into the top 20 again a few months ago
> > (should have captured it then for historical use).
> > As of June 2022 it is still at 20."
> > https://www.tiobe.com/tiobe-index/

Biologicians have found a new animal, speedy exit saurus
aka ruZZian soldier, its the fastest animal on this planet:

The fastest animals in the world...
https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849

You can learn a lot from this animal, for example:

- Rule 1 of speedy exit:
for maximum speed, washing machine trophy, just drop it.

- Rule 2 of speedy exit:
same holds for tank, ammunition, riffle, etc.. etc..

Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:21:08 UTC+2:
> Biologicians have found a new animal, speedy exit saurus
> aka ruZZian soldier, its the fastest animal on this planet:
>
> The fastest animals in the world...
> https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849

Disclaimer: Source of OSTINT, 9gag.com head quarters.
(one should not praise the morning before the evening)

Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:25:25 UTC+2:
> You can learn a lot from this animal, for example:
>
> - Rule 1 of speedy exit:
> for maximum speed, washing machine trophy, just drop it.
>
> - Rule 2 of speedy exit:
> same holds for tank, ammunition, riffle, etc.. etc..
> Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:21:08 UTC+2:
> > Biologicians have found a new animal, speedy exit saurus
> > aka ruZZian soldier, its the fastest animal on this planet:
> >
> > The fastest animals in the world...
> > https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849

Somebody said:

> I think probabilistic reasoning itself is borken

Well I was a purist like that also in the past. And I am still a
kind of purist like that in the present, avoiding probability
whenever possible. But its a nice little

mathematical model, which you can map to constraint logic
programming CLP(R). So if for example you have an
equation involving probability:

P(A & B) < P(C)

Then this says nothing else than the CLP(R) constraint:

w + z < z + y + x + c