I’m using: SWI-Prolog version : SWI-Prolog version 8.3.3 for x86_64-linux I posted this question here, few days ago, but I’m wasting my time in trying to get a solution : [user1121356] Prolog implementation of Quine's algorithm for classical propositional logic (in Quine's "M…

[image] anon95304481: Maybe try last(L,1). You find the spec of last/2 online. There is a trick to find the spec via Google, just type “last SWI-Prolog” into the search bar: https://lmgtfy.com/?q=last+SWI-Prolog Thanks ! Now boole prover in my file is : boole :- get_wff(_A,_L). get_wff…

[image] anon95304481: Can your program solve this? “My” program? It is your program, Jan. I would be very happy to be able to write such a program. Unfortunately, “ce n’est pas demain la veille”. :frowning: I will have a look on sat/1 and labeling/1.

Here is the boole-quine.pl prover in the last corrected version that I can publish. /* This prover is the work of Jan Burse. I changed only the symbols for operators, that's it. See the web page : https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830 and also https://stackoverflo…

[image] anon95304481: Can your program solve this? You need to implement sat/1 + labeling/1 , to list the positive answer. Or then realize sat/1 + sat_count/2 . I must tell you frankly Jan that even if I am really interested by your question, I am afraid to miss time. Feel free to use the file …

Jan, I have a question about ‘plain.pl’. Can a syntactic change of definition of operator affect the performances of this prover?

Jan, I’m much impressed by plain.pl . Here are the stastics with a very big disjunction that is not valid and proved as being such by plain.pl : % 447 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 3540510 Lips) A11 = A21, A21 = A31, A31 = A41, A41 = A51, A51 = A12, A12 = A22, A22 = A32, A32 = A4…

But unfortunately, plain.pl does not succeed in giving an output for the big valid formula that your know: time(falsify(((~ (( ~ A0 + F) * ((~ ( ~ B20 + B0) + A20) * ((~ ( ~ B0 + A1) + A0) * ( (~ ( ~ B1 + A2) + A1) * ((~ ( ~ B2 + A3) + A2) * ((~( ~ B3 + A4) + A3) * ((~ ( ~ B4 + A5) + A4) * (( ~ (…

[image] anon95304481: Do you have a student that can implement Herbrandization of Negation Normal Form in Prolog. Unfortunately, no. My first education was in Philosophy, and in France. I am interested in mathematical logic, but my students are often more afraid than interested by formal arg…

Do not hesitate to write to Jen : jeotten @ ifi.uio.no All his programs are in Prolog and he will be certainly interested to have discussions with you.

[image] anon95304481: Whether the second prover of Jen Otten is in the scope of your current endeavours or not. Every work in Prolog that is related to theorems provers in first order logic (not necessarily classical) interests me. But I stress on the point that my endeavours are mainly to …

Implementing Quine's algorithm

Help! Algorithm

Topic		Replies	Views
Improving Wang's algorithm in Prolog Algorithm how-to	66	4660	September 13, 2020
SWI-Prolog - PHP - Html Tools how-to	64	5158	September 21, 2020
Needing help with call_with_depth_limit/3 Predicate	40	1411	July 6, 2024
How to use of upcase_atom/2 to get uppercase letters in an output Data Structure how-to	61	4302	January 23, 2022
Understanding Bratko `translate` predicate General	21	858	April 22, 2023

Implementing Quine's algorithm

Related topics