Hello everybody, It is said about 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: % --------------------------------------------------------------------------------- % 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 : ?- 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?, 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.

@anon95304481 , unfortunately, there is a bug in your program: show((![X]:f(X) => ![Y]:g(Y)) => (?[X]: ![Y]: (f(X) => g(Y)))). \begin{prooftree}\AxiomC{} \RightLabel{Ax}\UnaryInfC{ ERROR: Domain error: `variable_name' expected, found `'['' ERROR: In: ERROR: [20] write_term(f(a),[variable_names(...)]) ERROR: [19] render_list([f(...)],['X'=_842,...|...]) Probably easy to fix for you, but too difficult for me. :frowning:

[image] anon95304481: What Prolog do you use? joseph@mx:~$ swipl --version SWI-Prolog version 9.0.4 for x86_64-linux

[image] anon95304481: You need to do the same for the skolem rewrite. With risk of adding errors…

portray_clause/1 for the proof of this theorem via leanseq.pl : ?- decide((![X]: f(X) => ![Y]: g(Y)) => (?[X]: ![Y]: (f(X) => g(Y)))). % 866 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 4402867 Lips) P_Proof: r_to([]>[((![A]:f(A)=>![B]:g(B))=> ?[A]:![B]:(f(A)=>g(B)))], l_to([(![A]:f(A)=>![B]:g(B))]>[?[A]:![B]:(f(A)=>g(B))], r_forall([]>[![A]:f(A), ?[A]:![B]:(f(A)=>g(B))], r_exists([]>[f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))], r_forall([]>[![C]:(f(f_sk(1, []))=>g(C)), f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))], r_to([]>[(f(f_sk(1, []))=>g(f_sk(2, [f_sk(1, [])]))), f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))], ax([f(f_sk(1, []))]>[g(f_sk(2, [f_sk(1, [])])), f(f_sk(1, [])), ?[A]:![B]:(f(A)=>g(B))], ax))))), r_exists([![B]:g(B)]>[?[A]:![B]:(f(A)=>g(B))], r_forall([![B]:g(B)]>[![D]:(f(E)=>g(D)), ?[A]:![B]:(f(A)=>g(B))], r_to([![B]:g(B)]>[(f(E)=>g(f_sk(3, [E]))), ?[A]:![B]:(f(A)=>g(B))], l_forall([f(E), ![B]:g(B)]>[g(f_sk(3, [E])), ?[A]:![B]:(f(A)=>g(B))], ax([g(f_sk(3, [E])), f(E), ![B]:g(B)]>[g(f_sk(3, [E])), ?[A]:![B]:(f(A)=>g(B))], ax))))))).

@anon95304481 , thanks. To compare with the output of Naoyuki’s prover: cl(first)> X@f(X) -> Y@g(Y) --> X#Y@(f(X) -> g(Y)). _10282@f(_10282)->_10292@g(_10292)-->_10282#_10292@(f(_10282)->g(_10292)). Trying to prove with threshold = 0 1 2 Succeed in proving _19520@f(_19520)->_19394@g(_19394) --> _19520#_19394@(f(_19520)->g(_19394)) (36 msec.) pretty:1 = ------------------------------------ Ax --------------------------------------------- Ax f(Z) --> f(Z),g(X1),X#Y@(f(X)->g(Y)) f(Y1),g(Z1),Y@g(Y) --> g(Z1),X#Y@(f(X)->g(Y)) -------------------------------------- R-> --------------------------------------------- L@ --> f(Z),f(Z)->g(X1),X#Y@(f(X)->g(Y)) f(Y1),Y@g(Y) --> g(Z1),X#Y@(f(X)->g(Y)) ----------------------------------------- R@ ---------------------------------------- R-> --> f(Z),Y@(f(Z)->g(Y)),X#Y@(f(X)->g(Y)) Y@g(Y) --> f(Y1)->g(Z1),X#Y@(f(X)->g(Y)) ----------------------------------------- R# ------------------------------------------- R@ --> f(Z),X#Y@(f(X)->g(Y)) Y@g(Y) --> Y@(f(Y1)->g(Y)),X#Y@(f(X)->g(Y)) ---------------------------- R@ ------------------------------------------- R# --> X@f(X),X#Y@(f(X)->g(Y)) Y@g(Y) --> X#Y@(f(X)->g(Y)) --------------------------------------------------------------------------- L-> X@f(X)->Y@g(Y) --> X#Y@(f(X)->g(Y)) yes cl(first)>

Your correction works with my file and my system. Thanks. :+1: :clap:

The heart button looks a little bit stoopid…it is also very limiting that it is the only option available…just saying…these guys at discourse must be politically correct gurus…it is all the more contradictory that one should place hearts on posts of strangers…but of course we are nothing but one big family (and not dysfunctional I hope…) :sweat_smile: :heartbeat:

This document is very useful: http://www.actual.world/resources/tex/doc/Proofs.pdf My favorite LaTeX macros for proofs in Fitch style Klüwer’s in the version given by Alexander W. Kocurek, June 8, 2019: % $Id: fitch.sty,v 1.6 2003/06/28 16:53:00 johanw Exp $ % Macros for Fitch-style formal proofs % Johan W. Klüwer, June 10, 2001 % EDITS (Alexander W. Kocurek, June 8, 2019) % %\RequirePackage{mdwtab,latexsym,amsmath,amsfonts,ifthen} % - too many fonts were loading % - removed mdwtab, which redefines tabular, causing several conflicts such as overriding color in tabular cells and redefining \hline so that \hline without arguments no longer works % ADDED (March 28, 2022) % - added more flexibility for horizontal spacing % - - \fitchsep controls separation between vertical lines % - - \fitchnumsep controls separation between numbers and vertical lines \RequirePackage{mathtools,amsmath,ifthen,array} % Line height in proofs \newlength{\fitchlineht} \setlength{\fitchlineht}{1.5\baselineskip} % Horizontal indent between proof levels \newlength{\fitchindent} \setlength{\fitchindent}{0.7em} % Indent to comment \newlength{\fitchcomind} \setlength{\fitchcomind}{2em} % Line number width \newlength{\fitchnumwd} \setlength{\fitchnumwd}{1em} % Horizontal space between vertical lines (AK added) \newlength{\fitchsep} \setlength{\fitchsep}{\fitchindent} % Horizontal space between numbers and vertical lines (AK added) \newlength{\fitchnumsep} \setlength{\fitchnumsep}{\fitchindent} % Altered from mdwtab.sty: shorter vline, for start of subproof \makeatletter \newcommand\fvline[1][\arrayrulewidth]{\vrule\@height.5\fitchlineht\@width#1\relax} \makeatother % Ordinary vertical line \newcommand{\fa}{\hspace*{\fitchsep}\vline\hspace*{\fitchindent}} % Vertical line, shorter: Use at start of (sub)proof \newcommand{\fb}{\hspace*{\fitchsep}\fvline\hspace*{\fitchindent}} % Hypothesis \newcommand{\fh}{\hspace*{\fitchsep}\fvline% \makebox[0pt][l]{{% \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}% \hspace*{\fitchindent}} % Hypothesis, with longer vert line: for >1 hypothesis \newcommand{\fj}{\hspace*{\fitchsep}\vline% \makebox[0pt][l]{{% \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}% \hspace*{\fitchindent}} % Modal subproof: takes argument = operator \newcommand{\fitchmodal}[1]{% \hspace*{\fitchsep}\makebox[0pt][r]{${}^{#1}$\,}\fvline\hspace*{\fitchindent}} \newcommand{\fn}{\fitchmodal{\Box}}% Box subproof \newcommand{\fp}{\fitchmodal{\Diamond}}% Diamond subproof % Modal subproof with hypothesis in first line (as in Fitch) \newcommand{\fitchmodalh}[1]{% \hspace*{\fitchsep}\makebox[0pt][r]{${}^{\footnotesize #1}$\,}% \fvline% \makebox[0pt][l]{{% \raisebox{-1.4ex}[0pt][0pt]{\rule{1.5em}{\arrayrulewidth}}}}% \hspace*{\fitchindent}} \newcommand{\fm}{\fitchmodalh{\Box}}% Box subproof with hypothesis \newcommand{\fq}{\fitchmodalh{\Diamond}}% Diamond subproof with hypothesis % Rule: formula introduction marker. \fr with line, \fs without line \newcommand{\fr}{% \hspace*{\fitchsep}\makebox[0pt][r]{${\rhd}$\,\,}\vline\hspace*{\fitchindent}} \newcommand{\fs}{% \hspace*{\fitchsep}\makebox[0pt][r]{${\rhd}$\,\,}} % Box around argument, like new variable in ql \newcommand{\fw}[1]{\fbox{\footnotesize $#1$}} % \newcounter{fitchcounter} \setcounter{fitchcounter}{0} %To avoid starting from 1, \setboolean{resetfitchcounter}{false} \newboolean{resetfitchcounter} \setboolean{resetfitchcounter}{true} %To avoid increasing numbers, \setboolean{increasefitchcounter}{false} \newboolean{increasefitchcounter} \setboolean{increasefitchcounter}{true} %\formatfitchcounter can be altered if need be, though only once per proof \newcommand{\formatfitchcounter}[1]{\scriptsize \arabic{#1}} %Typeset the counter \newcommand{\fitchcounter}{% \ifthenelse{\boolean{increasefitchcounter}}{\addtocounter{fitchcounter}{1}}{} \formatfitchcounter{fitchcounter}} %A line with a special number -- a tag, e.g. \ftag{\vdots}{} \newcommand{\ftag}[2]{\multicolumn{1}% {!{\makebox[\fitchnumwd][r]{\footnotesize $#1$}\hspace{\fitchindent}}>{$}l {$}l {$}l {$}l<{$}@{\hspace{\fitchcomind}}l}}% {\end{tabular}} \newenvironment{fitch}{\renewcommand{\arraystretch}{1.5} \begin{fitchnum}}{\end{fitchnum}} \newenvironment{fitch*}{\renewcommand{\arraystretch}{1.5} \begin{fitchunum}}{\end{fitchunum}} % The following is useful for giving a numbered formula, then the proof. \newenvironment{flem}[2]% {\begin{eqnarray} &#1\label{#2}\\ &\begin{fitch}}% {\end{fitch}\notag\end{eqnarray}} %To write comment field for two consecutive lines, with brace \newcommand{\ftwocom}[1]{% \parbox[t]{3cm}{ \raisebox{-.6\baselineskip}[\baselineskip][0pt]{% $\left. \begin{aligned} \,\\ \, \end{aligned} \right\}$\quad #1} }} Nothing in MathJax3 for Fitch style, unfortunately (and I am unable to fix this). Last, this pedagogical website is wonderful : https://carnap.io/ and it is mainly based on Fitch style,

Needing help with call_with_depth_limit/3

Help! Predicate

joseph-vidal-rosset May 31, 2024, 4:48pm 44

It works now.

Topic		Replies	Views
How to use of upcase_atom/2 to get uppercase letters in an output Data Structure how-to	61	4356	January 23, 2022
How to reverse the output of proof printing in this fork of seqprover.pl Discussion how-to	4	276	May 20, 2024
Implementing Quine's algorithm Algorithm how-to	104	5666	September 16, 2020
leanTAP , a Prolog prover for Classical Logic Nice to know	77	2792	February 10, 2022
Improving Wang's algorithm in Prolog Algorithm how-to	66	5058	September 13, 2020

Needing help with call_with_depth_limit/3

Related topics