977 views

Skip to first unread message

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.

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.

Aug 29, 2020, 11:58:27 PM8/29/20

to

* 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

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?

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?

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

Prolog Tautology Checking, who does it better?

https://qiita.com/j4n_bur53/items/28d667cf3412fa950bc7

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.

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.

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!
> 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 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 [?]

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

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.

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:
https://qiita.com/j4n_bur53/items/28d667cf3412fa950bc7

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.

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.

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

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

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

proof( expression , iterations-deep ) [?]

|- expression

where expression can begin not(expression)

SEE www.miniBASE.com

Aug 31, 2020, 5:41:55 PM8/31/20

to

|- ~A and |/- A is not the same.

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.

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.

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

>

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

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

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

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.

/* 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.

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

It does the example you asked for 10 times over!

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

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.

|- ~(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.

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:

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

www.miniBASE.com

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

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

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

www.miniBASE.com

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.

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.

Aug 31, 2020, 6:23:04 PM8/31/20

to

Ok, if you come up with a complete solution,

please let us know.

please let us know.

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
> Ok, if you come up with a complete solution,

> please let us know.

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!

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.

You wrote:

> i had this working 5 years ago

So please show us, or it never happened.

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
> Well, you need to test your code by yourself.

http://mud.com/PROLOG.png

Notice the CONTRADICTION last line!

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:

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:

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
> 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 */

>

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!

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.

by reducing the given formula A to 1.

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

the formula A to 1, it will answer with "No".

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
> It proves that the formula is a tautology,

> by reducing the given formula A to 1.

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

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.

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.

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

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

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

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

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

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

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

deep do you want to go before you try

the second rule?

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?

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

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

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

So you require depth limited search

Sep 1, 2020, 2:16:41 PM9/1/20

to

Corr.:

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

prove( Q , D ).

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

answer( Q , 'false' ) :- somedepth(D),

prove( not(Q) , D ).
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

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

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

Code is here:

Prolog implementation of Quine's algorithm

https://stackoverflow.com/a/63603544/502187

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

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

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).
write(' --> '),

write_term(B, [variable_names(N)]),nl,

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

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
> I dont have nonsense like this here in my system:

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

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

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

your system will go into an infinite loop

Try www.miniBASE.com Today!

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

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

Sep 2, 2020, 1:03:12 PM9/2/20

to

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

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:

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:

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.

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.

Sep 2, 2020, 2:50:50 PM9/2/20

to

Nothing parallel Ross the Floss, Doctor Coronaris.

It all still happens in sequential execution.

It all still happens in sequential execution.

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

>

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

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

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,

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

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

Sep 2, 2020, 3:24:26 PM9/2/20

to

Still the same as here, it didn't change:

Sep 2, 2020, 10:36:40 PM9/2/20

to

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.

Sep 2, 2020, 10:40:08 PM9/2/20

to

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

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.

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

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.

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

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

more visible the use of this in the algorithm:

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

Here is an example run:

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

Sep 3, 2020, 12:49:13 PM9/3/20

to

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

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:

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.

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:

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.

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

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

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 [?]

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 [?]

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!
> You are right, sometimes plain Prolog works as well

> quite well. Try this here:

>

> :- op(300, fy, ~).

>

> or(1, _, 1).

> or(0, X, X).

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

prove( and( X,Y) )

:-

prove( X )

prove( Y )

this is where branches in the proof are made

Try www.miniBASE.com AGAIN !!

Sep 4, 2020, 2:28:55 PM9/4/20

to

Its not a prover its a model finder:

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

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

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
> Its not a prover its a model finder:

>

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

HAVE YOU TRIED miniBASE [?]

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

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

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

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

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

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?

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?

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