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 : % ------------------------------------------…

@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(..…

[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([(![…

@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) --> _19…

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…

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…

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	4297	January 23, 2022
How to reverse the output of proof printing in this fork of seqprover.pl Discussion how-to	4	254	May 20, 2024
Implementing Quine's algorithm Algorithm how-to	104	5036	September 16, 2020
leanTAP , a Prolog prover for Classical Logic Nice to know	77	2589	February 10, 2022
Improving Wang's algorithm in Prolog Algorithm how-to	66	4638	September 13, 2020

Needing help with call_with_depth_limit/3

Related topics