# Needing help with call\_with\_depth\_limit/3 **URL:** \ **Category:** Predicate\ **Created:** [April 24, 2024, 3:00pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398 "2024-04-24T15:00:01Z")\ **Posts on this page:** 20\ **Page:** 1
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 24, 2024, 3:00pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/1 "2024-04-24T15:00:01Z")
Hello everybody, It is said about [call\_with\_depth\_limit/3](https://www.swi-prolog.org/pldoc/man?predicate=call_with_depth_limit/3) that > This predicate may be used for theorem provers to realise techniques like _iterative deepening_. The code below is a theorem prover for classical F.O.L. that is based on [Jens Otten’s work](http://www.jens-otten.de/tutorial_tableaux19/): ```prolog % --------------------------------------------------------------------------------- % leanseq.pl - A sequent calculus prover for classical F.O.L. implemented in Prolog % --------------------------------------------------------------------------------- % operator definitions (TPTP syntax) :- op( 500, fy, ~). % negation :- op(1000, xfy, &). % conjunction :- op(1100, xfy, '|'). % disjunction :- op(1110, xfy, =>). % conditional :- op(1120, xfy, <=>). % biconditional :- op( 500, fy, !). % universal quantifier: ![X]: :- op( 500, fy, ?). % existential quantifier: ?[X]: :- op( 500,xfy, :). % ----------------------------------------------------------------- decide(F) :- prove(F,_P). prove(F,P) :- time(prove(F,1,P)),nl, write('Prolog proof : '), write(P),!. prove(F,I,P) :- print(iteration:I), nl, prove([] > [F],[],I,1,_,P). prove(F,I,P) :- I1 is I+1, prove(F,I1,P). % ----------------------------------------------------------------- % THE LOGICAL RULES % 1.The axiom prove(G > D,_,_,J,J,ax(G>D, ax)) :- member(A,G), A\=(_&_), A\=(_|_), A\=(_=>_), A\=(~_), A\=(!_), A\=(?_), member(B,D), unify_with_occurs_check(A,B). % FIRST, NON-BRANCHING RULES % %% 2. Conditional on the right prove(G > D,FV,I,J,K,rcond(G>D,P)) :- select(A=>B,D,D1), !, prove([A|G] > [B|D1],FV,I,J,K,P). %% 3. Disjunction on the right prove(G > D,FV,I,J,K,ror(G>D, P)) :- select(A|B,D,D1), !, prove(G > [A,B|D1],FV,I,J,K,P). %% 4. Negation on the right prove(G > D,FV,I,J,K,rneg(G>D,P)) :- select(~A,D,D1), !, prove([A|G] > D1,FV,I,J,K,P). %% 5. Negation on the left prove(G > D,FV,I,J,K,lneg(G>D,P)) :- select(~A,G,G1), !, prove(G1 > [A|D],FV,I,J,K,P). %% 6. Conjunction on the left prove(G > D,FV,I,J,K,land(G>D,P)) :- select(A&B,G,G1), !, prove([A,B|G1] > D,FV,I,J,K,P). % SECOND, BRANCHING PROPOSITIONAL LOGIC RULES % 7. Biconditional on the right prove(G>D,FV,I,J,K, rbicond(G>D,P1,P2)):- select((A<=>B),D,D1),!, prove([A|G]>[B|D1],FV,I,J,J1,P1), prove([B|G]>[A|D1],FV,I,J1,K,P2). %% 8. Biconditional on the left prove(G>D,FV,I,J,K, lbicond(G>D, P1,P2)):- select((A<=>B),G,G1),!, prove([A,B|G1]>D,FV,I,J,J1,P1), prove(G1>[A,B|D],FV,I,J1,K,P2). %% 9. Conditional on the left prove(G > D,FV,I,J,K,lcond(G>D,P1,P2)) :- select(A=>B,G,G1), !, prove(G1 > [A|D],FV,I,J,J1,P1), prove([B|G1] > D,FV,I,J1,K,P2). %% 10. Conjunction on the right prove(G > D,FV,I,J,K,rand(G>D,P1,P2)) :- select(A&B,D,D1), !, prove(G > [A|D1],FV,I,J,J1,P1), prove(G > [B|D1],FV,I,J1,K,P2). %% 11. Disjunction on the left prove(G > D,FV,I,J,K,lor(G>D, P1,P2)) :- select(A|B,G,G1), !, prove([A|G1] > D,FV,I,J,J1,P1), prove([B|G1] > D,FV,I,J1,K,P2). %% QUANTIFICATION RULES % 12. universal quantifier on the right prove(G > D,FV,I,J,K,rall(G>D,P)) :- select((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)), J1 is J+1, prove(G > [A1|D1],FV,I,J1,K,P). % 13. existential quantifier on the left prove(G > D,FV,I,J,K,lex(G>D,P)) :- select((?[X]:A),G,G1), !, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)), J1 is J+1, prove([A1|G1] > D,FV,I,J1,K,P). % 14. existential quantifier on the right prove(G > D,FV,I,J,K,rex(G>D,P)) :- member((?[X]:A),D), \+ length(FV,I), copy_term((X:A,FV),(Y:A1,FV)), prove(G > [A1|D],[Y|FV],I,J,K,P),!. % 15. universal quantifier on the left prove(G > D,FV,I,J,K,lall(G>D,P)) :- member((![X]:A),G), \+ length(FV,I), copy_term((X:A,FV),(Y:A1,FV)), prove([A1|G] > D,[Y|FV],I,J,K,P),!. %% END of leanseq.pl code /* Example : ?- decide((![Y]:(f(Y)) => ![X]:(g(X))) <=> (?[Y]:(![X]:(f(Y) => g(X))))). iteration:1 iteration:2 % 1,235 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 827557 Lips) Prolog proof : rbicond([]>[(![_18]:f(_18)=>![_20]:g(_20)<=> ?[_18]:![_20]:(f(_18)=>g(_20)))],lcond([(![_18]:f(_18)=>![_20]:g(_20))]>[?[_18]:![_20]:(f(_18)=>g(_20))],rall([]>[![_18]:f(_18),?[_18]:![_20]:(f(_18)=>g(_20))],rex([]>[f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],rall([]>[![_520]:(f(f_sk(1,[]))=>g(_520)),f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],rcond([]>[(f(f_sk(1,[]))=>g(f_sk(2,[f_sk(1,[])]))),f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],ax([f(f_sk(1,[]))]>[g(f_sk(2,[f_sk(1,[])])),f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],ax))))),rex([![_20]:g(_20)]>[?[_18]:![_20]:(f(_18)=>g(_20))],rall([![_20]:g(_20)]>[![_836]:(f(_806)=>g(_836)),?[_18]:![_20]:(f(_18)=>g(_20))],rcond([![_20]:g(_20)]>[(f(_806)=>g(f_sk(3,[_806]))),?[_18]:![_20]:(f(_18)=>g(_20))],lall([f(_806),![_20]:g(_20)]>[g(f_sk(3,[_806])),?[_18]:![_20]:(f(_18)=>g(_20))],ax([g(f_sk(3,[_806])),f(_806),![_20]:g(_20)]>[g(f_sk(3,[_806])),?[_18]:![_20]:(f(_18)=>g(_20))],ax)))))),rcond([?[_18]:![_20]:(f(_18)=>g(_20))]>[(![_18]:f(_18)=>![_20]:g(_20))],rall([![_18]:f(_18),?[_18]:![_20]:(f(_18)=>g(_20))]>[![_20]:g(_20)],lex([![_18]:f(_18),?[_18]:![_20]:(f(_18)=>g(_20))]>[g(f_sk(4,[]))],lall([![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[g(f_sk(4,[]))],lcond([(f(f_sk(5,[]))=>g(f_sk(4,[]))),![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[g(f_sk(4,[]))],lall([![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[f(f_sk(5,[])),g(f_sk(4,[]))],ax([f(f_sk(5,[])),![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[f(f_sk(5,[])),g(f_sk(4,[]))],ax)),ax([g(f_sk(4,[])),![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[g(f_sk(4,[]))],ax))))))) true. */ ``` Unfortunately, when formula F is invalid, we get this : ```prolog ?- decide(a). iteration:1 iteration:2 iteration:3 iteration:4 iteration:5 iteration:6 iteration:7 iteration:8 iteration:9 iteration:10 iteration:11 iteration:12 iteration:13 iteration:14 iteration:15 iteration:16 iteration:17 iteration:18 iteration:19 iteration:20 iteration:21 iteration:22 iteration:23 iteration:24 iteration:25 iteration:26 iteration:27 iteration:28 iteration:29 iteration:30 iteration:31 iteration:32 iteration:33 . . . ``` It would be a nice improvement either to limit the iteration (with [call\_with\_depth\_limit/3](https://www.swi-prolog.org/pldoc/man?predicate=call_with_depth_limit/3)?, or (better), to generate a countermodel. Unfortunately, I succeed to do neither the former nor the latter. Your help is welcome. All the best, Jo. PS: Once this problem solved, my goal will be to get a pretty printing with bussproofs.sty to show the output with MathJax 3. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 24, 2024, 4:02pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/3 "2024-04-24T16:02:17Z")
I have checked that the antisequent trick used this prover for classical propositional logic [https://vidal-rosset.net/sequent\_calculus\_prover\_with\_antisequents\_for\_classical\_propositional\_logic.html](https://vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html) unfortunately does not work with this FOL prover. [https://www.umsu.de/trees/](https://www.umsu.de/trees/) also gives countermodels for invalid FOL formulas. The other solution would be to limit the proof search with an adequate built-in predicate, like [call\_with\_depth\_limit/3](https://www.swi-prolog.org/pldoc/man?predicate=call_with_depth_limit/3) . But I did not succeed to do it. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 25, 2024, 8:25am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/5 "2024-04-25T08:25:22Z")
> [@anon95304481](#): > > [call\_with\_depth\_limit/3](https://www.swi-prolog.org/pldoc/doc_for?object=call_with_depth_limit/3) cannot do that. [call\_with\_depth\_limit/3](https://www.swi-prolog.org/pldoc/doc_for?object=call_with_depth_limit/3) doesn’t > provide you a **separate algorithm** different from the calculus at hand. Yes, I am aware of this point, but the first goal for me was to ban the indefinite iteration and I just thought about this solution that works, changing clauses 4 and 5 of this prover: ```prolog prove(F,I,P) :- I < 20, print(iteration:I), nl, prove([] > [F],[],I,1,_,P). prove(F,I,P) :- I1 is I+1, I1 < 20, prove(F,I1,P). ``` It is a reasonable limit: ```prolog ?- decide((![X]:(?[Y]:(f(X,Y)))) => (?[Y]:(![X]:(f(X,Y))))). iteration:1 iteration:2 iteration:3 iteration:4 iteration:5 iteration:6 iteration:7 iteration:8 iteration:9 iteration:10 iteration:11 iteration:12 iteration:13 iteration:14 iteration:15 iteration:16 iteration:17 iteration:18 iteration:19 % 14,369,992 inferences, 1.392 CPU in 1.402 seconds (99% CPU, 10325074 Lips) false. ``` ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 25, 2024, 8:27am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/6 "2024-04-25T08:27:00Z")
> [@anon95304481](#): > > You can imagine a finite model finder as a [Quine algorithm](https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830/67), whereas > a 1st order Quine algorithm takes a propositional variable P and assigns > it 0 or 1. A FOL Quine algorithm takes a predicate variable P of arity n. Thanks for this interesting suggestion. I will try to do this. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 27, 2024, 8:25am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/8 "2024-04-27T08:25:28Z")
My difficulties are more in the practice of Prolog coding than in understanding mathematical logic (here Skolem transformations). In the same way, I met difficulties yesterday with the pretty printing to get the LaTeX bussproofs translation of the Prolog output. It works with in the propositional case, not in FOL… About coding the Quine algorithm, I guess that this [prolog program](https://www.vidal-rosset.net/quine/) makes the job and that you know his author. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [April 27, 2024, 12:39pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/9 "2024-04-27T12:39:13Z")
It’s good to know person interested in (deprecated ? ) `call_with_depth_limit`. I found all of old Prolog codes of mine on “Ordered Linear with Ancestor resolution” prover were broken, which used the `call_with_depth_limit`. So I got curious of writing a (toy) simple-minded resolution prover, which is based on: - iterated deepening ( hand made on simple limited purpose ). - prolog like proof search: - history of literals relolved upon (tabling ?). Fortunately, functionality of my old codes was fully recovered. some example queries follows. ```prolog % Valid formula. % ?- F = (all(y, f(y)==p) == (p==all(x, f(x)))), prove(F). % ?- F = (((f(1)==p) & (f(2) == p)) == (p== (f(1) & f(2)))), prove(F). % ?- F = (all(A, p==f(A))==(p==all(B, f(B)))), prove(F). % ?- F = ((p == all(A, f(A))) == all(B, p== f(B))), prove(F). % ?- F = ((p == all(A, f(A))) -> all(B, p -> f(B))), prove(F). % ?- F = ((p == all(A, f(A))) -> all(B, f(B) -> p)), prove(F). % ?- F = ((p == all(A, f(A))) -> all(B, p -> f(B))), prove(F). % ?- F = ((p == all(A, f(A))) -> all(B, f(B) -> p)), prove(F). % Invalid formula. % ?- prove(all(y, some(x, f(x, y)) -> some(x, all(y, f(x, y))))). % false % ?- prove((all(X, some(Y, p(X, Y)))->some(Y, all(X, p(X, Y))))). % false. % ?- prove((some(X, p(X))->all(X, p(X)))). % false. ``` However new codes lacks anything like paramodulation strategy, for which I have no idea (sigh). So, to prove properties on functions on natural number, for example, it must be very weak. BTW, I have tried to upload my pack pac as v1.8.9 with this new codes, but failed. It seems that packages manager has been changed. ---
**Author:** ![mgondan1](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/mgondan1/32/803_2.png) [@mgondan1](https://swi-prolog.discourse.group/u/mgondan1)\ **Post date:** [April 27, 2024, 5:24pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/10 "2024-04-27T17:24:46Z")
> [@joseph-vidal-rosset](#): > > Once this problem solved, my goal will be to get a pretty printing with bussproofs.sty to show the output with MathJax 3. This is actually on the way, not yet 100% done, but very promising already. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 28, 2024, 7:13am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/13 "2024-04-28T07:13:14Z")
> [@anon95304481](#): > > This is what Wolfgang Schwarz uses. I do not propose a model > finder with anything Skolem functions. You must be mistaken. > Its much much more trivial, the domain expansion I propose. This misunderstanding is explained by the fact that Skolem function are also used in [Jens Otten’s prover](http://www.jens-otten.de/tutorial_tableaux19/slides/prover_tutorial_TABLEAUX19_2.pdf): > rules for Eigenvariables using Skolemization [rules E left and A right] But [seqprover.pl](https://gitlab.com/cspsat/seqprover-gitpod), the classical sequent calculus prover (akin to **LK** ) by Naoyuki Tamura [Naoyuki Tamura](https://www.researchgate.net/profile/Naoyuki-Tamura) maybe fits with your point of view. See its code where [ground/1](https://www.swi-prolog.org/pldoc/man?predicate=ground/1) is used. I feel free to paste seqprover.pl here, even if it contains many lines of Prolog code. It works perfectly with SWI Prolog. The LaTeX macro that is used is [proof.sty](https://www.math.mcgill.ca/rags/texmacros/proof.sty) but it is probably possible to rewrite this part to use [bussproofs.sty](https://ctan.org/pkg/bussproofs?lang=en) instead. ```prolog %%% %%% Sequent Calculus Prover in Prolog %%% by Naoyuki Tamura (tamura@kobe-u.ac.jp) %%% TeX form output by Eiji Sugiyama %%% %%% You can freely distribute or modify this program. %%% %%% Version 2.0 %%% 12/30/2020 Modified for SWI Prolog %%% :- dynamic seq_system/2, threshold/1, output_form/1, logging/2, output_count/1, output_result/2, proved/3, not_proved/2, axiom/1. %seq_system(cl,first). %threshold(5). %output_form(pretty). %logging(no, _). %output_count(1). :- op(1200, xfx, [-->, <-->]). :- op( 900, xfy, [->]). % :- op( 850, xfy, [->]). :- op( 850, xfy, [/\, \/]). :- op( 800, fy, [~]). :- op( 750, xfy, [@, #]). prover :- writex('Sequent Calculus Prover ver 2.0 in Prolog'), nlx, writex(' by Naoyuki Tamura (tamura@kobe-u.ac.jp)'), nlx, % seq_init, statistics(runtime, [T0,_]), seq_prover, statistics(runtime, [T1,_]), T is T1-T0, writex('Exit from Sequent Calculus Prover...'), nlx, writex('Total CPU time = '), writex(T), writex(' msec.'), nlx, log_end. seq_init :- set_system(cl,first), set_threshold(5), set_axioms([]), set_output_form(pretty), log_end, reset_output_result. seq_prover :- current_input(STR), seq_prover(STR). seq_prover(STR) :- prompt(_, ''), repeat, seq_system(Sys, Opt), writex(Sys), writex('('), writex(Opt), writex(')'), writex('> '), flush_out, readx(STR, X), seq_command(X), seq_quit(X), close(STR). seq_quit(X) :- nonvar(X), memberq(X, [quit, end, bye, halt, end_of_file]). seq_command(X) :- seq_execute(X), !, writex(yes), nlx. seq_command(_) :- writex(no), nlx. seq_execute(X) :- var(X), !, fail. seq_execute(X) :- seq_quit(X), !. seq_execute(help) :- !, seq_help. seq_execute(init) :- !, seq_init. seq_execute([File]) :- !, seq_consult(File). seq_execute(cl(Opt)) :- !, set_system(cl,Opt). %seq_execute(il(Opt)) :- !, set_system(il,Opt). seq_execute(threshold(N)) :- var(N), !, threshold(N), writex(threshold(N)), nlx. seq_execute(threshold(N)) :- !, set_threshold(N). seq_execute(axioms(As)) :- var(As), !, (bagof(A, axiom(([]-->[A])), As); As=[]), !, writex(axioms(As)), nlx. seq_execute(axioms(As)) :- !, set_axioms(As). seq_execute(output(Form)) :- var(Form), !, output_form(Form), writex(output(Form)), nlx. seq_execute(output(Form)) :- set_output_form(Form). seq_execute(log(File)) :- var(File), !, logging(File, _), writex(log(File)), nlx. seq_execute(log(no)) :- !, log_end. seq_execute(log(File)) :- !, log_start(File). seq_execute(N) :- integer(N), !, get_output_result(N, N1, P), print_output(N1, P). seq_execute((Xs <--> Ys)) :- !, seq_execute((Xs --> Ys)), seq_execute((Ys --> Xs)). seq_execute((Xs --> Ys)) :- convert_to_seq((Xs --> Ys), Seq), sequentq(Seq), !, seq_prove(Seq). seq_execute(X) :- writex('Error '), writex(X), writex(' is not a command nor a sequent.'), nlx. seq_help :- writex('A1,...,Am --> B1,...,Bn : Try to prove the sequent.'), nlx, writex('A1,...,Am <--> B1,...,Bn : Try to prove the sequent '), writex('in both directions.'), nlx, writex('help : Help.'), nlx, writex('init : Initialize the prover.'), nlx, writex('[File] : Read from the file.'), nlx, writex('Sys(Opt) : Select the system. '), writex('Sys={cl}, Opt={first|prop}'), nlx, writex('threshold(N) : Set/retrieve the threshold. N>=0'), nlx, writex('axioms(Axioms) : Set/retrieve the axioms. '), writex('Axioms=[A1,...,Am]'), nlx, writex('output(Form) : Set/retrieve the output form. '), writex('Form={pretty|tex|standard|term}'), nlx, writex('log(L) : Start/stop/retrieve the output logging. '), writex('L={yes|File|no}'), nlx, writex('N : Display the N-th output.'), nlx, writex('quit : Quit.'), nlx. seq_consult(File) :- open(File, read, STR), seq_prover(STR). seq_prove(Seq) :- statistics(runtime,[_,_]), prove(Seq, Proof), statistics(runtime,[_,Time]), writex('Succeed in proving '), write_seq(Seq), writex(' ('), writex(Time), writex(' msec.)'), nlx, output_count(N), assert_output_result(Proof), !, print_output(N, Proof). seq_prove(Seq) :- statistics(runtime,[_,Time]), writex('Fail to prove '), write_seq(Seq), writex(' ('), writex(Time), writex(' msec.)'), nlx. print_output(N, P) :- output_form(Form), writex(Form), writex(':'), writex(N), writex(' ='), nlx, print_proof(P). print_proof(P) :- output_form(Form), print_proof_form(Form, P). print_proof_form(pretty, P) :- !, pretty_print(P). print_proof_form(tex, P) :- !, tex_print(P). print_proof_form(standard, P) :- !, standard_print(P). print_proof_form(term, P) :- !, writex(P), nlx. set_system(Sys, Opt) :- memberq(Sys, [cl]), memberq(Opt, [prop,first]), retractall(seq_system(_,_)), assert(seq_system(Sys,Opt)). set_threshold(N) :- integer(N), N >= 0, retractall(threshold(_)), assert(threshold(N)). set_axioms(Axioms) :- retractall(axiom(_)), assert_axioms(Axioms). assert_axioms([]). assert_axioms([A|As]) :- formulaq(A), !, assert(axiom(([]-->[A]))), assert_axioms(As). assert_axioms([A|As]) :- writex('Error '), writex(A), writex(' is not a formula.'), nlx, assert_axioms(As). set_output_form(Form) :- memberq(Form, [pretty, tex, standard, term]), retractall(output_form(_)), assert(output_form(Form)). reset_output_result :- retractall(output_count(_)), retractall(output_result(_,_)), assert(output_count(1)). assert_output_result(P) :- output_count(N), assert(output_result(N,P)), retractall(output_count(_)), N1 is N+1, assert(output_count(N1)). get_output_result(N, N, P) :- N>0, !, output_result(N, P). get_output_result(N, N1, P) :- output_count(M), N1 is M+N, output_result(N1, P). convert_to_seq((Xs --> Ys), (Xs1 --> Ys1)) :- convert_to_list(Xs, Xs1), convert_to_list(Ys, Ys1). convert_to_list(X, _) :- var(X), !, fail. convert_to_list([], []) :- !. convert_to_list([X|Xs], [X|Xs]) :- !. convert_to_list((X,Xs), [X|Zs]) :- !, convert_to_list(Xs, Zs). convert_to_list(X, [X]). sequentq((X-->Y)) :- formula_listq(X), formula_listq(Y). formula_listq([]). formula_listq([A|As]) :- formulaq(A), formula_listq(As). formulaq(A) :- var(A), !, fail. formulaq((_-->_)) :- !, fail. formulaq([]) :- !, fail. formulaq([_|_]) :- !, fail. formulaq(~A) :- !, formulaq(A). formulaq(A/\B) :- !, formulaq(A), formulaq(B). formulaq(A\/B) :- !, formulaq(A), formulaq(B). formulaq(A->B) :- !, formulaq(A), formulaq(B). formulaq(_X@A) :- !, formulaq(A). formulaq(_X#A) :- !, formulaq(A). formulaq(_). %% %% Sequent Calculus Prover %% %% seq_system( {cl}, {prop|first} ). %% seq_system(cl,first). %% Max number of cut and contraction rules: cut, r(all), l(exists) %% threshold(5). %% Axioms %% axiom(Ax1). axiom(Ax2). .... prove(S, P) :- retractall(proved(_,_,_)), retractall(not_proved(_,_)), threshold(N), writex('Trying to prove with threshold ='), for(I, 0, N), writex(' '), writex(I), flush_out, prove(S, P, I), nlx, !. prove(_S, _P) :- nlx, fail. prove(S, _P, N) :- ground(S), clause(not_proved(S,M), _), N =< M, !, fail. prove(S, P, N) :- ground(S), clause(proved(S,P,M), _), M =< N, !. prove(S, P, _N) :- clause(axiom(S), _), P = [axiom,[[]],S], !. prove(S, P, N) :- check_sequent(S), select_rule(Rule, S, Ss, Pos), P = [Rule,Pos,S|Ps], set_sequents(Ss, Ps), rule_constraint(Rule, Ps, M), N1 is N-M, N1 >= 0, prove_all(Ss, Ps, N1), % !, assert(proved(S,P,N)). prove(S, _P, N) :- ground(S), assert(not_proved(S,N)), !, fail. prove_all([], [], _N). prove_all([S|Ss], [P|Ps], N) :- prove(S, P, N), prove_all(Ss, Ps, N). check_sequent((X-->Y)) :- length(X, N1), length(Y, N2), N1 + N2 < 20. %check_sequent(_) :- seq_system(cl,_), !. %check_sequent((_X-->Y)) :- (Y=[]; Y=[_]), !. select_rule(Rule, S, Ss, Pos) :- rule(RuleSys, inv, Rule, S, Ss, Pos), check_rule(RuleSys), !. select_rule(Rule, S, Ss, Pos) :- rule(RuleSys, no, Rule, S, Ss, Pos), check_rule(RuleSys). check_rule([RSys,ROp]) :- seq_system(Sys, Op), check_rule1(Sys, RSys), check_rule2(Op, ROp), !. check_rule1(Sys, Sys). check_rule1(cl, _). check_rule2(Op, Op). check_rule2(first, _). set_sequents([], []). set_sequents([S|Ss], [[_,_,S|_]|Ps]) :- set_sequents(Ss, Ps). rule_constraint(cut, [P1,_P2], 1) :- !, axiom(S1), P1 = [axiom,_,S1]. % bug report from Joseph Vidal-Rosset rule_constraint(l(all), [P1], 1) :- !, P1 = [NextRule,_,_|_], dif(NextRule, l(all)). rule_constraint(r(exists), [P1], 1) :- !, P1 = [NextRule,_,_|_], dif(NextRule, r(exists)). rule_constraint(_Rule, _, 0). % Logical axiom % cannot be invertible owing to unification rule([cl,prop], no, ax, S, [], [[]]) :- match(S, ([_X1,[A],_X2]-->[_Y1,[A],_Y2])). % Rules for the propositional constants rule([cl,prop], inv, l(top), S, [S1], [l(N),[]]) :- match(S, ([X1,[top],X2]-->[Y])), match(S1, ([X1,X2]-->[Y])), length(X1, N). rule([cl,prop], inv, r(top), S, [], [r(N)]) :- match(S, ([_X]-->[Y1,[top],_Y2])), length(Y1, N). rule([cl,prop], inv, l(bot), S, [], [r(N)]) :- match(S, ([X1,[bot],_X2]-->[_Y])), length(X1, N). rule([cl,prop], inv, r(bot), S, [S1], [r(N),[]]) :- match(S, ([X]-->[Y1,[bot],Y2])), match(S1, ([X]-->[Y1,Y2])), length(Y1, N). % Rules for the propositional connectives rule([cl,prop], inv, l(~), S, [S1], [l(N),r(0)]) :- match(S, ([X1,[(~A)],X2]-->[Y])), match(S1, ([X1,X2]-->[[A],Y])), length(X1, N). rule([cl,prop], inv, r(~), S, [S1], [r(N),l(0)]) :- match(S, ([X]-->[Y1,[~A],Y2])), match(S1, ([[A],X]-->[Y1,Y2])), length(Y1, N). rule([cl,prop], inv, l(/\), S, [S1], [l(N),[l(N),l(N1)]]) :- match(S, ([X1,[A/\B],X2]-->[Y])), match(S1, ([X1,[A,B],X2]-->[Y])), length(X1, N), N1 is N+1. rule([cl,prop], inv, r(\/), S, [S1], [r(N),[r(N),r(N1)]]) :- match(S, ([X]-->[Y1,[A\/B],Y2])), match(S1, ([X]-->[Y1,[A,B],Y2])), length(Y1, N), N1 is N+1. rule([cl,prop], inv, r(->), S, [S1], [r(N),[l(0),r(N)]]) :- match(S, ([X]-->[Y1,[A->B],Y2])), match(S1, ([[A],X]-->[Y1,[B],Y2])), length(Y1, N). rule([cl,prop], inv, r(/\), S, [S1, S2], [r(N),r(N),r(N)]) :- match(S, ([X]-->[Y1,[A/\B],Y2])), match(S1, ([X]-->[Y1,[A],Y2])), match(S2, ([X]-->[Y1,[B],Y2])), length(Y1, N). rule([cl,prop], inv, l(\/), S, [S1, S2], [l(N),l(N),l(N)]) :- match(S, ([X1,[A\/B],X2]-->[Y])), match(S1, ([X1,[A],X2]-->[Y])), match(S2, ([X1,[B],X2]-->[Y])), length(X1, N). rule([cl,prop], inv, l(->), S, [S1, S2], [l(N),r(0),l(N)]) :- match(S, ([X1,[A->B],X2]-->[Y])), match(S1, ([X1,X2]-->[[A],Y])), match(S2, ([X1,[B],X2]-->[Y])), length(X1, N). % Rules for the quantifiers rule([cl,first], no, l(all), S, [S1], [l(N),[l(N),l(N1)]]) :- match(S, ([X1,[V@A],X2]-->[Y])), substitute(V, _V1, A, A1), match(S1, ([X1,[A1,V@A],X2]-->[Y])), length(X1, N), N1 is N+1. rule([cl,first], no, r(all), S, [S1], [r(N),r(N)]) :- match(S, ([X]-->[Y1,[V@A],Y2])), substitute(V, V1, A, A1), match(S1, ([X]-->[Y1,[A1],Y2])), eigen_variable(V1, S), length(Y1, N). rule([cl,first], no, l(exists), S, [S1], [l(N),l(N)]) :- match(S, ([X1,[V#A],X2]-->[Y])), substitute(V, V1, A, A1), match(S1, ([X1,[A1],X2]-->[Y])), eigen_variable(V1, S), length(X1, N). rule([cl,first], no, r(exists), S, [S1], [r(N),[r(N),r(N1)]]) :- match(S, ([X]-->[Y1,[V#A],Y2])), substitute(V, _V1, A, A1), match(S1, ([X]-->[Y1,[A1,V#A],Y2])), length(Y1, N), N1 is N+1. % Cut rule rule([cl,prop], no, cut, S, [S1, S2], [[],r(0),l(0)]) :- match(S, ([X]-->[Y])), match(S1, ([]-->[[C]])), match(S2, ([[C],X]-->[Y])). match((X-->Y), (P-->Q)) :- append_all(P, X), append_all(Q, Y). eigen_variable(V, X) :- freeze(V, fail), free_variables(X, Us), dif_list(Us, V). free_variables(X, Vs) :- free_vars(X, [], [], Vs). free_vars(X, BVs, Vs0, Vs) :- var(X), !, free_vars1(X, BVs, Vs0, Vs). free_vars(X, _BVs, Vs, Vs) :- ground(X), !. free_vars([X|Y], BVs, Vs0, Vs) :- !, free_vars(X, BVs, Vs0, Vs1), free_vars(Y, BVs, Vs1, Vs). free_vars(all(X,A), BVs, Vs0, Vs) :- !, free_vars(A, [X|BVs], Vs0, Vs). free_vars(exists(X,A), BVs, Vs0, Vs) :- !, free_vars(A, [X|BVs], Vs0, Vs). free_vars(X, BVs, Vs0, Vs) :- X =.. Y, free_vars(Y, BVs, Vs0, Vs). free_vars1(X, BVs, Vs, Vs) :- (memq(X, BVs); memq(X, Vs)), !. free_vars1(X, _BVs, Vs, [X|Vs]). dif_list([], _). dif_list([U|Us], V) :- dif(U, V), dif_list(Us, V). %% %% Standard form printer %% standard_print(P) :- standard_print(P, 0). standard_print([Rule,_,S|Ps], Tab) :- tabx(Tab), write_rule_name(Rule), writex(': '), write_seq(S), nlx, Tab1 is Tab+2, standard_print_list(Ps, Tab1). standard_print_list([], _). standard_print_list([P|Ps], Tab) :- standard_print(P, Tab), standard_print_list(Ps, Tab). %% %% Pretty form printer %% pretty_print(P0) :- name_variables(P0, P), place_proof(P, [], Q, _, _), print_placed_proof(Q), fail. pretty_print(_). name_variables(X, Z) :- name_variables(X, 0, _N, [], _Vs, Z). name_variables(X, N, N, Vs, Vs, X) :- ground(X), !. name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !. name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !, V is N0 mod 3, VN is N0//3, name_var(V, VN, Z), N is N0+1. name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !, name_variables(X, N0, N1, Vs0, Vs1, Z), name_variables(Xs, N1, N, Vs1, Vs, Zs). name_variables(X, N0, N, Vs0, Vs, Z) :- X =.. Xs, name_variables(Xs, N0, N, Vs0, Vs, Zs), Z =.. Zs. name_var(0, VN, X) :- !, name_var1([0'X], VN, X). name_var(1, VN, X) :- !, name_var1([0'Y], VN, X). name_var(2, VN, X) :- !, name_var1([0'Z], VN, X). name_var1([V], 0, X) :- !, name(X, [V]). name_var1([V], VN, X) :- name(VN, Ns), name(X, [V|Ns]). %% %% place_proof(+Proof, +Margins, %% -Proof_with_pos, -LowerLeftPos, -NewMargins) %% place_proof([Rule,_,S|Ps1], Ms0, Q, LowerPos, Ms) :- get_margins([M0,M1|Ms1], Ms0), place_uppers(Ps1, Ms1, Ps2, UpperPos0, Ms2), get_margins([M2|_], Ms2), UpperWidth is M2-UpperPos0, get_rule_name_width(Rule, W1), get_seq_width(S, LowerWidth), LowerOff is max(0,max(UpperPos0,max(M1,M0))-UpperPos0), RulePos is UpperPos0+LowerOff, RuleWidth is max(UpperWidth,LowerWidth), LowerPos is RulePos+(RuleWidth-LowerWidth)//2, UpperPos is max(UpperPos0,RulePos), UpperOff is UpperPos-UpperPos0, move_proof_list(Ps2, UpperOff, Ps3), move_margins(Ms2, UpperOff, Ms3), new_rule_width(Rule, RuleWidth, W1, RuleWidth1, W2), Q = [RulePos+RuleWidth1,Rule,LowerPos+LowerWidth,S|Ps3], M11 is RulePos+RuleWidth1+W2, M01 is LowerPos+LowerWidth, Ms = [M01,M11|Ms3]. new_rule_width([_Rule,_], _, W1, 0, W1) :- !. new_rule_width(_Rule, RW, W1, RW, W2) :- W2 is W1+1. place_uppers(Ps, Ms0, Qs, T, Ms) :- place_proof_list(Ps, Ms0, Qs, T, Ms). place_proof_list([], Ms0, [], T, Ms0) :- !, get_margins([T|_], Ms0). place_proof_list([P1], Ms0, [Q1], T, Ms) :- !, place_proof(P1, Ms0, Q1, T, Ms). place_proof_list([P1|Ps], Ms0, [Q1|Qs], T, Ms) :- place_proof(P1, Ms0, Q1, T, Ms1), move_margins(Ms1, 2, Ms2), place_proof_list(Ps, Ms2, Qs, _T1, Ms). move_proof_list([], _, []). move_proof_list([P0|Ps0], Off, [P|Ps]) :- move_proof(P0, Off, P), move_proof_list(Ps0, Off, Ps). move_proof([M0+W0,Rule,M1+W1,S|Ps0], Off, [N0+W0,Rule,N1+W1,S|Ps]) :- N0 is M0+Off, N1 is M1+Off, move_proof_list(Ps0, Off, Ps). get_margins(Zs, Xs) :- var(Zs), !, Zs=Xs. get_margins([], _). get_margins([Z|Zs], []) :- !, Z=0, get_margins(Zs, []). get_margins([Z|Zs], [Z|Xs]) :- get_margins(Zs, Xs). move_margins([], _, []). move_margins([M0|Ms0], Off, [M|Ms]) :- M is M0+Off, move_margins(Ms0, Off, Ms). %% %% print_placed_proof(+Placed_Proof) %% print_placed_proof(P) :- print_placed_proofs([P]). print_placed_proofs([]). print_placed_proofs(Ps) :- Ps=[_|_], gather_uppers(Ps, Qs), print_placed_proofs(Qs), print_rules(Ps), nlx, print_lowers(Ps), nlx. gather_uppers([], []). gather_uppers([P|Ps], Qs) :- gather_uppers(Ps, Qs1), P = [_,_Rule,_,_S|P0], append(P0, Qs1, Qs). print_rules([]). print_rules([P|Ps]) :- P = [M0+W0,Rule,_M1+_W1,_S|_], goto_pos(M0), print_rule_line(W0), write_rule_name(Rule), print_rules(Ps). print_rule_line(0) :- !. print_rule_line(N) :- N>0, n_writex(N, '-'), writex(' '). print_lowers([]). print_lowers([P|Ps]) :- P = [_M0+_W0,_Rule,M1+_W1,S|_], goto_pos(M1), write_seq(S), print_lowers(Ps). get_width(X, W) :- open_null(NULL, OldSTR, OldLog), nlx, writex(X), line_position(W), close_null(NULL, OldSTR, OldLog). get_rule_name_width(R, W) :- open_null(NULL, OldSTR, OldLog), nlx, write_rule_name(R), line_position(W), close_null(NULL, OldSTR, OldLog). get_seq_width(S, W) :- open_null(NULL, OldSTR, OldLog), nlx, write_seq(S), line_position(W), close_null(NULL, OldSTR, OldLog). open_null(NULL, OldSTR, OldLog) :- current_output(OldSTR), open_null_stream(NULL), set_output(NULL), log_suspend(OldLog). close_null(NULL, OldSTR, OldLog) :- close(NULL), set_output(OldSTR), log_resume(OldLog). write_rule_name(axiom) :- !, writex('Axiom'). write_rule_name(ax) :- !, writex('Ax'). write_rule_name(cut) :- !, writex('Cut'). write_rule_name(r(all)) :- !, writex('R@'). write_rule_name(r(exists)) :- !, writex('R#'). write_rule_name(r(R)) :- !, writex('R'), writex(R). %write_rule_name(r(R,N)) :- !, writex('R'), writex(R), writex(N). write_rule_name(l(all)) :- !, writex('L@'). write_rule_name(l(exists)) :- !, writex('L#'). write_rule_name(l(R)) :- !, writex('L'), writex(R). %write_rule_name(l(R,N)) :- !, writex('L'), writex(R), writex(N). write_seq((Xs-->Ys)) :- write_list(Xs), writex(' --> '), write_list(Ys). write_list([]). write_list([X]) :- !, writex(X). write_list([X|Xs]) :- writex(X), writex(','), write_list(Xs). %% %% Tex form printer %% tex_print(P) :- tex_name_variables(P, Q), tex_print(0, Q). tex_name_variables(X, Z) :- tex_name_variables(X, 0, _N, [], _Vs, Z). tex_name_variables(X, N, N, Vs, Vs, X) :- ground(X), !. tex_name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !. tex_name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !, V is N0 mod 3, VN is N0//3, tex_name_var(V, VN, Z), N is N0+1. tex_name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !, tex_name_variables(X, N0, N1, Vs0, Vs1, Z), tex_name_variables(Xs, N1, N, Vs1, Vs, Zs). tex_name_variables(X, N0, N, Vs0, Vs, Z) :- X =.. Xs, tex_name_variables(Xs, N0, N, Vs0, Vs, Zs), Z =.. Zs. tex_name_var(0, VN, X) :- !, tex_name_var1([0'x], VN, X). tex_name_var(1, VN, X) :- !, tex_name_var1([0'y], VN, X). tex_name_var(2, VN, X) :- !, tex_name_var1([0'z], VN, X). tex_name_var1([V], 0, X) :- !, name(X, [V]). tex_name_var1([V], VN, X) :- name(VN, Ns), append(Ns, [0'}], Ns1), name(X, [V,0'_,0'{|Ns1]). tex_print(Tab, [[Rule,LN],_,S]) :- !, tabx(Tab), writex('\\deduce{'), tex_print_sequent(S), writex('}{'), tex_print_rule_name([Rule,LN]), writex('}'), nlx. tex_print(Tab, [Rule,_,S]) :- (Rule = ax; Rule = axiom), !, tabx(Tab), tex_print_sequent(S). tex_print(Tab, [Rule,_,S|Ss]) :- tabx(Tab), writex('\\infer['), tex_print_rule_name(Rule), writex(']{'), tex_print_sequent(S), writex('}{'), tex_print_list(Ss, Tab), writex('}'), nlx. tex_print_list([], _Tab). tex_print_list([S1], Tab) :- !, nlx, Tab1 is Tab+2, tex_print(Tab1, S1), tabx(Tab). tex_print_list([S1|Ss], Tab) :- !, nlx, Tab1 is Tab+2, tex_print(Tab1, S1), tabx(Tab1), writex('&'), tex_print_list(Ss, Tab). tex_print_sequent((Xs-->Ys)) :- tex_print_formulas(Xs), writex(' \\lra '), tex_print_formulas(Ys). tex_print_formulas([]). tex_print_formulas([A]) :- !, tex_print_formula(A). tex_print_formulas([A|As]) :- tex_print_formula(A), writex(', '), tex_print_formulas(As). tex_print_formula(A) :- tex_print_formula(999, A). tex_print_formula(Prec0, A) :- tex_quantifier_name(A, Q, X, B), !, Prec = 999, (Prec0 < Prec -> writex('('); true), writex(Q), writex(' '), writex(X), writex('.'), tex_print_formula(B), (Prec0 < Prec -> writex(')'); true), !. tex_print_formula(Prec0, A) :- is_op(A, Prec, Type, Op, As), !, (Prec0 < Prec -> writex('('); true), tex_print_op_formula(Prec, Type, Op, As), (Prec0 < Prec -> writex(')'); true), !. tex_print_formula(_Prec0, A) :- tex_unit_name(A, U), !, writex(U). tex_print_formula(_Prec0, A) :- rename_functor(A, A1), writex(A1). rename_functor(X, Z) :- X =.. [F0|As], capitalize_atom(F0, F), Z =.. [F|As]. tex_quantifier_name(X@A, '\\forall', X, A). tex_quantifier_name(X#A, '\\exists', X, A). tex_unit_name(_, _) :- fail. tex_unit_name(bot, '\\bot'). tex_unit_name(top, '\\top'). %tex_print_op_formula(Prec, fy, Op, [A1]) :- Op = ~, !, % tex_print_op(Op), writex('{'), % tex_print_formula(Prec, A1), writex('}'). tex_print_op_formula(Prec, fx, Op, [A1]) :- !, Prec1 is Prec - 1, tex_print_op(Op), writex(' '), tex_print_formula(Prec1, A1). tex_print_op_formula(Prec, fy, Op, [A1]) :- !, tex_print_op(Op), writex(' '), tex_print_formula(Prec, A1). tex_print_op_formula(Prec, xf, Op, [A1]) :- !, Prec1 is Prec - 1, tex_print_formula(Prec1, A1), writex(' '), tex_print_op(Op). tex_print_op_formula(Prec, yf, Op, [A1]) :- !, tex_print_formula(Prec, A1), writex(' '), tex_print_op(Op). tex_print_op_formula(Prec, xfx, Op, [A1,A2]) :- !, Prec1 is Prec - 1, tex_print_formula(Prec1, A1), writex(' '), tex_print_op(Op), writex(' '), tex_print_formula(Prec1, A2). tex_print_op_formula(Prec, xfy, Op, [A1,A2]) :- !, Prec1 is Prec - 1, tex_print_formula(Prec1, A1), writex(' '), tex_print_op(Op), writex(' '), tex_print_formula(Prec, A2). tex_print_op_formula(Prec, yfx, Op, [A1,A2]) :- !, Prec1 is Prec - 1, tex_print_formula(Prec, A1), writex(' '), tex_print_op(Op), writex(' '), tex_print_formula(Prec1, A2). is_op(A, Prec, Type, Op, As) :- functor(A, Op, N), current_op(Prec, Type, Op), is_op0(A, Type, N, As), !. is_op0(A, fx, 1, [A1]) :- arg(1, A, A1). is_op0(A, fy, 1, [A1]) :- arg(1, A, A1). is_op0(A, xf, 1, [A1]) :- arg(1, A, A1). is_op0(A, yf, 1, [A1]) :- arg(1, A, A1). is_op0(A, xfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2). is_op0(A, xfy, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2). is_op0(A, yfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2). tex_print_op(Op) :- tex_op_name(Op, OpName), !, writex(OpName). tex_op_name(~, '\\lnot'). tex_op_name(/\, '\\land'). tex_op_name(\/, '\\lor'). tex_op_name(->, '\\imp'). tex_print_rule_name([Rule,LN]) :- !, tex_rule_name(Rule, RuleName), !, writex(RuleName), writex('('), writex(LN), writex(')'). tex_print_rule_name(Rule) :- tex_rule_name(Rule, RuleName), !, writex(RuleName). tex_rule_name(ax, '({\\rm Ax})'). tex_rule_name(axiom, '({\\rm Axiom})'). tex_rule_name(l(top), '({\\rm L}\\top)'). tex_rule_name(r(top), '({\\rm R}\\top)'). tex_rule_name(l(bot), '({\\rm L}\\bot)'). tex_rule_name(r(bot), '({\\rm R}\\bot)'). tex_rule_name(l(~), '({\\rm L}\\lnot)'). tex_rule_name(r(~), '({\\rm R}\\lnot)'). tex_rule_name(l(/\), '({\\rm L}\\land)'). tex_rule_name(r(/\), '({\\rm R}\\land)'). tex_rule_name(l(\/), '({\\rm L}\\lor)'). tex_rule_name(r(\/), '({\\rm R}\\lor)'). tex_rule_name(l(->), '({\\rm L}\\imp)'). tex_rule_name(r(->), '({\\rm R}\\imp)'). tex_rule_name(l(all), '({\\rm L}\\forall)'). tex_rule_name(r(all), '({\\rm R}\\forall)'). tex_rule_name(l(exists), '({\\rm L}\\exists)'). tex_rule_name(r(exists), '({\\rm R}\\exists)'). tex_rule_name(cut, '({\\rm Cut})'). %% %% Utilities %% append_all([], []). append_all([P], P). append_all([P|Ps], X) :- Ps=[_|_], append(P, X1, X), append_all(Ps, X1). merge(X1, X2, X) :- split(X, X1, X2). split([], [], []). split([X|Xs], [X|Ys], Zs) :- split(Xs, Ys, Zs). split([X|Xs], Ys, [X|Zs]) :- split(Xs, Ys, Zs). append([], Z, Z). append([W|X], Y, [W|Z]) :- append(X, Y, Z). member(X, [X|_Xs]). member(X, [_Y|Xs]) :- member(X, Xs). memberq(X, [X|_Xs]) :- !. memberq(X, [_Y|Xs]) :- memberq(X, Xs). memq(X, [Y|_Xs]) :- X==Y, !. memq(X, [_Y|Xs]) :- memq(X, Xs). get_nth(0, [X|_Xs], X) :- !. get_nth(N, [_|Xs], X) :- N>0, N1 is N-1, get_nth(N1, Xs, X). for(I, M, N) :- M =< N, I=M. for(I, M, N) :- M =< N, M1 is M+1, for(I, M1, N). assoc(X, Z, [[X0|Z]|_As]) :- X==X0, !. assoc(X, Z, [_|As]) :- assoc(X, Z, As). substitute(X0, X, A0, A) :- var(A0), X0==A0, !, A=X. substitute(_X0, _X, A0, A) :- var(A0), !, A=A0. substitute(_X0, _X, A0, A) :- atomic(A0), !, A=A0. substitute(X0, X, [A0|B0], [A|B]) :- !, substitute(X0, X, A0, A), substitute(X0, X, B0, B). substitute(X0, X, A0, A) :- A0 =.. B0, substitute(X0, X, B0, B), A =.. B. capitalize_atom(X, Z) :- atom(X), name(X, [C0|Cs]), C0 >= 0'a, C0 =< 0'z, !, C is ((C0 - 0'a) + 0'A), name(Z, [C|Cs]). capitalize_atom(X, X). n_writex(0, _) :- !. n_writex(N, X) :- N>0, writex(X), N1 is N-1, n_writex(N1, X). flush_out :- current_output(S), flush_output(S). goto_pos(T) :- current_output(S), line_position(S, T0), tabx(T-T0). line_position(W) :- current_output(S), line_position(S, W). %% %% Logging %% log_start(yes) :- !, log_start('seqprover.log'). log_start(File) :- logging(no, _), !, open(File, write, STR), retractall(logging(_,_)), assert(logging(File, STR)). log_end :- logging(no, _), !. log_end :- logging(_File, STR), close(STR), fail. log_end :- retractall(logging(_,_)), assert(logging(no, _)). log_suspend(logging(File,STR)) :- logging(File, STR), retractall(logging(_,_)), assert(logging(no, _)). log_resume(logging(File,STR)) :- retractall(logging(_,_)), assert(logging(File, STR)). readx(STR, X) :- read(STR, X), echo_read(STR, X). echo_read(user_input, _X) :- logging(no, _), !. echo_read(user_input, X) :- logging(_File, STR), !, write(STR, X), write(STR, '.'), nl(STR). echo_read(_, X) :- writex(X), writex('.'), nlx. writex(X) :- logging(no, _), !, write(X). writex(X) :- logging(_, STR), write(X), write(STR, X). nlx :- logging(no, _), !, nl. nlx :- logging(_, STR), nl, nl(STR). tabx(X) :- logging(no, _), !, tab(X). tabx(X) :- logging(_, STR), tab(X), tab(STR, X). %% %% Batch %% batch :- nl, write('# Start'), nl, % prolog_flag(syntax_errors, _, quiet), read(Output), read(Sequent), set_output_form(Output), batch_prove(Sequent), !, flush_out, halt. batch :- nl, write('# Syntax error'), nl, flush_out, halt. batch_prove((X <--> Y)) :- !, batch_prove((X --> Y)), nl, batch_prove((Y --> X)). batch_prove(S0) :- ( convert_to_seq(S0, S), sequentq(S) ; formulaq(S0), S = ([] --> [S0]) ), !, write('# Proving '), write(S), nl, statistics(runtime, _), (prove(S, P) -> statistics(runtime, [_,T]), nl, write('# BEGIN Proof'), nl, print_proof(P), nl, write('# END Proof'), nl, nl, write('# Proved in '), write(T), write(' msec.'), nl ; nl, write('# Fail to prove'), nl ). %% %% Initialization %% :- seq_init. ``` ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 28, 2024, 7:28am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/14 "2024-04-28T07:28:15Z")
> [@mgondan1](#): > > This is actually on the way, not yet 100% done, but very promising already. Thanks ! I paste here leanseq.pl for the propositional case only. It contains a LaTeX printer that works, but I did not succeed to use it for the FOL case. Maybe it can help: ```prolog % ----------------------------------------------------------------- % leanseq.pl - A sequent calculus prover implemented in Prolog % ----------------------------------------------------------------- :- use_module(library(lists)). :- use_module(library(ordsets)). :- use_module(library(time)). :- use_module(library(terms)). % :- [bussproofs]. % operator definitions (TPTP syntax) :- op( 500, fy, ~). % negation :- op(1000, xfy, &). % conjunction :- op(1100, xfy, '|'). % disjunction :- op(1110, xfy, =>). % conditional :- op(1120, xfy, <=>). % biconditional % :- op(500, fy, !). % universal quantifier: ![X]: % :- op(500, fy, ?). % existential quantifier: ?[X]: % :- op(500,xfy, :). %-------------------------------------------------------------- prove1(F,P):- time(prove([]>[F],P)). prove2(F,W):- time(prove([]>[F],P)), term_lower_upper(P,J), nl, write('Prolog output : '), write(P), nl, nl, latex(J,W),!, nl, nl. decide(F) :- prove2(F, _W). % ----------------------------------------------------------------- %% 1. Initial rule: if G and D are strings [i.e. lists] of atomic formulae, %% then G > D is a theorem if some atomic formula occurs on both sides of the arrow: prove(G>D, ax(G>D, ax)):- list_to_ord_set(G,Ord_G), list_to_ord_set(D,Ord_D), \+ ord_disjoint(Ord_G,Ord_D),!. /* prove(G>D, ax(G>D, ax)):- member(A,G), member(B,D), A==B,!. */ % In the ten rules listed below, G and D, are always % strings (possibly empty) of atomic formulae. % FIRST, NON-BRANCHING RULES %% 2. Conditional on the right prove(G>D, rcond(G>D,P)):- select((A=>B),D,D1),!, prove([A|G]>[B|D1],P). %% 3. Disjunction on the right prove(G>D, ror(G>D, P)):- select((A|B),D,D1),!, prove(G>[A,B|D1],P). %% 4. Negation on the right prove(G>D, rneg(G>D,P)):- select(~A,D,D1),!, prove([A|G]>D1,P). %% 5. Negation on the left prove(G>D, lneg(G>D,P)):- select(~A,G,G1),!, prove(G1>[A|D],P). %% 6. Conjunction on the left prove(G>D, land(G>D,P)):- select((A&B),G,G1),!, prove([A,B|G1]>D,P). % SECOND, BRANCHING RULES %% 7. Biconditional on the right prove(G>D, rbicond(G>D,P1,P2)):- select((A<=>B),D,D1),!, prove([A|G]>[B|D1],P1), prove([B|G]>[A|D1], P2). %% 8. Biconditional on the left prove(G>D, lbicond(G>D, P1,P2)):- select((A<=>B),G,G1),!, prove([A,B|G1]>D,P1), prove(G1>[A,B|D],P2). %% 9. Conditional on the left prove(G>D, lcond(G>D,P1,P2)):- select((A=>B),G,G1),!, prove(G1>[A|D],P1), prove([B|G1]>D,P2). %% 10. Conjunction on the right prove(G>D, rand(G>D,P1,P2)):- select((A&B),D,D1),!, prove(G>[A|D1],P1), prove(G>[B|D1],P2). %% 11. Disjunction on the left prove(G>D, lor(G>D, P1,P2)):- select((A|B),G,G1),!, prove([A|G1]>D, P1), prove([B|G1]>D, P2). % universal quantifier % Third - One and only one refutation rule. % NB: this rule in Prolog must be the last one in the order of clauses. %% 12 - Failure-rule prove(G>D, asq(G>D, asq)):- ord_disjoint(G,D),!. /* Now, to upcase atomic variables in LaTeX output, the following code is Carlo Capelli's https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/118 mapargs(term_lower_upper,Lower,Upper) ; is_list(Lower) -> maplist(term_lower_upper,Lower,Upper) ; var(Lower) -> Upper = Lower ; atomic(Lower) % this should be useless -> upcase_atom(Lower,Upper) ; throw(term_lower_upper(Lower,Upper)) ). / ****************************************************************** / /* Pretty Printing */ / ****************************************************************** / atom_split(X, D, L) :- atomic_list_concat(L, D, X). latex(H, J) :- latex_root(H, J, L, []), atom_split(Y, '', L), write(Y),nl. latex_root(P, J) --> ['\\begin{prooftree}'], latex_proof(P, J), ['\\end{prooftree}']. latex_proof(ax(S,U), J) --> ['\\RightLabel{$Ax.$} \\AxiomC{} \\UnaryInfC{'], latex_sequent(S, ax(S,U), J), ['}']. latex_proof(rcond(S,P), J) --> latex_proof(P, J), ['\\RightLabel{$R\\to$} \\UnaryInfC{'], latex_sequent(S, rcond(S,P), J), ['}']. latex_proof(land(S,P), J) --> latex_proof(P, J), ['\\RightLabel{$L\\land$} \\UnaryInfC{'], latex_sequent(S, land(S,P), J), ['}']. latex_proof(ror(S,P), J) --> latex_proof(P, J), ['\\RightLabel{$R\\lor$} \\UnaryInfC{'], latex_sequent(S, ror(S,P), J), ['}']. latex_proof(lneg(S,P), J) --> latex_proof(P, J), ['\\RightLabel{$L\\neg$} \\UnaryInfC{'], latex_sequent(S, lneg(S,P), J), ['}']. latex_proof(rneg(S,P), J) --> latex_proof(P, J), ['\\RightLabel{$R\\neg$} \\UnaryInfC{'], latex_sequent(S, rneg(S,P), J), ['}']. latex_proof(rand(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J), ['\\RightLabel{$R\\land$} \\BinaryInfC{'], latex_sequent(S, rand(S,P,Q), J), ['}']. latex_proof(lor(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J), ['\\RightLabel{$L\\lor$} \\BinaryInfC{'], latex_sequent(S, lor(S,P,Q), J), ['}']. latex_proof(lcond(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J), ['\\RightLabel{$L\\to$} \\BinaryInfC{'], latex_sequent(S, lcond(S,P,Q), J), ['}']. latex_proof(lbicond(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J), ['\\RightLabel{$R\\leftrightarrow$} \\BinaryInfC{'], latex_sequent(S, lbicond(S,P,Q), J), ['}']. latex_proof(rbicond(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J), ['\\RightLabel{$R\\leftrightarrow$} \\BinaryInfC{'], latex_sequent(S, rbicond(S,P,Q), J), ['}']. latex_proof(asq(S,U), J) --> ['\\RightLabel{$Asq.$} \\AxiomC{} \\UnaryInfC{'], latex_antisequent(S, asq(S,U), J), ['}']. latex_sequent(G > D, P, J) --> ['$ '], latex_list(G, P, left, 0, J), [' \\vdash '], latex_list(D, P, right, 0, J), [' $']. latex_antisequent(G > D, P, J) --> ['$ '], latex_list(G, P, left, 0, J), [' \\nvdash '], latex_list(D, P, right, 0, J), [' $']. latex_list([], _, _, _, _) --> []. % latex_list([X|L], P, F, N, J) --> {has_usage(P, F, N)}, !, latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J). latex_list([X|L], P, F, N, J) --> latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J). latex_list([_|L], P, F, N, J) --> {M is N+1}, latex_list(L, P, F, M, J). latex_rest([], _, _, _, _) --> []. % latex_rest([X|L], P, F, N, J) --> {has_usage(P, F, N)}, !, [', '], latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J). latex_rest([X|L], P, F, N, J) --> [', '], latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J). latex_rest([_|L], P, F, N, J) --> {M is N+1}, latex_rest(L, P, F, M, J). latex_formula(~A, J) --> !, ['\\neg '], latex_term(A, J). latex_formula((A&B), J) --> !, latex_term(A, J), [' \\land '], latex_term(B, J). latex_formula((A|B), J) --> !, latex_term(A, J), [' \\lor '], latex_term(B, J). latex_formula((A=>B), J) --> !, latex_term(A, J), [' \\to '], latex_term(B, J). latex_formula((A<=>B), J) --> !, latex_term(A, J), [' \\leftrightarrow '], latex_term(B, J). % latex_formula(![X], J) --> !, ['\\forall '], latex_term(X, J). % latex_formula(?[Y], J) --> !, ['\\exists '], latex_term(Y, J). latex_formula(X, J) --> latex_factor(X, J). latex_term(~A, J) --> !, ['\\neg '], latex_term(A, J). latex_term((A&B), J) --> !, ['('], latex_term(A, J), [' \\land '], latex_term(B, J), [')']. latex_term((A|B), J) --> !, ['('], latex_term(A, J), [' \\lor '], latex_term(B, J), [')']. latex_term((A=>B), J) --> !, ['('], latex_term(A, J), [' \\to '], latex_term(B, J), [')']. latex_term((A<=>B), J) --> !, ['('], latex_term(A, J), [' \\leftrightarrow '], latex_term(B, J), [')']. % latex_term(![X], J) --> !, ['\\forall '], latex_term(X, J). % latex_term(?[Y], J) --> !, ['\\exists '], latex_term(Y, J). latex_term(X, J) --> latex_factor(X, J). latex_factor(X, J) --> {var(X), member(W = N, J), W == X}, !, [N]. latex_factor(X, _) --> {var(X)}, !, ['?']. latex_factor(X, J) --> {X=..[F,Y|L]}, !, [F, '('], latex_factor(Y, J), latex_args(L, J), [')']. latex_factor(X, _) --> [X]. latex_args([], _) --> []. latex_args([X|L], J) --> [','], latex_factor(X, J), latex_args(L, J). /* Example: ?- decide(p => p). % 10 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 321926 Lips) Prolog output : rcond([]>[(p=>p)],ax([p]>[p],ax)) \begin{prooftree}\RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$ P \vdash P $}\RightLabel{$R\to$} \UnaryInfC{$ \vdash P \to P $}\end{prooftree} true. ?- decide(p => q). % 36 inferences, 0.000 CPU in 0.000 seconds (92% CPU, 675371 Lips) Prolog output : rcond([]>[(p=>q)],asq([p]>[q],asq)) \begin{prooftree}\RightLabel{$Asq.$} \AxiomC{} \UnaryInfC{$ P \nvdash Q $}\RightLabel{$R\to$} \UnaryInfC{$ \vdash P \to Q $}\end{prooftree} true. */ ``` ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [April 28, 2024, 11:49am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/15 "2024-04-28T11:49:17Z")
Once I write codes which parses proof trees given in plain text, then renders into pdf/svg via latex/divpdfmx[/pdf2svg] using Paulson’s prooftree.tex. Although it was a work of mine more than 20 years ago, the CGI version was recovered recently to work without changes on core of the Prolog codes. I neither remember well details of the codes nor am interested in revising version. However I think now, using the dot language (graphviz) joint with latex might fit my purpose and hope also for your current work and useful to displaying graph structure like proof tree. Please let me know if this comment would be relevant to your post and interested in more details. Now I feel getting interested into the dot version though I have no idea in details. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 28, 2024, 2:10pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/16 "2024-04-28T14:10:08Z")
Without code to test thanks to a clear “howto”, it is difficult for me to give an opinion. ---
**Author:** ![kuniaki.mukai](https://avatars.discourse-cdn.com/v4/letter/k/c67d28/32.png) [@kuniaki.mukai](https://swi-prolog.discourse.group/u/kuniaki.mukai)\ **Post date:** [April 28, 2024, 2:37pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/17 "2024-04-28T14:37:57Z")
I should post after I am sure that dot allow graphics (jpeg/pdf/svg) as a label of node or edges, but it is just personal expectation for now. I have to check it. **EDIT** A quick search " graphviz svg for node" returns positive answers. I will take time later for more details. **EDIT** There exists dot2tex, which might be what I meant as far as I have tested a sample file in the github. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [April 29, 2024, 4:36pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/20 "2024-04-29T16:36:57Z")
> [@anon95304481](#): > > **The Modelfinder** > Often there are simple countermodels that are hard to find through > the tableau method. We therefore run a **separate algorithm** to find > smallest countermodels. > [GitHub - wo/tpg: Tree Proof Generator](https://github.com/wo/tpg?tab=readme-ov-file#the-modelfinder) Yes. The quotation of what Wolfgang wrote must go on: > […] We therefore run a separate algorithm to find smallest countermodels. > > In outline, this works as follows. > > We transform the formulas for which we want to find a model into clausal normal form, > which gives us literal “constraints” that we’re trying to satisfy. > For example, Fa ∧ Fb is split into two constraints, Fa and Fb; **∀x∃yRxy is turned into Rxf(x)**; > Fa ∨ Fb is turned into the disjunctive constraint [Fa, Fb]. What I have put in bold fonts is nothing else than Skolemization… > [@anon95304481](#): > > That it is a separate algorithm also means that Skolemization is not > necessarely the approach to find a model. You can try to introduce > Skolemization into the model finder, but some model finders don’t use > Skolemization. You might do a literature search about model finders, you > will find that there are some model finders without Skolemization at all! 1. I never wrote that Skolemization is the only way to make a model finder in FOL. 2. I never wrote that Jens Otten’s prover was sufficient to do it. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 4, 2024, 8:52am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/26 "2024-05-04T08:52:18Z")
> [@anon95304481](#): > > For LeanSeq which uses Herbrandization/Skolemization on the > fly. It is not possible to generate LK proof display. Because > LeanSeq doesn’t use Sequent Calculus Gentzen quantifier rules. The goal is not to display **LK** sequent calculus, but **Leanseq** i.e. **Lean** sequent calculus. Jens’ Otten explanations are given in these [slides.](http://www.jens-otten.de/tutorial_tableaux19/slides/prover_tutorial_TABLEAUX19_2.pdf) **LK** (more precisely, a sequent calculus akin to **LK** ) has been translated by Tamura. It provides for example the following sequent proof in LaTeX via proof.sty: ![tamura-exampe](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/2X/7/719d80bcbf600001ccd1f7d245a792fcdef605fd.jpeg) Now, I do not know if it is possible or impossible to translate the leanseq proof of this same sequent in bussproofs.sty, but via [portray\_clause/1](https://www.swi-prolog.org/pldoc/doc_for?object=portray_clause/1) we get already a much more clear proof of it (thanks to Jan Wielemaker to have insisted on this point) : ```prolog decide((?[Y]: ![X]: f(X,Y)) => (![X]: ?[Y]: f(X,Y))). iteration:1 iteration:2 % 451 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 3396008 Lips) Prolog proof: r_to([]>[(?[A]:![B]:f(B, A)=>![B]: ?[A]:f(B, A))], r_forall([?[A]:![B]:f(B, A)]>[![B]: ?[A]:f(B, A)], l_exists([?[A]:![B]:f(B, A)]>[?[C]:f(f_sk(1, []), C)], r_exists([![D]:f(D, f_sk(2, []))]>[?[C]:f(f_sk(1, []), C)], l_forall([![D]:f(D, f_sk(2, []))]>[f(f_sk(1, []), f_sk(2, [])), ?[C]:f(f_sk(1, []), C)], ax([f(f_sk(1, []), f_sk(2, [])), ![D]:f(D, f_sk(2, []))]>[f(f_sk(1, []), f_sk(2, [])), ?[C]:f(f_sk(1, []), C)], ax)))))). true. ``` Note that the proof is different. It has been producted via the program below, a bit different from the first I pasted at the beginning of this discussion. ```prolog % --------------------------------------------------------------------------------- % leanseq.pl - A sequent calculus prover for classical F.O.L. implemented in Prolog % --------------------------------------------------------------------------------- % :- [latex_pc]. % operator definitions (TPTP syntax) :- op( 500, fy, ~). % negation :- op(1000, xfy, &). % conjunction :- op(1100, xfy, '|'). % disjunction :- op(1110, xfy, =>). % conditional :- op(1120, xfy, <=>). % biconditional :- op( 500, fy, !). % universal quantifier: ![X]: :- op( 500, fy, ?). % existential quantifier: ?[X]: :- op( 500,xfy, :). % ----------------------------------------------------------------- decide(F) :- prove(F,P),nl, write('Prolog proof: '), portray_clause(P),!. prove(F,I,P) :- I < 5, print(iteration:I), nl, prove([] > [F],[],I,1,_,P). prove(F,I,P) :- I1 is I+1, I < 5, prove(F,I1,P). prove(F,P) :- time(prove(F,1,P)). % ----------------------------------------------------------------- % THE LOGICAL RULES % 1.The axiom prove(G > D,_,_,J,J,Proof) :- member(A,G), A\=(_&_), A\=(_|_), A\=(_=>_), A\=(~_), A\=(!_), A\=(?_), member(B,D), unify_with_occurs_check(A,B), Proof = ax(G > D,ax). % FIRST, NON-BRANCHING RULES % %% 2. Conditional on the right prove(G > D,FV,I,J,K,Proof) :- select(A=>B,D,D1), !, prove([A|G] > [B|D1],FV,I,J,K,Rule_applied), Proof = r_to(G > D, Rule_applied). %% 3. Disjunction on the right prove(G > D,FV,I,J,K,Proof) :- select(A|B,D,D1), !, prove(G > [A,B|D1],FV,I,J,K,Rule_applied), Proof = r_lor(G > D, Rule_applied). %% 4. Negation on the right prove(G > D,FV,I,J,K,Proof) :- select(~A,D,D1), !, prove([A|G] > D1,FV,I,J,K,Rule_applied), Proof = r_neg(G > D, Rule_applied). %% 5. Negation on the left prove(G > D,FV,I,J,K,Proof) :- select(~A,G,G1), !, prove(G1 > [A|D],FV,I,J,K,Rule_applied), Proof = l_neg(G > D, Rule_applied). %% 6. Conjunction on the left prove(G > D,FV,I,J,K,Proof) :- select(A&B,G,G1), !, prove([A,B|G1] > D,FV,I,J,K,Rule_applied), Proof = l_land(G > D, Rule_applied). % SECOND, BRANCHING PROPOSITIONAL LOGIC RULES % 7. Biconditional on the right prove(G>D,FV,I,J,K,Proof) :- select((A<=>B),D,D1),!, prove([A|G]>[B|D1],FV,I,J,J1,Rule_applied1), prove([B|G]>[A|D1],FV,I,J1,K,Rule_applied2), Proof = l_leftrightarrow(G > D, Rule_applied1, Rule_applied2). %% 8. Biconditional on the left prove(G>D,FV,I,J,K,Proof):- select((A<=>B),G,G1),!, prove([A,B|G1]>D,FV,I,J,J1,Rule_applied1), prove(G1>[A,B|D],FV,I,J1,K,Rule_applied2), Proof = l_leftrightarrow(G > D, Rule_applied1, Rule_applied2). %% 9. Conditional on the left prove(G > D,FV,I,J,K,Proof) :- select(A=>B,G,G1), !, prove(G1 > [A|D],FV,I,J,J1,Rule_applied1), prove([B|G1] > D,FV,I,J1,K,Rule_applied2), Proof = l_to(G > D, Rule_applied1, Rule_applied2). %% 10. Conjunction on the right prove(G > D,FV,I,J,K,Proof) :- select(A&B,D,D1), !, prove(G > [A|D1],FV,I,J,J1,Rule_applied1), prove(G > [B|D1],FV,I,J1,K,Rule_applied2), Proof = r_land(G > D, Rule_applied1, Rule_applied2). %% 11. Disjunction on the left prove(G > D,FV,I,J,K,Proof) :- select(A|B,G,G1), !, prove([A|G1] > D,FV,I,J,J1,Rule_applied1), prove([B|G1] > D,FV,I,J1,K,Rule_applied2), Proof = l_lor(G > D, Rule_applied1, Rule_applied2). %% QUANTIFICATION RULES % 12. universal quantifier on the right prove(G > D,FV,I,J,K,Proof) :- select((![X]:A),D,D1),!, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)), J1 is J+1, prove(G > [A1|D1],FV,I,J1,K,Rule_applied), Proof = r_forall(G > D, Rule_applied). % 13. existential quantifier on the left prove(G > D,FV,I,J,K,Proof) :- select((?[X]:A),G,G1),!, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)), J1 is J+1, prove([A1|G1] > D,FV,I,J1,K,Rule_applied), Proof = l_exists(G > D, Rule_applied). % 14. existential quantifier on the right prove(G > D,FV,I,J,K,Proof) :- member((?[X]:A),D), \+ length(FV,I), copy_term((X:A,FV),(Y:A1,FV)), prove(G > [A1|D],[Y|FV],I,J,K,Rule_applied), Proof = r_exists(G > D, Rule_applied). % 15. universal quantifier on the left prove(G > D,FV,I,J,K,Proof) :- member((![X]:A),G), \+ length(FV,I), copy_term((X:A,FV),(Y:A1,FV)), prove([A1|G] > D,[Y|FV],I,J,K,Rule_applied), Proof = l_forall(G > D, Rule_applied). %% END of leanseq.pl code ``` ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 4, 2024, 10:26am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/29 "2024-05-04T10:26:12Z")
There is an interesting comparison between Jens Otten’s Prover and Naoyuki Tamura’s. In his slides Jens Otten wrote: ![Jens4](https://global.discourse-cdn.com/free1/uploads/swiprolog/original/2X/2/2b221499766f14822ad0ce2dc0d1e1bcc72ba0d3.jpeg) And indeed, whith Jens’ prover, we get : ```prolog ?- decide((![X]: f(a) => ![Y]: f(Y))). iteration:1 iteration:2 iteration:3 iteration:4 % 26,717 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 4486571 Lips) false. ``` By contrast with Naoyuki’s prover: ```prolog Sequent Calculus Prover ver 2.0 in Prolog by Naoyuki Tamura (tamura@kobe-u.ac.jp) cl(first)> X@f(a) --> Y@f(Y). _7964@f(a)-->_7970@f(_7970). Trying to prove with threshold = 0 Succeed in proving a@f(a) --> a@f(a) (0 msec.) pretty:1 = ----------------- Ax a@f(a) --> a@f(a) yes ``` And we can also compare the proofs for the valid sequent ∀x Fx → ∀y Fy . Leanseq by Jens Otten makes perfectly the job: ```prolog ?- decide((![X]: f(X) => ![Y]: f(Y))). iteration:1 % 90 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 480179 Lips) Prolog proof: r_to([]>[(![A]:f(A)=>![B]:f(B))], r_forall([![A]:f(A)]>[![B]:f(B)], l_forall([![A]:f(A)]>[f(f_sk(1, []))], ax([f(f_sk(1, [])), ![A]:f(A)]>[f(f_sk(1, []))], ax)))). true. ``` By contrast, the output of seqprover.pl is not adequate: ```prolog cl(first)> X@f(X) --> Y@f(Y). _7960@f(_7960)-->_7970@f(_7970). Trying to prove with threshold = 0 Succeed in proving _7960@f(_7960) --> _7960@f(_7960) (0 msec.) pretty:2 = ----------------- Ax X@f(X) --> X@f(X) yes cl(first)> ``` ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 5, 2024, 9:48am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/31 "2024-05-05T09:48:47Z")
I have a very simple question to help understand the pretty-printing. I get the following output: ```prolog decide(((a => b) => a => a)). iteration:1 % 29 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 300708 Lips) Prolog Proof: r_to([]>[((a=>b)=>a=>a)], r_to([(a=>b)]>[(a=>a)], ax([a, (a=>b)]>[a], ax))). LaTeX Proof: \begin{prooftree}\RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$ A, A \to B \vdash A $}\RightLabel{$R\to$} \UnaryInfC{$ A \to B \vdash A \to A $}\RightLabel{$R\to$} \UnaryInfC{$ \vdash (A \to B) \to (A \to A) $}\end{prooftree} true. ``` It would be better to get: ```prolog LaTeX Proof: \begin{prooftree} \RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$ A, A \to B \vdash A $} \RightLabel{$R\to$} \UnaryInfC{$ A \to B \vdash A \to A $} \RightLabel{$R\to$} \UnaryInfC{$ \vdash (A \to B) \to (A \to A) $} \end{prooftree} ``` The first new line can easily be obtained by the “driver” in leanseq.pl, but the others depend on the pretty-printing file that is with DCG, and I do not succeed to dot it, even if it is easy to see that after each `}` we need a new line… ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 5, 2024, 1:34pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/33 "2024-05-05T13:34:20Z")
Many thanks for your reply. Now the output is very nice: ```prolog ?- decide((((a => b) => a) => a)). iteration:1 % 61 inferences, 0.000 CPU in 0.004 seconds (2% CPU, 702360 Lips) Prolog Proof: r_to([]>[(((a=>b)=>a)=>a)], l_to([((a=>b)=>a)]>[a], r_to([]>[(a=>b), a], ax([a]>[b, a], ax)), ax([a]>[a], ax))). LaTeX Proof: \begin{prooftree} \RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$ A \vdash B, A $} \RightLabel{$R\to$} \UnaryInfC{$ \vdash A \to B, A $} \RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$ A \vdash A $} \RightLabel{$L\to$} \BinaryInfC{$ (A \to B) \to A \vdash A $} \RightLabel{$R\to$} \UnaryInfC{$ \vdash ((A \to B) \to A) \to A $} \end{prooftree} true. ?- ``` ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 5, 2024, 6:25pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/34 "2024-05-05T18:25:17Z")
> [@anon95304481](#): > > Well, nobody is perfect! Apart from this bug, Naoyuki’s prover has some interesting features, among which it provides LaTex output of FOL proofs. Therefore it would be possible to change the code of Leanseq prove, preserving its soundness but allowing LaTeX FOL proofs. ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 6, 2024, 9:56am UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/36 "2024-05-06T09:56:57Z")
> [@anon95304481](#): > > What makes you think the output algorithm of Naoyuki’s prover of > would help you? Naoyuki’s prover has another point of departure, > when it generates a proof display. The point of departure for proof > > display in Naoyuki’s prover is a proof term without Skolem terms in it. > Naoyuki’s prover doesn’t use Skolem terms. For example thats his ∃L rule, > eigen\_variable/2 generates a constraint not a Skolem term: I believed that it was possible to use Naoyuki code only to replace the rules for quantification, in order to cancel FV,I,J,K in Jens Prover and to come back to a structure that is propositional calculus leanseq’s prover. But all my tentatives fail. 🙁 ---
**Author:** ![joseph-vidal-rosset](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/joseph-vidal-rosset/32/2594_2.png) [@joseph-vidal-rosset](https://swi-prolog.discourse.group/u/joseph-vidal-rosset)\ **Post date:** [May 31, 2024, 4:28pm UTC](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/40 "2024-05-31T16:28:01Z")
Ugliness is not really the problem, because what is ugly can become pretty. It is more difficult to obtain a correct first result. Thanks for your help ! [Next page](https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398.md?page=2)