Logic Rules

977 views
Skip to first unread message

Graham Cooper

unread,
Aug 29, 2020, 11:35:55 PM8/29/20
to
www.miniBASE.com




case('1.2', 'Taut', P+P=<P).
case('1.3', 'Add', Q=<P+Q).
case('1.4', '', P+Q=<Q+P).
case('1.5', 'Assoc', P+(Q+R)=<Q+(P+R)).
case('1.6', 'Sum', (Q=<R)=<(P+Q=<P+R)).
case('2.01', '', (P=< ~P)=< ~P).
case('2.02', 'Simp', Q=<(P=<Q)).
case('2.03', '', (P=< ~Q)=<(Q=< ~P)).
case('2.04', 'Comm', (P=<(Q=<R))=<(Q=<(P=<R))).
case('2.05', 'Syll', (Q=<R)=<((P=<Q)=<(P=<R))).
case('2.06', 'Syll', (P=<Q)=<((Q=<R)=<(P=<R))).
case('2.07', '', P=<P+P).
case('2.08', 'Id', P=<P).
case('2.1', '', ~P+P).
case('2.11', '', P+ ~P).
case('2.12', '', P=< ~ ~P).
case('2.13', '', P+ ~ ~ ~P).
case('2.14', '', ~ ~P=<P).
case('2.15', 'Transp', (~P=<Q)=<(~Q=<P)).
case('2.16', '', (P=<Q)=<(~Q=< ~P)).
case('2.17', 'Transp', (~Q=< ~P)=<(P=<Q)).
case('2.18', '', (~P=<P)=<P).
case('2.2', '', P=<P+Q).
case('2.21', '', ~P=<(P=<Q)).
case('2.24', '', P=<(~P=<Q)).
case('2.25', '', P+(P+Q=<Q)).
case('2.26', '(GB 35=>25)', ~P+((P=<Q)=<Q)).
case('2.27', '', P=<((P=<Q)=<Q)).
case('2.3', '', P+(Q+R)=<P+(R+Q)).
case('2.31', '', P+(Q+R)=<P+Q+R).
case('2.32', '', P+Q+R=<P+(Q+R)).
case('2.36', '', (Q=<R)=<((~P=<Q)=<(~R=<P))).
case('2.37', '', (Q=<R)=<((~Q=<P)=<(~P=<R))).
case('2.38', '', (Q=<R)=<((~Q=<P)=<(~R=<P))).
case('2.4', '', P+(P+Q)=<P+Q).
case('2.41', '', Q+(P+Q)=<P+Q).
case('2.42', '', ~P+(P=<Q)=<(P=<Q)).
case('2.43', '', (P=<(P=<Q))=<(P=<Q)).
case('2.45', '', ~ (P+Q)=< ~P).
case('2.46', '', ~ (P+Q)=< ~Q).
case('2.47', '(GB 35=>31)', ~ (P+Q)=< ~P+Q).
case('2.48', '(GB 45=>43)', ~ (P+Q)=<P+ ~Q).
case('2.49', '(GB 35=>31)', ~ (P+Q)=< ~P+ ~Q).
case('2.5', '(GB 35=>31)', ~ (P=<Q)=<(~P=<Q)).
case('2.51', '(GB 45=>43)', ~ (P=<Q)=<(P=< ~Q)).
case('2.52', '(GB 35=>31)', ~ (P=<Q)=<(~P=< ~Q)).
case('2.521', '(GB 29=>25)', ~ (P=<Q)=<(Q=<P)).
case('2.53', '', P+Q=<(~P=<Q)).
case('2.54', '', (~P=<Q)=<P+Q).
case('2.55', '', ~P=<(P+Q=<Q)).
case('2.56', '(GB 37=>35)', ~Q=<(P+Q=<P)).
case('2.6', '', (~P=<Q)=<((P=<Q)=<Q)).
case('2.61', '', (P=<Q)=<((~P=<Q)=<Q)).
case('2.62', '', P+Q=<((P=<Q)=<Q)).
case('2.621', '', (P=<Q)=<(P+Q=<Q)).
case('2.63', '', P+Q=<(~P+Q=<Q)).
case('2.64', '(GB 61=>39)', P+Q=<(P+ ~Q=<P)).
case('2.65', '', (P=<Q)=<((P=< ~Q)=< ~P)).
case('2.67', '', (P+Q=<Q)=<(P=<Q)).
case('2.68', '', ((P=<Q)=<Q)=<P+Q).
case('2.69', '', ((P=<Q)=<Q)=<((Q=<P)=<P)).
case('2.73', '', (P=<Q)=<(P+Q+R=<Q+R)).
case('2.74', '', (Q=<P)=<(P+Q+R=<P+R)).
case('2.75', '', P+Q=<(P+(Q=<R)=<P+R)).
case('2.76', '', P+(Q=<R)=<(P+Q=<P+R)).
case('2.77', '', (P=<(Q=<R))=<((P=<Q)=<(P=<R))).
case('2.8', '(GB 63=>43)', Q+R=<(~R+S=<Q+S)).
case('2.81', '', (Q=<(R=<S))=<(P+Q=<(P+R=<P+S))).
case('2.82', '', P+Q+R=<(P+ ~R+S=<P+Q+S)).
case('2.83', '', (P=<(Q=<R))=<((P=<(R=<S))=<(P=<(Q=<S)))).
case('2.85', '(GB 41=>37)', (P+Q=<P+R)=<P+(Q=<R)).
case('2.86', '(GB 41=>37)', ((P=<Q)=<(P=<R))=<(P=<(Q=<R))).
case('3.1', '(GB 79=>73)', P*Q=< ~ (~P+ ~Q)).
case('3.11', '(GB 73=>63)', ~ (~P+ ~Q)=<P*Q).
case('3.12', '(GB 73=>63)', ~P+ ~Q+P*Q).
case('3.13', '(GB 47=>37)', ~ (P*Q)=< ~P+ ~Q).
case('3.14', '', ~P+ ~Q=< ~ (P*Q)).
case('3.2', '', P=<(Q=<P*Q)).
case('3.21', '', Q=<(P=<P*Q)).
case('3.22', '(GB 79=>69)', P*Q=<Q*P).
case('3.24', '', ~ (P* ~P)).
case('3.26', 'Simp', P*Q=<P).
case('3.27', 'Simp', P*Q=<Q).
case('3.3', 'Exp (GB 63=>59)', (P*Q=<R)=<(P=<(Q=<R))).
case('3.31', 'Imp', (P=<(Q=<R))=<(P*Q=<R)).
case('3.33', 'Syll (GB 113=>105)', (P=<Q)*(Q=<R)=<(P=<R)).
case('3.34', 'Syll', (Q=<R)*(P=<Q)=<(P=<R)).
case('3.35', 'Ass (GB 93=>63)', P*(P=<Q)=<Q).
case('3.37', 'Transp', (P*Q=<R)=<(P* ~R=< ~Q)).
case('3.4', '(GB 33=>31)', P*Q=<(P=<Q)).
case('3.41', '', (P=<R)=<(P*Q=<R)).
case('3.42', '', (Q=<R)=<(P*Q=<R)).
case('3.43', 'Comp', (P=<Q)*(P=<R)=<(P=<Q*R)).
case('3.44', '', (Q=<P)*(R=<P)=<(Q+R=<P)).
case('3.45', 'Fact (GB 79=>71)', (P=<Q)=<(P*R=<Q*R)).
case('3.47', '', (P=<R)*(Q=<S)=<(P*Q=<R*S)).
case('3.48', '(GB 245=>241)', (P=<R)*(Q=<S)=<(P+Q=<R+S)).
case('4.1', '', (P=<Q)=:=(~Q=< ~P)).
case('4.11', '', (P=:=Q)=:=(~P=:= ~Q)).
case('4.12', '', (P=:= ~Q)=:=(Q=:= ~P)).
case('4.13', '', P=:= ~ ~P).
case('4.14', '(GB 325=>321)', (P*Q=<R)=:=(P* ~R=< ~Q)).
case('4.15', '(GB 281=>277)', (P*Q=< ~R)=:=(Q*R=< ~P)).
case('4.2', '', P=:=P).
case('4.21', '(GB 183=>163)', (P=:=Q)=:=(Q=:=P)).
case('4.22', '(GB 329=>273)', (P=:=Q)*(Q=:=R)=<(P=:=R)).
case('4.24', '(GB 91=>89)', P=:=P*P).
case('4.25', '', P=:=P+P).
case('4.3', '(GB 183=>163)', P*Q=:=Q*P).
case('4.31', '', P+Q=:=Q+P).
case('4.32', '(GB 359=>355)', P*Q*R=:=P*(Q*R)).
case('4.33', '', P+Q+R=:=P+(Q+R)).
case('4.36', '(GB 311=>291)', (P=:=Q)=<(P*R=:=Q*R)).
case('4.37', '(GB 311=>307)', (P=:=Q)=<(P+R=:=Q+R)).
case('4.38', '', (P=:=R)*(Q=:=S)=<(P*Q=:=R*S)).
case('4.39', '(GB 913=>901)', (P=:=R)*(Q=:=S)=<(P+Q=:=R+S)).
case('4.4', '', P*(Q+R)=:=P*Q+P*R).
case('4.41', '', P+Q*R=:=(P+Q)*(P+R)).
case('4.42', '(GB 175=>165)', P=:=P*Q+P* ~Q).
case('4.43', '', P=:=(P+Q)*(P+ ~Q)).
case('4.44', '', P=:=P+P*Q).
case('4.45', '(GB 161=>107)', P=:=P*(P+Q)).
case('4.5', '(GB 177=>161)', P*Q=:= ~ (~P+ ~Q)).
case('4.51', '(GB 127=>117)', ~ (P*Q)=:= ~P+ ~Q).
case('4.52', '(GB 231=>219)', P* ~Q=:= ~ (~P+Q)).
case('4.53', '(GB 181=>169)', ~ (P* ~Q)=:= ~P+Q).
case('4.54', '', ~P*Q=:= ~ (P+ ~Q)).
case('4.55', '', ~ (~P*Q)=:=P+ ~Q).
case('4.56', '', ~P* ~Q=:= ~ (P+Q)).
case('4.57', '', ~ (~P* ~Q)=:=P+Q).
case('4.6', '', (P=<Q)=:= ~P+Q).
case('4.61', '', ~ (P=<Q)=:=P* ~Q).
case('4.62', '', (P=< ~Q)=:= ~P+ ~Q).
case('4.63', '', ~ (P=< ~Q)=:=P*Q).
case('4.64', '', (~P=<Q)=:=P+Q).
case('4.65', '', ~ (~P=<Q)=:= ~P* ~Q).
case('4.66', '', (~P=< ~Q)=:=P+ ~Q).
case('4.67', '', ~ (~P=< ~Q)=:= ~P*Q).
case('4.7', '', (P=<Q)=:=(P=<P*Q)).
case('4.71', '', (P=<Q)=:=(P=:=P*Q)).
case('4.72', '', (P=<Q)=:=(Q=:=P+Q)).
case('4.73', '', Q=<(P=:=P*Q)).
case('4.74', '', ~P=<(Q=:=P+Q)).
case('4.76', '', (P=<Q)*(P=<R)=:=(P=<Q*R)).
case('4.77', '', (Q=<P)*(R=<P)=:=(Q+R=<P)).
case('4.78', '(GB 327=>319)', (P=<Q)+(P=<R)=:=(P=<Q+R)).
case('4.79', '(GB 547=>383)', (Q=<P)+(R=<P)=:=(Q*R=<P)).
case('4.8', '', (P=< ~P)=:= ~P).
case('4.81', '', (~P=<P)=:=P).
case('4.82', '(GB 249=>179)', (P=<Q)*(P=< ~Q)=:= ~P).
case('4.83', '', (P=<Q)*(~P=<Q)=:=Q).
case('4.84', '(GB 139=>135)', (P=:=Q)=<((P=<R)=:=(Q=<R))).
case('4.85', '', (P=:=Q)=<((R=<P)=:=(R=<Q))).
case('4.86', '(GB 621=>617)', (P=:=Q)=<((P=:=R)=:=(Q=:=R))).
case('4.87', '(GB 531=>523)', ((P*Q=<R)=:=(P=<(Q=<R)))*((
P=<(Q=<R))=:=(Q=<(P=<R)))*((Q=<(P=<R))=:=(Q*P=<R))).
case('5.1', '(GB 111=>107)', P*Q=<(P=:=Q)).
case('5.11', '(GB 35=>31)', (P=<Q)+(~P=<Q)).
case('5.12', '(GB 45=>43)', (P=<Q)+(P=< ~Q)).
case('5.13', '(GB 29=>25)', (P=<Q)+(Q=<P)).
case('5.14', '(GB 29=>25)', (P=<Q)+(Q=<R)).
case('5.15', '', (P=:=Q)+(P=:= ~Q)).
case('5.16', '(GB 377=>333)', ~ ((P=:=Q)*(P=:= ~Q))).
case('5.17', '', (P+Q)* ~ (P*Q)=:=(P=:= ~Q)).
case('5.18', '(GB 577=>503)', (P=:=Q)=:= ~ (P=:= ~Q)).
case('5.19', '(GB 141=>131)', ~ (P=:= ~P)).
case('5.21', '(GB 123=>115)', ~P* ~Q=<(P=:=Q)).
case('5.22', '', ~ (P=:=Q)=:=P* ~Q+Q* ~P).
case('5.23', '(GB 557=>513)', (P=:=Q)=:=P*Q+ ~P* ~Q).
case('5.24', '(GB 669=>585)', ~ (P*Q+ ~P* ~Q)=:=P* ~Q+Q* ~P).
case('5.25', '', P+Q=:=((P=<Q)=<Q)).
case('5.3', '', (P*Q=<R)=:=(P*Q=<P*R)).
case('5.31', '', R*(P=<Q)=<(P=<Q*R)).
case('5.32', '(GB 633=>625)', (P=<(Q=:=R))=:=(P*Q=:=P*R)).
case('5.33', '', P*(Q=<R)=:=P*(P*Q=<R)).
case('5.35', '', (P=<Q)*(P=<R)=<(P=<(Q=:=R))).
case('5.36', '(GB 417=>393)', P*(P=:=Q)=:=Q*(P=:=Q)).
case('5.4', '', (P=<(P=<Q))=:=(P=<Q)).
case('5.41', '(GB 67=>63)', ((P=<Q)=<(P=<R))=:=(P=<(Q=<R))).
case('5.42', '(GB 109=>105)', (P=<(Q=<R))=:=(P=<(Q=<P*R))).
case('5.44', '', (P=<Q)=<((P=<R)=:=(P=<Q*R))).
case('5.5', '', P=<((P=<Q)=:=Q)).
case('5.501', '', P=<(Q=:=(P=:=Q))).
case('5.53', '', (P+Q+R=<S)=:=(P=<S)*(Q=<S)*(R=<S)).
case('5.54', '(GB 253=>239)', (P*Q=:=P)+(P*Q=:=Q)).
case('5.55', '', (P+Q=:=P)+(P+Q=:=Q)).
case('5.6', '(GB 207=>203)', (P* ~Q=<R)=:=(P=<Q+R)).
case('5.61', '(GB 269=>259)', (P+Q)* ~Q=:=P* ~Q).
case('5.62', '', P*Q+ ~Q=:=P+ ~Q).
case('5.63', '', P+Q=:=P+ ~P*Q).
case('5.7', '(GB 681=>673)', (P+R=:=Q+R)=:=R+(P=:=Q)).
case('5.71', '(GB 259=>249)', (Q=< ~R)=<((P+Q)*R=:=P*R)).
case('5.74', '(GB 345=>337)', (P=<(Q=:=R))=:=((P=<Q)=:=(P=<R))).
case('5.75', '', (R=< ~Q)*(P=:=Q+R)=<(P* ~Q=:=R)).

test :-
case(I, _, F),
falsify(F),
write(I),
write(' failure.'),
nl,
fail; true.

Graham Cooper

unread,
Aug 29, 2020, 11:58:27 PM8/29/20
to
(c)
* Rights & License
* All industrial property rights regarding the information - copyright
* and patent rights in particular - are the sole property of XLOG

https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-principia-pl

Mostowski Collapse

unread,
Aug 31, 2020, 6:31:48 AM8/31/20
to
Warning: Be careful besides Boole, Beth and Maslov,
there could be many many more methods.
Maslov is already a Sequent Calculus search

and not a Hilbert Calculus search. BTW, as
usually Jean-Yves Girard is quite an inspiration,
he writes the Cut rule as follows:

G, A & ~A
-------------
G

Transcendental syntax I: deterministic case
http://girard.perso.math.cnrs.fr/Archives.html

Which would work in any take which has
a & rule, multiplicative or additive.

Variant 1: à la Gentzen, with a Split, Cut
Elimination would den be Formula Substitution:

G, A ~A, D
----------------------- (&)
G, D, A & ~A
------------- (Cut)
G, D

Variant 2: à la Maslov, without a Split,
and the Cut could be viewed kind of Boole Probing

A, G ~A, G
----------------------- (&)
G, A & ~A
------------- (Cut)
G

So adding Cut to Maslov, gives a Hybrid Maslov
Boole. But the Hybrid is not perfect, would
also need something like for the Boole reduction:

G[1] G[0]
--------- ----------
A, G[A] ~A, G[A]

Or show that certain paths of derivations give
the same, and the above would be meta-logical.
Not sure what method would result if we would

apply Tarski (Th 66, 1923), see also:

A Note on Satisfying Truth-Value Assignments
of Boolean Formulas - Zbigniew Stachniak -2004
http://www.satisfiability.org/SAT04/programme/52.pdf

Tarskis second theorem on the upper bound of a
function now suddently reminds me of Cut Elimination
à la Gentzen, where we have substitution,

plus Cut Elimination à la Boole, a reading
just proposed here. Is there a relationship?

Mostowski Collapse

unread,
Aug 31, 2020, 6:37:49 AM8/31/20
to
Boole, Beth and Maslov are showcased here:

Prolog Tautology Checking, who does it better?
https://qiita.com/j4n_bur53/items/28d667cf3412fa950bc7

Mostowski Collapse

unread,
Aug 31, 2020, 12:25:16 PM8/31/20
to
Pleae not, its a "checker". Iterative deepening
will not help you in any way at all, if the
search space is infinite. And usually a formula
has infinitely many different proofs, this

for example the case in Hilbert Style. So before
you figured out that your formula hasn't
a proof, your system will nevertheless try
infinitely many proofs, in vain, and not terminate.

You are just a moron Graham Cooper.

Graham Cooper

unread,
Aug 31, 2020, 12:54:36 PM8/31/20
to
On Tuesday, September 1, 2020 at 2:25:16 AM UTC+10, Mostowski Collapse wrote:
> Pleae not, its a "checker". Iterative deepening
> will not help you in any way at all, if the
> search space is infinite. And usually a formula
> has infinitely many different proofs, this
>
> for example the case in Hilbert Style. So before
> you figured out that your formula hasn't
> a proof, your system will nevertheless try
> infinitely many proofs, in vain, and not terminate.


You Fool!

You ASKED IF ANYBODY had seen a similar proof checker that falsifies

and I gave you


?- t( not( and( A , not(B) ) , l(l(0)) ).


--------------------


then you spout nonsense about your mis-understanding of depth limited proof search

HINT: depth limited = BREADTH FIRST MORON



you CHANGE THE PARDIGM


DO NOT ASK - DOES X HAVE A PROOF?

ASK - DOES X HAVE A PROOF IN n STEPS?


Check out the all new www.miniBASE.com

try to enter: ss gray [?]








Mostowski Collapse

unread,
Aug 31, 2020, 5:31:09 PM8/31/20
to
You are changing the topic.

Thats not an answer. It must satisfy positive
and negative test cases. The negative test
cases are here:

Please read carefully:

"As test cases we first used some 6 propositional
logic non-tautologies from Fallacy Files, so as to
see whether the various methods can indeed falsify formulas."
Prolog Tautology Checking, who does it better?
https://qiita.com/j4n_bur53/items/28d667cf3412fa950bc7

And then consider:


negcase('1', 'Affirming a Disjunct', (P+Q)*P=< ~Q).
negcase('2', 'Affirming the Consequent', (P=<Q)*Q=<P).
negcase('3', 'Commutation of Conditionals', (P=<Q)=<(Q=<P)).
negcase('4', 'Denying a Conjunct', ~ (P*Q)* ~P=<Q).
negcase('5', 'Denying the Antecedent', (P=<Q)* ~P=< ~Q).
negcase('6', 'Improper Transposition', (P=<Q)=<(~P=< ~Q)).
6 propositional logic test cases from Fallacy Files.
https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-fallacies-pl

Otherwise its not similar. Otherwise is only
remotely similar. Otherwise its not a
propositional checker.

Whats wrong with you?

P.S.: I am looking for some famous
fallacies that would also test =:=.
Any suggestions.

Mostowski Collapse

unread,
Aug 31, 2020, 5:34:58 PM8/31/20
to
So whats your single predicate that
can both do falsify and tautology at
the same time? This here is not

a falsification:

?- t( not( and( A , not(B) ) , l(l(0)) ).

This would only prove:

|- ~A

Which is not the same as:

|/- A

Example take this formula here, just
a propositional variable:

P

You can neither prove |- P nor can
you prove |- ~P, but you can falsify
P by setting P=0.

Graham Cooper

unread,
Aug 31, 2020, 5:41:16 PM8/31/20
to
On Tuesday, September 1, 2020 at 7:34:58 AM UTC+10, Mostowski Collapse wrote:
> So whats your single predicate that
> can both do falsify and tautology at
> the same time? This here is not
>
> a falsification:
> ?- t( not( and( A , not(B) ) , l(l(0)) ).
> This would only prove:
>
> |- ~A
>
> Which is not the same as:
>
> |/- A
>
> Example take this formula here, just
> a propositional variable:
>
> P
>
> You can neither prove |- P nor can
> you prove |- ~P, but you can falsify
> P by setting P=0.


Ahahaha you are stupid with logic provers


proof( expression , iterations-deep ) [?]

|- expression



where expression can begin not(expression)


SEE www.miniBASE.com

























Mostowski Collapse

unread,
Aug 31, 2020, 5:41:55 PM8/31/20
to
|- ~A and |/- A is not the same.

Mostowski Collapse

unread,
Aug 31, 2020, 5:44:14 PM8/31/20
to
Show me your code for:

falsify(A): The predicate succeeds if |/- A,
i.e. if there is a counter model to A, otherwise
the predicate fails if |- A, i.e. if the formula
A is generally valid. There is no floundering,
the predicate always terminates and succeeds
or fails.

And then we run it through case/3 and negcase/3.
And don't need an iterations deep parameter.
And iterations deep parameter is not

a solution. The predicate might internally use
such a parameter, but to the outside it should
be just a predicate falsify/1, not

more and not less.

Graham Cooper

unread,
Aug 31, 2020, 5:51:39 PM8/31/20
to
On Tuesday, September 1, 2020 at 7:44:14 AM UTC+10, Mostowski Collapse wrote:
> Show me your code for:
>
> falsify(A): The predicate succeeds if |/- A,
> i.e. if there is a counter model to A, otherwise
> the predicate fails if |- A, i.e. if the formula
> A is generally valid. There is no floundering,
> the predicate always terminates and succeeds
> or fails.
>
> And then we run it through case/3 and negcase/3.
> And don't need an iterations deep parameter.
> And iterations deep parameter is not
>
> a solution. The predicate might internally use
> such a parameter, but to the outside it should
> be just a predicate falsify/1, not
>


HERE IS THE PROLOG CODE AGAIN






********************* PROLOG CODE ***********************


t(1,1).
not(0).


if( and(X,Y) , or(X,Y) ).
if( and(not(X),Y) , or(X,Y) ).
if( and(X,not(Y)) , or(X,Y) ).
if( and(not(X),not(Y)) , not(or(X,Y)) ).

if( and(not(X),not(Y)) , not(and(X,Y)) ).
if( and(not(X),Y) , not(and(X,Y)) ).
if( and(X,not(Y)) , not(and(X,Y)) ).

if( and(X,Y) , if(X,Y) ).
if( and(not(X),not(Y)) , if(X,Y) ).
if( and(not(X),Y) , if(X,Y) ).
if( and(X,not(Y)) , not(if(X,Y)) ).

if( and(X,Y) , iff(X,Y) ).
if( and(not(X),not(Y)) , iff(X,Y) ).
if( and(not(X),Y) , not(iff(X,Y)) ).
if( and(X,not(Y)) , not(iff(X,Y)) ).


if( not(and(X,Y)) , or(not(X),not(Y)) ).
if( not(or(X,Y)) , and(not(X),not(Y)) ).
if( not(xor(X,Y)) , iff(X,Y) ).
if( not(not(X)) , X ).
if( X , not(not(X)) ).

if( and(if(A,B),if(B,C)) , if(A,C) ).
if( and(or(A,B),if(B,C)) , or(A,C) ).
if( and(and(A,B),if(B,C)) , and(A,C) ).

if( and(A,B) , and(B,A) ).
if( or(A,B) , or(B,A) ).

t(X,l(L)) :- t(X,L).

t(and(X,Y), l(L)) :- t(X,L), t(Y,L).
t(and(X,not(Y)), l(L)) :- t(X,L), not(Y).
t(and(not(X),Y), l(L)) :- not(X), t(Y,L).
t(and(not(X),not(Y)), l(L)) :- not(X), not(Y).


if( e(X,X) , e(X,sc) ).

t(e(A,B),1) :- e(A,B).


t(NEW,l(L)) :- if(OLD,NEW) , t(OLD,L).
*************************************************



WHEN you falsify an expression it uses these 2 inference rules


if( not(not(X)) , X ).
if( X , not(not(X)) ).


SO YOU GIVE IT


?-t( not( or(X,not(Y)) ) , l(l(0)) ).


and it constructs:


not( not (not(


and REDUCES that expression with MORE inference rules

That's all FALSIFY DOES!


falsify( A , l(L) ) :- t( not(A) , L ).










Mostowski Collapse

unread,
Aug 31, 2020, 5:55:40 PM8/31/20
to
You are confused.

Thats not falsification. Proving |- ~f(X1,..,Xn) is
not falsification. Look at the truth tables
of |- f(X1,..,Xn) and |- ~f(X1,..,Xn).

This is a truth table for |- f(X1,..,Xn), everything
is a one, 1:

X1 Xn f(X1,..,Xn)
0 0 1
0 1 1
..
1 0 1
1 1 1

This is a truth table for |- ~f(X1,..,Xn), everything
is a zero, 0:

X1 Xn f(X1,..,Xn)
0 0 0
0 1 0
..
1 0 0
1 1 0

Falsification means something else, means at least
one zero, it looks like this, for example:

X1 Xn f(X1,..,Xn)
0 0 1
0 1 0 /* yeah a zero, falsified */
..
1 0 1
1 1 1

Mostowski Collapse

unread,
Aug 31, 2020, 5:58:23 PM8/31/20
to
Lets repeat, this here:

/* Faux Falsify, trying to prove |- ~A */

falsify( A ) :- somedepth(L), t( not(A) , L ).

Is not falsification. It checks whether the
truth table has everywhere a zero.

But for falsification you need only tell
whether there is at least one row

in the truth table with a zero.

Graham Cooper

unread,
Aug 31, 2020, 6:08:10 PM8/31/20
to
On Tuesday, September 1, 2020 at 7:58:23 AM UTC+10, Mostowski Collapse wrote:
> Lets repeat, this here:
>
> /* Faux Falsify, trying to prove |- ~A */
>
> falsify( A ) :- somedepth(L), t( not(A) , L ).
>
> Is not falsification. It checks whether the
> truth table has everywhere a zero.
>
> But for falsification you need only tell
> whether there is at least one row
>
> in the truth table with a zero.


No it works for numbers and sub-predicates

It does the example you asked for 10 times over!


SEE www.miniBASE.com and check out the DATABASE and DOWNLOAD or GO AWAY!





Mostowski Collapse

unread,
Aug 31, 2020, 6:14:58 PM8/31/20
to
No it does not the example, because this here:

|- ~(Av~B)

Is not provable. So there are other errors as
well in your code. Its impossible that t(not(or(A,not(B)))
succeeds in anyway. Thats just nonsense.

Graham Cooper

unread,
Aug 31, 2020, 6:18:16 PM8/31/20
to
On Tuesday, September 1, 2020 at 7:58:23 AM UTC+10, Mostowski Collapse wrote:
> Lets repeat, this here:
>
>


"As test cases we first used some 6 propositional
logic non-tautologies from Fallacy Files, so as to
see whether the various methods can indeed falsify formulas."


Yes i think this works they are tautologies because they have a logical counter-example to the not( expression )

It will search through 0 s(0) s(s(0))) to find solutions & counter-examples

www.miniBASE.com

Mostowski Collapse

unread,
Aug 31, 2020, 6:19:51 PM8/31/20
to
You are highly confused.

In as far ?- t( not( and( A , not(B) ) , l(l(0)) ).
is irelevant, since I asked for these two examples
as a starter. The (+)/2 is disjunction.

> % ?- falsify(A+ ~A).
> % No
>
> % ?- falsify(A+ ~B).
> % A = 0,
> % B = 1 ;
> % No

So the question is for t(not(or(A,not(B))) and
not for t(not(and(A,not(B))) in your idea of
falsify. Besides you can also not prove ~(A&~B)

this would be equally well nonsense.

Mostowski Collapse

unread,
Aug 31, 2020, 6:23:04 PM8/31/20
to
Ok, if you come up with a complete solution,
please let us know.

Graham Cooper

unread,
Aug 31, 2020, 6:26:15 PM8/31/20
to
On Tuesday, September 1, 2020 at 8:23:04 AM UTC+10, Mostowski Collapse wrote:
> Ok, if you come up with a complete solution,
> please let us know.


my prolog VTProlog stopped running on windows
and turboprolog is expired
and miniBASE only does flat unification of table fields

i am hoping you test out the code on your prolog

why did you not test it? instead you wasted half a day telling me its no good

its the HIGHEST TECH LOGIC SOLVER!






Mostowski Collapse

unread,
Aug 31, 2020, 7:05:26 PM8/31/20
to
Well, you need to test your code by yourself.

You wrote:

> i had this working 5 years ago

So please show us, or it never happened.

Graham Cooper

unread,
Aug 31, 2020, 7:15:25 PM8/31/20
to
On Tuesday, September 1, 2020 at 9:05:26 AM UTC+10, Mostowski Collapse wrote:
> Well, you need to test your code by yourself.


I tested 5 PROLOG downloads and ONLINE PROLOG and they are all very buggy



http://mud.com/PROLOG.png

Notice the CONTRADICTION last line!








Mostowski Collapse

unread,
Aug 31, 2020, 7:50:10 PM8/31/20
to
Maybe try 10 Prolog systems and pray to mecca,
moron. BTW: This is a nice modification of Boole.
Call it Quine. Instead of falsify like this:

falsify(A) :- eval(A, B), term_variables(B, L), falsify(B, L).

falsify(0,_) :- !.
falsify(A, [0 _]) :- falsify(A), !.
falsify(A, [1|_]) :- falsify(A).

We implement prove like this:

prove(A) :- eval(A, B), term_variables(B, L), prove(B, L).

prove(1,_) :- !.
prove(A, [B|_]) :- forall((B = 0; B = 1), prove(A)).

Here is an example run:

?- prove(((P+Q)=<R)=:=((P=<R)*(Q=<R))).
(P+Q =< R) =:= (P =< R)*(Q =< R)
(0+Q =< R) =:= (0 =< R)*(Q =< R)
(0 =< R) =:= (0 =< R)
(1 =< R) =:= (1 =< R)
0 =:= 0
1 =:= 1
(1+Q =< R) =:= (1 =< R)*(Q =< R)
0 =:= 0*(Q =< 0)
1 =:= 1*(Q =< 1)
Yes /* Proof Complete */

To print the variable names, I used current_prolog_flag(
sys_print_map, N), write_term(A, [variable_names(N)]), nl .
Maybe not available in all Prolog systems.

Am Dienstag, 1. September 2020 01:15:25 UTC+2 schrieb Graham Cooper:

Graham Cooper

unread,
Aug 31, 2020, 9:06:13 PM8/31/20
to
On Tuesday, September 1, 2020 at 9:50:10 AM UTC+10, Mostowski Collapse wrote:
> Maybe try 10 Prolog systems and pray to mecca,
> moron. BTW: This is a nice modification of Boole.
> Call it Quine. Instead of falsify like this:
>
> falsify(A) :- eval(A, B), term_variables(B, L), falsify(B, L).
>
> falsify(0,_) :- !.
> falsify(A, [0 _]) :- falsify(A), !.
> falsify(A, [1|_]) :- falsify(A).
>
> We implement prove like this:
>
> prove(A) :- eval(A, B), term_variables(B, L), prove(B, L).
>
> prove(1,_) :- !.
> prove(A, [B|_]) :- forall((B = 0; B = 1), prove(A)).
>
> Here is an example run:
>
> ?- prove(((P+Q)=<R)=:=((P=<R)*(Q=<R))).
> (P+Q =< R) =:= (P =< R)*(Q =< R)
> (0+Q =< R) =:= (0 =< R)*(Q =< R)
> (0 =< R) =:= (0 =< R)
> (1 =< R) =:= (1 =< R)
> 0 =:= 0
> 1 =:= 1
> (1+Q =< R) =:= (1 =< R)*(Q =< R)
> 0 =:= 0*(Q =< 0)
> 1 =:= 1*(Q =< 1)
> Yes /* Proof Complete */
>



That is a simple proposition solver it proves nothing

you dont need FALSIFY


?- prove( not( expression ) , l(l(l(l(0)))) )

In my PROVER there are only 2 rules

prove( X , l(Z) )
:-
if( L , R ) ,
prove( L , Z ) .


prove( and( X , Y ) , l(Z) )
:-
prove( X , Z ) ,
prove( Y , Z ) .


TRY TO PROVE NOT(ALL(n) neEVENS)

MY prover will search through numbers to find a counter-example 0 , s(0) BiNGO!












Mostowski Collapse

unread,
Sep 1, 2020, 3:00:18 AM9/1/20
to
It proves that the formula is a tautology,
by reducing the given formula A to 1.

Mostowski Collapse

unread,
Sep 1, 2020, 3:01:34 AM9/1/20
to
It also always terminates, if it cannot reduce
the formula A to 1, it will answer with "No".

Graham Cooper

unread,
Sep 1, 2020, 4:19:15 AM9/1/20
to
On Tuesday, September 1, 2020 at 5:00:18 PM UTC+10, Mostowski Collapse wrote:
> It proves that the formula is a tautology,
> by reducing the given formula A to 1.

isnt that a SIMPLER class of solver

they should follow a proof by COUNTER-EXAMPLE

not(and( X , not(Y) ))

COUNTER EXAMPLE
X=1
Y=0



YOU SHOULD TRY

proof( and(A,B) , l(Z) ) :- proof(A,Z),proof(B,Z).
proof( R , l(Z) ) :- if(L,R),proof(L,Z).


O N L Y - 2 - R U L E S

WILL DO *ANY* PROOF!


www.miniBASE.com



Mostowski Collapse

unread,
Sep 1, 2020, 10:44:07 AM9/1/20
to
Whats is missing is a 3-way implementation. The 3
outcomes of predicate taut/2 are succeeds with 1,
succeeds with 0 or fails. So far we do not yet
have a predicate

taut(+Expr, -T)
If Expr is a tautology with respect to the posted
constraints, succeeds with T = 1 . If Expr cannot
be satisfied, succeeds with T = 0 . Otherwise, it fails.
https://www.swi-prolog.org/pldoc/man?section=clpb

Currently we would need to call first prove(A) and
then prove(~A). Any ideas how to do it one go? I know
how to do it in one go for Binary Decision Diagrams (BDD).

But how would you do it based on Quine, if at all?

Here are some example runs in SWI-Prolog CLP(B):

?- taut(A+ ~A, T).
T = 1.

?- taut(A* ~A, T).
T = 0.

?- taut(A+ ~B, T).
false.

Mostowski Collapse

unread,
Sep 1, 2020, 11:12:11 AM9/1/20
to
Here is some really nasty idea:

taut(A, T) :- eval(A, B), term_variables(B, L), taut(B, L, T).

taut(T, [], T) :- !.
taut(A, [B|_], T) :- catch((B = 0, taut(A, T), throw(T)), T, true),
B = 1, taut(A, S), T = S.

The catch/throw idea to undo bindings, I borrowed
from Markus Triska. We can call T = 0 by the
name antilogy. It seems to work:

?- taut(A+ ~A, T).
A+ ~A --> A+ ~A
0+ ~0 --> 1
1+ ~1 --> 1
T = 1 /* Proof Complete, Tautology */

?- taut(A* ~A, T).
A* ~A --> A* ~A
0* ~0 --> 0
1* ~1 --> 0
T = 0 /* Proof Complete, Antilogy */

?- taut(A+ ~B, T).
A+ ~B --> A+ ~B
0+ ~B --> ~B
~0 --> 1
~1 --> 0
No /* Neither Tautology nor Antilogy */

?- taut(((P+Q)=<R)=:=((P=<R)*(Q=<R)), T).
(P+Q =< R) =:= (P =< R)*(Q =< R) --> (P+Q =< R) =:= (P =< R)*(Q =< R)
(0+Q =< R) =:= (0 =< R)*(Q =< R) --> (Q =< R) =:= (Q =< R)
(0 =< R) =:= (0 =< R) --> 1
(1 =< R) =:= (1 =< R) --> R =:= R
0 =:= 0 --> 1
1 =:= 1 --> 1
(1+Q =< R) =:= (1 =< R)*(Q =< R) --> R =:= R*(Q =< R)
0 =:= 0*(Q =< 0) --> 1
1 =:= 1*(Q =< 1) --> 1
T = 1 /* Proof Complete, Tautology */

I placed the write_term/2 like this:

taut(A, T) :-
eval(A, B),
current_prolog_flag(sys_print_map, N),
write_term(A, [variable_names(N)]),
write(' --> '),
write_term(B, [variable_names(N)]),
nl,
term_variables(B, L),
taut(B, L, T).

Graham Cooper

unread,
Sep 1, 2020, 2:10:00 PM9/1/20
to
On Wednesday, September 2, 2020 at 1:12:11 AM UTC+10, Mostowski Collapse wrote:
> Here is some really nasty idea:
>
> taut(A, T) :- eval(A, B), term_variables(B, L), taut(B, L, T).
>
> taut(T, [], T) :- !.
> taut(A, [B|_], T) :- catch((B = 0, taut(A, T), throw(T)), T, true),
> B = 1, taut(A, S), T = S.


Stop wasting your time on FORMULA REDUCTION


proof( and(A,B) , l(Z) ) :- proof(A,Z),proof(B,Z).
proof( R , l(Z) ) :- if(L,R),proof(L,Z).


AND is a SEARCH BRANCHER (CARTESION JOIN of VARIABLES/BRANCHES)

proof(XandY)
:-
proof(X)
&proof(Y)


your proof search must NOT TERMINATE because the size of proofs is unbounded

so you are STUCK with depth limited (breadth first) search


then you can search both branches if you need to


(its more a user interface style - ask a positive or ask a negative but you can do this)


answer( Q , 'true' ) :-
prove( Q , l(l(l(l(l(0))))) ) <---------- terminates

answer( Q , 'false' ) :-
prove( not(Q) , l(l(l(0))) )







Mostowski Collapse

unread,
Sep 1, 2020, 2:15:27 PM9/1/20
to
Ha Ha, you ARE a moron.

This here never works in Prolog:

answer( Q , 'true' ) :- somedepth(D),
prove( Q , D )

answer( Q , 'false' ) :- somedepth(D),
prove( not(Q) , l(l(l(0))) )

Take a formula where answer is 'false'. How
deep do you want to go before you try
the second rule?

Graham Cooper

unread,
Sep 1, 2020, 2:16:34 PM9/1/20
to
On Wednesday, September 2, 2020 at 4:10:00 AM UTC+10, Graham Cooper wrote:
> On Wednesday, September 2, 2020 at 1:12:11 AM UTC+10, Mostowski Collapse wrote:
> > Here is some really nasty idea:
> >
> > taut(A, T) :- eval(A, B), term_variables(B, L), taut(B, L, T).
> >
> > taut(T, [], T) :- !.
> > taut(A, [B|_], T) :- catch((B = 0, taut(A, T), throw(T)), T, true),
> > B = 1, taut(A, S), T = S.
> Stop wasting your time on FORMULA REDUCTION
> proof( and(A,B) , l(Z) ) :- proof(A,Z),proof(B,Z).
> proof( R , l(Z) ) :- if(L,R),proof(L,Z).
> AND is a SEARCH BRANCHER (CARTESION JOIN of VARIABLES/BRANCHES)
>
> proof(XandY)
> :-
> proof(X)
> &proof(Y)
>
>
> your proof search must NOT TERMINATE because the size of proofs is unbounded


your system will not terminate given these 2 necessary inference rules

if( X , not(not(X)) )
if( not(not(X)) , X )


So you require depth limited search














Mostowski Collapse

unread,
Sep 1, 2020, 2:16:41 PM9/1/20
to
Corr.:

answer( Q , 'true' ) :- somedepth(D),
prove( Q , D ).
answer( Q , 'false' ) :- somedepth(D),
prove( not(Q) , D ).

Mostowski Collapse

unread,
Sep 1, 2020, 2:19:52 PM9/1/20
to
I dont have nonsense like this here in my system:

if( X , not(not(X)) )
if( not(not(X)) , X )

I even dont have if/2 anywhere. Whats wrong with you?

Code is here:

Prolog implementation of Quine's algorithm
https://stackoverflow.com/a/63603544/502187

Mostowski Collapse

unread,
Sep 1, 2020, 2:46:03 PM9/1/20
to
If you want to see something try this:

taut(A, T, N) :- eval(A, B),
write_term(A, [variable_names(N)]),
write(' --> '),
write_term(B, [variable_names(N)]),nl,
term_variables(B, L), taut(B, L, T, N).

taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, taut(A, T, N), throw(T)), T, true),
B = 1, taut(A, S, N), T = S.

And then call this here, passing variable names to taut:

?- read_term(A, [variable_names(N)]), taut(A, T, N).

Graham Cooper

unread,
Sep 1, 2020, 7:13:45 PM9/1/20
to
On Wednesday, September 2, 2020 at 4:19:52 AM UTC+10, Mostowski Collapse wrote:
> I dont have nonsense like this here in my system:
> if( X , not(not(X)) )
> if( not(not(X)) , X )

How do you SOLVE


?-t( iff( not(not(not(X))) , not(X) ) ).

your system will go into an infinite loop


Try www.miniBASE.com Today!







Mostowski Collapse

unread,
Sep 2, 2020, 12:15:36 PM9/2/20
to
This is yet another take, closer to Boole, and
returning a proof object. The proof object is
just a list of formulas, result of the reductions.

Quine calls it the "resolution" steps, but Boole
helps us to model the Quine split into an equational
step, so that we dont have any branching and simply

linearly progression:

judge(A, [B|R]) :- eval(A, B), term_variables(B, L), judge(B, L, R).

judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]), judge(C*D, R).

Works smooth, here are some example runs:

?- judge(A+ ~A, L).
L = [A+ ~A, 1] /* Ends in 1, Tautology */

?- judge(A+ ~B, L).
L = [A+ ~B, ~B, 0] /* Ends in 0, Falsifiable */

?- judge(((P+Q)=<R)=:=((P=<R)*(Q=<R)), L).
L = [(P+Q =< R) =:= (P =< R)*(Q =< R),
((Q =< R) =:= (Q =< R))*(R =:= R*(Q =< R)),
(R =:= R)*((R =:= R)*(R =:= R*R)), 1].

Ross A. Finlayson

unread,
Sep 2, 2020, 1:03:12 PM9/2/20
to
It reminds me of writing algorithm what to for example reduce
the factorial algorithm that is only checking indicators, to
combine them to a large serial word thusly, that though for
example maybe it's a serial word larger than the register or
vector word, what is a usual factorial algorithm runs in linear
time.

It is similar in combining cases that that are separable
besides composable thus recomposable and in a sense
embarrassingly parallel - besides what there is something like
conjunctive normal form, having a form for example with
terms that combine or recombine in terms of one combined
term instead of "branching" (branching only at the end),
is another example of efficiency in terms, in usual routine.

I.e. making the summary terms tractable is a usual memory
organization, about the balance of state and summary in store.

"Imagine a Beowulf cluster of large vector machines...."

It seems for categorizing forms by their organization.

(Logical forms.)

Here I'd arrived at for the parameter of a form, for
a query or filter, of a column attribute and match term
pair the form, then for example is that those compose to
the block parameter, and are so separable, running out each
in their linear time, making for a parallel solution.

It is a form....


Mostowski Collapse

unread,
Sep 2, 2020, 1:17:35 PM9/2/20
to
I guess the context for Quine and Boole is missing.

Methods of Logic, von W. V. Quine
https://books.google.ch/books?id=liHivlUYWcUC&lpg=PA1&ots=JLNryA81AV&dq=quine%20Methods%20of%20Logic&lr&hl=de&pg=PA34#v=onepage&q=resolution&f=false

Returning a proof, comes with some cost. At least
what we did now has an additional cost, since we
cannot use backtracking anymore.

We have two copy_term/2 and are really branching
out without any backtracking. So the costs are
as follows:

?- time(falsify( ... big formula ...)).
% Up 9 ms, GC 0 ms, Threads 8 ms (Current 09/02/20 18:54:21)
No

?- time(judge( ... big formula ..., _)).
% Up 64 ms, GC 0 ms, Threads 61 ms (Current 09/02/20 18:58:59)
Yes

The test formula is, I don't know where the
hecking formula comes from, but it seems
to be a tautology:

((( A0 =< F) * ((( B20 =< B0) =< A20) * ((( B0 =< A1) =< A0) * (
(( B1 =< A2) =< A1) * ((( B2 =< A3) =< A2) * ((( B3 =< A4) =< A3) *
((( B4 =< A5) =< A4) * ((( B5 =< A6) =< A5) * ((( B6 =< A7) =< A6)
* ((( B7 =< A8) =< A7) * ((( B8 =< A9) =< A8) * ((( B9 =< A10) =<
A9) * ((( B10 =< A11) =< A10) * ( (( B11 =< A12) =< A11) * ((( B12
=< A13) =< A12) * ((( B13 =< A14) =< A13) * ((( B14 =< A15) =< A14)
* ((( B15 =< A16) =< A15) * ((( B16 =< A17) =< A16) * ((( B17 =<
A18) =< A17) * ((( B18 =< A19) =< A18) * ((B19 =< A20) =< A19))))
)))))))))))))))))) =< F) * (((( B19 =< A20) =< A19)
* ((( B18 =< A19) =< A18) * ((( B17 =< A18) =< A17) * ((( B16 =<
A17) =< A16) * ((( B15 =< A16) =< A15) * ((( B14 =< A15) =< A14) * (
(( B13 =< A14) =< A13) * ((( B12 =< A13) =< A12) * ((( B11 =< A12)
=< A11) * ((( B10 =< A11) =< A10) * ((( B9 =< A10) =< A9) * ((( B8
=< A9) =< A8) * ((( B7 =< A8) =< A7) * ((( B6 =< A7) =< A6) * (((
B5 =< A6) =< A5) * ((( B4 =< A5) =< A4) * ((( B3 =< A4) =< A3) * ((
( B2 =< A3) =< A2) * ((( B1 =< A2) =< A1) * ((( B0 =< A1) =< A0) * (
(( B20 =< B0) =< A20) * ( A0 =< F)))))))))))))))))))))) =< F))

Mostowski Collapse schrieb:

Mostowski Collapse

unread,
Sep 2, 2020, 2:48:51 PM9/2/20
to
You need a good structure sharing Prolog to
have falsify/1 flying. Otherwise your Prolog
system might also do some copying during
backtracking. I am even not sure whether
miniKanren can do it. Many functional programming
prototypes of “logic programming” miserably fail here.

But a structure sharing Prolog has also a copy
fight to fight inside falsify/1, since eval/2
will also do a kind of copy. This could be maybe
a little be redesigned, so that sub expressions that
are not affected by simp/1 are shared instead copied.

But again a Prolog system without structure sharing
might even more miserably fail in the eval/2 predicate,
like commulating uncessary copying.

Mostowski Collapse

unread,
Sep 2, 2020, 2:50:50 PM9/2/20
to
Nothing parallel Ross the Floss, Doctor Coronaris.
It all still happens in sequential execution.

Graham Cooper

unread,
Sep 2, 2020, 2:57:11 PM9/2/20
to
On Thursday, September 3, 2020 at 2:15:36 AM UTC+10, Mostowski Collapse wrote:
> This is yet another take, closer to Boole, and
> returning a proof object. The proof object is
> just a list of formulas, result of the reductions.
>
> Quine calls it the "resolution" steps, but Boole
> helps us to model the Quine split into an equational
> step, so that we dont have any branching and simply
>
> linearly progression:
>
> judge(A, [B|R]) :- eval(A, B), term_variables(B, L), judge(B, L, R).
>

AND WHAT IS EVAL HERE?

ONLY A FOOL would implement EVAL into PROLOG

eval( *expression* )(a) --> expression(a)


in LISP eval takes a SENTENCE and runs it like a program
in PROLOG all strings are *executed*


www.miniBASE.com



Graham Cooper

unread,
Sep 2, 2020, 3:11:34 PM9/2/20
to
On Thursday, September 3, 2020 at 3:03:12 AM UTC+10, Ross A. Finlayson wrote:
> "so that we dont have any branching and simply
>
> linearly progression"
> It reminds me of writing algorithm what to for example reduce
> the factorial algorithm that is only checking indicators, to
> combine them to a large serial word thusly, that though for
> example maybe it's a serial word larger than the register or
> vector word, what is a usual factorial algorithm runs in linear
> time.

i think thats a contradiction

O(n * log(n))

will handle the large output of multiples in decimal or binary




>
> It is similar in combining cases that that are separable
> besides composable thus recomposable and in a sense
> embarrassingly parallel - besides what there is something like
> conjunctive normal form,


we dont need Quantifiers for Proof Search

USE: ALWAYS IMPLIES

@->( A , B )

ALL(X) XeODDS -> XeEVENS

@->( XeODDS , XeEVENS )



so you can FULLY PREDICATE CNF (without leading quantifiers)

Your RIGHT a trace of FACTORIAL will look similar to a PROOF SEARCH


Graham Cooper

unread,
Sep 2, 2020, 3:16:29 PM9/2/20
to
On Thursday, September 3, 2020 at 3:03:12 AM UTC+10, Ross A. Finlayson wrote:

Heres a PROOF TRACE that derived *anything* from

AXIOM TRUE
AXIOM NOT(TRUE)

EX-CONTRADICTINE QUADLIBET!

http://databasescript.com/THEOREM-PROVER.png


Mostowski Collapse

unread,
Sep 2, 2020, 3:24:26 PM9/2/20
to
Still the same as here, it didn't change:

Prolog implementation of Quine's algorithm
https://stackoverflow.com/a/63603544/502187

Ross A. Finlayson

unread,
Sep 2, 2020, 10:36:40 PM9/2/20
to
It is to check every not by checking each, but that each checks to a bit,
then the word is compared to zero. It doesn't say which checked,
only one checked. This way it is a large vector word of otherwise
a factorial rules engine. (There is a linear speedup.)

Then it is linear in the size of the large vector word, but when
that is still very much that it is a very small cost in time if that's
available in space, then though it seems a large constant, it's
this way under constant instead of being in the term factorial.

So, it is a memoryless operation, that what's otherwise there
the factorial in the count of rules (matchers) that by implementing
those also in arithmetic on the large vector word, effectively
result in a 0 or 1 bit.

There are only 5000 rules so it seems to make sense to keep up
this way a vector word of 5024 bits, that it crunches and accumulates
reducing the factorial quite a bit.

Of course if there is a new rule then it would need to fit or instead
there would have to be that the rules are constant.

This is for example running the item out over the rule-set as
if it were column-wise, what computes the word, instead of
that each of the rules is being applied to all the items as the
factorial. Seating the item or seating the rule seems for
having O(mn) that it is O(m O(n) ) or O(n O(m)), seated in
m or n, here that knowing the ruleset is constant makes for
just an example of what would be less efficient as formally
defined, the case for putting the scale of m or n into the
scale of the bounds of arithmetic, which isn't much limited
in memory with extended precision arithmetic beyond the
machine word (and particularly in vector organizations in
the machine word).

It results faster because all the rules have to be run anyway,
they're arithmetized as a constant and summed together
instead of needing to synchronize on the result or wait for
it.

(For example the numbers don't need deduplication when
the items are coded as primes, here though mostly about
indexing the attributes, each as of the items as a column
vector, mostly in example that access routine has both
implementations, of terms of branching and seating.)

Dedicating the organization of one to the other effectively
makes up for it in routine, fitting "memoryless" containers
into heap bounds, as what they use constant blocks of memory
of the machine organization in memory to thus be "timeless".

It is trading in bounds to result the speedup in the harder bound.

I keep ranting about these O(n!) -> O(n^2) these past few paragraphs.
It is some example that keeping a library, or, catalog of constants, is
for the usual advantage of indexing (or, "naming"), besides that
of course any abstract machine has a constant time operation
for some implementation of a constant distribution, besides
that there are defineable bounds, for the outside case
otherwise defined by iteration, linearly in iterators.







Ross A. Finlayson

unread,
Sep 2, 2020, 10:40:08 PM9/2/20
to
Each column's terms is combined with OR then those are combined with AND.

(That's the form, that how they're conjunctive or disjunctive, is for example
that what would usually be written "NOT A", for "A", is written as two items
in the form, instead of one, to still be able to write it out that way, the form,
using AND/OR and NOT.)

Each column's terms are combined with OR,
then those are combined with AND.

This is just a detail about search, and, organizations, making for forms.

(It's a usual form.)

Mostowski Collapse

unread,
Sep 3, 2020, 4:50:56 AM9/3/20
to
No, you dont need a normal form, like conjunctive
normal form or disjunctive normal form, to
run Quines algorithm. It could be also prohibitive

to use such forms, since sometime they tend
to explode. Quines algorithm that "resolves"
a formula doesn't use a normal form,

see ch. 1 sec. 5 for the algorithm.

Mostowski Collapse

unread,
Sep 3, 2020, 6:36:47 AM9/3/20
to
Here is a little pretty printer, making
more visible the use of this in the algorithm:

∀P^A == A[P/0]*A[P/1]

Here is an example run:

?- judge(((P+Q)=<R)=:=((P=<R)*(Q=<R)), L), pretty(L).
∀P^ ∀Q^ ∀R^((P+Q =< R) =:= (P =< R)*(Q =< R))
∀Q^ ∀R^(((Q =< R) =:= (Q =< R))*(R =:= R*(Q =< R)))
∀R^((R =:= R)*((R =:= R)*(R =:= R*R)))
1

This is the code for the pretty printer:

:- op(200, fy, ∀).

pretty([B|R]) :-
term_variables(B, L),
prenex(L, B, A),
current_prolog_flag(sys_print_map, N),
write_term(A, [variable_names(N)]), nl,
pretty(R).
pretty([]).

prenex([V|L], B, ∀V^C) :-
prenex(L, B, C).
prenex([], B, B).

Ross A. Finlayson

unread,
Sep 3, 2020, 12:49:13 PM9/3/20
to
Having the random-access model or the uniform memory instead
of for example a stack machine for counting in resources, seems to
greatly increase then for what's the usual unsettling experience that
is an introduction to an array in form terms: with the 0-based array.
The 0-based array in instruction for its definition, because the "1-based
array" or numbers of an array are so usual, there is that 0-based arrays
are unsettling. This is advised by that the zero, only means the address
offset, from the beginning of the array, that is really "array item 1".

The address offset itself or location really helps to organize data in
memory as for example sharing an address space besides relations.

Then for that later the length or number or count, isn't the last element
of the array, zero-based, that it's instead the last offset from the first,
makes for all usual tests when an iterator or counter is past the offset,
that learning why arrays in memory are zero-based instead of one-based,
is then for the point that different algorithms result.

It's a normal algorithm. (It's a form.)

I wonder they still have Iverson's APL or the original IDL system as
having the most operators in the language, where it is a heap machine.

Of course more relevant here are symbolic calculators and
proof finding and proof verifiers of the usual sort.

Flow machines in the systolic of course make for
massive wide parallel arrays in the hardware.
Free-form custom and standard logic in the integrated
circuit, make for usual power computing.


One wonders it's better to make half the register
word as state, accumulators or variables, and
half as summary, statistics, then what naturally
farm and split out tractable data, as what was
at the time the state, those for example are another
example of data structures and the simple cost of
maintenance and organization, to improve then
later what are results in partitioning (aggregation).

Of course the machine word itself and the usual
constancy of the arithmetical logic unit besides the
register and transfer operations on the words,
makes for the half-word and the "vari-parallel".

Mostowski Collapse

unread,
Sep 3, 2020, 2:35:28 PM9/3/20
to
You are highly confused.

If you use logic programming to model
Quines method, the is hardly an encounter
with a low-level machine model.

Check this out again, it is written
in Prolog. It already says Prolog in the title:

Prolog implementation of Quine's algorithm
https://stackoverflow.com/a/63603544/502187

Or you might also use functional programming,
again high-level programming:

Quine's algorithm in Haskell
http://cmsc-16100.cs.uchicago.edu/2016/Lectures/26-propositional-logic-quine-prover.php

The above says Haskell in its title.

Mostowski Collapse

unread,
Sep 3, 2020, 4:37:21 PM9/3/20
to
Here some joy of CLP(B). You can also
use it to generate truth tables:

?- use_module(library(clpb)).
true.

?- sat(~(~A + A)=:=R), labeling([A,R]),
write(A-R), nl, fail; true.
0-0
1-0
true.

So no need to graze outside of your
Prolog system. Here a bigger example:

?- sat((A=<B)*(B=<C)=:=R), labeling([A,B,C,R]),
write(A-B-C-R), nl, fail; true.
0-0-0-1
0-0-1-1
0-1-0-0
0-1-1-1
1-0-0-0
1-0-1-0
1-1-0-0
1-1-1-1
true.

labeling/1 is the analogue
to label/1 from CLP(FD).

Mostowski Collapse

unread,
Sep 4, 2020, 7:08:53 AM9/4/20
to
You are right, sometimes plain Prolog works as well
quite well. Try this here:

:- op(300, fy, ~).

or(1, _, 1).
or(0, X, X).

and(0, _, 0).
and(1, X, X).

not(0, 1).
not(1, 0).

solve(A, R) :- var(A), !, R = A.
solve(A+B, R) :- !, solve(A, X), solve(B, Y), or(X, Y, R).
solve(A*B, R) :- !, solve(A, X), solve(B, Y), and(X, Y, R).
solve(~A, R) :- !, solve(A,X), not(X,R).
solve(A, A).

falsify(A) :- solve(A, 0).

Here are example runs:

?- falsify(A+ ~A).
No

?- falsify(A+ ~B).
A = 0,
B = 1

On Monday, August 31, 2020 at 6:54:36 PM UTC+2, Graham Cooper wrote:
> On Tuesday, September 1, 2020 at 2:25:16 AM UTC+10, Mostowski Collapse wrote:
> > Pleae not, its a "checker". Iterative deepening
> > will not help you in any way at all, if the
> > search space is infinite. And usually a formula
> > has infinitely many different proofs, this
> >
> > for example the case in Hilbert Style. So before
> > you figured out that your formula hasn't
> > a proof, your system will nevertheless try
> > infinitely many proofs, in vain, and not terminate.
>
>
> You Fool!
>
> You ASKED IF ANYBODY had seen a similar proof checker that falsifies
>
> and I gave you
>
>
> ?- t( not( and( A , not(B) ) , l(l(0)) ).
>
>
> --------------------
>
>
> then you spout nonsense about your mis-understanding of depth limited proof search
>
> HINT: depth limited = BREADTH FIRST MORON
>
>
>
> you CHANGE THE PARDIGM
>
>
> DO NOT ASK - DOES X HAVE A PROOF?
>
> ASK - DOES X HAVE A PROOF IN n STEPS?
>
>
> Check out the all new www.miniBASE.com
>
> try to enter: ss gray [?]

Graham Cooper

unread,
Sep 4, 2020, 12:44:55 PM9/4/20
to
On Friday, September 4, 2020 at 9:08:53 PM UTC+10, Mostowski Collapse wrote:
> You are right, sometimes plain Prolog works as well
> quite well. Try this here:
>
> :- op(300, fy, ~).
>
> or(1, _, 1).
> or(0, X, X).


I wish they had PROLOG on WINDOWS so i could try it!

but its not real OR , or is a relation

or( X , Y ) :- prove( X )
or( X , Y ) :- prove( Y )

or using more advanced again

if( and(X,Y) , or(X,Y) ).
if( and(not(X),Y) , or(X,Y) ).
if( and(X,not(Y)) , or(X,Y) ).
if( and(not(X),not(Y)) , not(or(X,Y)) ).




>
> and(0, _, 0).
> and(1, X, X).
>
> not(0, 1).
> not(1, 0).
>
> solve(A, R) :- var(A), !, R = A.
> solve(A+B, R) :- !, solve(A, X), solve(B, Y), or(X, Y, R).
> solve(A*B, R) :- !, solve(A, X), solve(B, Y), and(X, Y, R).
> solve(~A, R) :- !, solve(A,X), not(X,R).
> solve(A, A).


Wow! but its BACK TO FRONT


prove( and( X,Y) )
:-
prove( X )
prove( Y )

this is where branches in the proof are made


Try www.miniBASE.com AGAIN !!






Mostowski Collapse

unread,
Sep 4, 2020, 2:28:55 PM9/4/20
to
Its not a prover its a model finder:

falsify(A) :- solve(A, 0).

Graham Cooper

unread,
Sep 5, 2020, 4:26:11 AM9/5/20
to
On Saturday, September 5, 2020 at 4:28:55 AM UTC+10, Mostowski Collapse wrote:
> Its not a prover its a model finder:
>
> falsify(A) :- solve(A, 0).


www.miniBASE.com
HAVE YOU TRIED miniBASE [?]

TYPE *ANYTHING* 2 - 8 words long and CLICK [ENTER] or [?]
























Mostowski Collapse

unread,
Sep 9, 2020, 11:32:50 AM9/9/20
to
Ok, here is the prover. Its just my Maslov
with an exist/2 rule. The iteration parameter
does not determine the wideness of some

variable list, but rather the number of times
the exist/2 rule is tried. Also we do not
separate literals, so that we have less parameters.

Here are some example runs:

?- prove(all(A,(A;-A))).
# existenials 0
A = '$H'(0, [])

?- prove(exist(X,all(Y,(p(X);-p(Y))))).
# existenials 0
# existenials 1
# existenials 2
Y = '$H'(0, [X])

I have named the file fitting.pl in honor of
Melvin Fitting’s heroic 1990 book. Although
its just my 1993 working paper outlook,

implemented for the first time on the
computer. Still need more testing, pretty
printing of proof tree and experimentation

with ∃* versus ∃c rule.

Source code:

Maslov Calculus over Herbrandisized Formulas
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-fitting-pl

Mostowski Collapse

unread,
Sep 9, 2020, 4:32:04 PM9/9/20
to
Yesterday nice surprise. The () block operator
introduce in release 1.4.5 can be used to read
some formulas in an Isabelle/HOL document.

case(1,'Pelletier p18',
exists y.forall x.P(y) ==> P(x)).
Etc..

The new () block operator is suitable to read
the P(y) and the P(x). It will not convert the
P Prolog variable in a 'P' Prolog atom.

We then wrote some code, that converts the
() block operator into a Prolog compound whereas
at the same time converting the P Prolog variable

into a p Prolog atom in lowercase. So we now
have the Pelletier test cases in Beckert and
Posegga operators and some new inventions:

case(1, 'Pelletier p18',
exist(A, all(B, (p(A) -: p(B))))).
Etc..

Conversion code from the formulas in an Isabelle/HOL
document to the Beckert and Posegga operators
is found at the end of the file harrison.pl.

Pelletier & Others Test Cases from Isabelle/HOL
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-harrison-pl

Pelletier & Others Test Cases from Isabelle/HOL
With Beckert and Posegga operators
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-pelletier-pl

Mostowski Collapse

unread,
Sep 13, 2020, 5:33:07 AM9/13/20
to
The new Beckert and Posegga theorem prover is
quite useful. Was wondering whether this
ex-falso-quodlibet also holds in certain

modal logics. And yes it seems so. First
there is a little translator from Description
Logic to FOL:

?- concept(∀r^(¬p) ⊑ ∀r^(p ⊑ q), X, Y).
Y = (all(_A, (r(X, _A) -: -p(_A))) -:
all(_B, (r(X, _B) -: (p(_B) -: q(_B)))))

Basically was translating ~P -> (P -> Q)
modally, using A -> B :<=> [](A => B), which
also gives ~A <=> [](-A).

And interestingly the above is provable:

?- concept(∀r^(¬p) ⊑ ∀r^(p ⊑ q), X, Y), prove(Y, 3, N).
N = 1

But ~P -> (P -> Q) fails in minimal logic. So
I guess minimal logic would need non-normal modal
logic or some such?

Mostowski Collapse

unread,
Sep 13, 2020, 5:34:56 AM9/13/20