Improving Wang's algorithm in Prolog

Help! Algorithm
34

Sorry :slightly_frowning_face: but you will have to identify each post individually. If I move post by others based on your statement then I have to deal with the problem. If you identify each post individually and then there is a problem with the owner of that post then I can let you resolve the problem with them. I don’t mind helping but I won’t do something that can causes me more work.

You can search for such post.

You have to be on the web site to do this.

  1. Click on the magnifying glass in the upper right.
  2. Select Search this topic
  3. Enter Wang for the search phrase.

A list of topics should display.

Don’t forget to click More at the bottom. :slightly_smiling_face:

35

@EricGT from this post to the last post of this web page, all this stuff would be better placed on the page Improving Wang's algorithm in Prolog

36

The starting post is #161 and the ending post is #174

37

That’s correct !

1 Like
39

Yes. This prover is not good as soon as the formula is not valid…

41

Impressive ! I am going to test it. Thanks Jan, thanks again !

Something goes wrong for me with leanseq2.pl:

?- prove(?[X]:![Y]:(p(X) | ~p(Y))).
ERROR: Syntax error: Operator expected
ERROR: prove(
ERROR: ** here **
ERROR: ?[X]:![Y]:(p(X) | ~p(Y))) . 
?-
42

I forgot to say thank your Eric. I apologize !

44

Done, but here is the very surprising result:

?- true.

?- prove(p => p).
iteration:1
1: iteration:2
1: iteration:3
1: iteration:4
1: iteration:5
1: iteration:6
1: iteration:7
1: iteration:8
1: iteration:9
1: iteration:10
1: iteration:11
1: iteration:12
1: iteration:13
1: iteration:14
1: iteration:15
without stop...
46

:slight_smile: Funny word.

48

I am glad to provide you some stuff to study, but a little bit sad to be not competent enough to follow you easily. I will try nevertheless. Forgive me if I am slow. It is a quality only in philosophy, according to Wittgenstein who wrote:

Philosophy is a race where the winner is the slowest.

Do not ask me the reference, I remember only a conversation with Jacques Bouveresse who quoted this word…

1 Like
50

It is always a good thing to share the same conventions and norms. SWI-Prolog has the merit to be a free software, a merit that is not share by other Prolog distributions. At least we can hope that conventions and norms will be shared on the free side.

51

This is not true for certain. You can see a somewhat decent comparison of Prolog implementations and how they are licensed/distributed here:

Or did you mean that not all Prolog distributions are free software?

PS: or did you mean that Jeke Jeke Prolog is not free software?

52

No. I am aware that they are commercial Prolog (SICStu for example, to mention one of the most famous.)
Before reading Jan’s posts, I did not know Jeke Jeke Prolog.

53

There are other “free software” Prolog implementations (see the Wikipedia page I linked above). Some have licenses that are less permissive than SWI-Prolog’s (in the sense that some people would argue that SWI-Prolog is not “free as in freedom”).

54

@Boris I agree !

58

Thanks Jan. I am interested by ASP solver that I did not know.
I’ve lost my time in trying to change Wang prover in order to implement in it an efficient counter-model finder, and because I am weak in Prolog, I waste too much time… I’ve tried to use the Isabelle-Newbie program and also your boole2.pl , all my tentatives failed until now… :frowning:

60

Your last question is of course relevant. I do not understand if I can use ASP with SWI-Prolog of if I need to use another Prolog.

61

I add that my difficulties to implement a more efficient couter-model prover into Wang prover are caused only by my lack of skills in Prolog. But I take this as an exercise.

65

This is just an opinion that I will almost certainly not be able to back up by writing code and showing what I mean. Either way, I will write it down.

There are two issues in this program that muddle the problem by quite a bit. Both are (or have been?) in vogue so this is definitely not a criticism; just an idea on how to approach it differently.

The two issues:

  1. Defining operators so that the end user can write valid Prolog that looks as similar to the formalism of the original domain as possible;
  2. Interleaving input and output with the underlying logic and algorithms.

The way to do it differently:

  • Define an interface to the underlying algorithm that makes it easy to think about the implementation, and to actually write the code;
  • Use obvious, descriptive data structures;
  • Completely separate the logic from the input and output.

Operators get in the way because if I would be to read this code, I need to first internalize the idiosyncratic notation. The interleaved input and output get in the way because they inflate the code, add noise to whatever is really happening.

There is nothing wrong with exposing to the end user the exact same interface as now, with the operators, and the input/output, but this would be a wrapper for what is really happening.

1 Like
69

I think adding test cases would be great. If this were my code I would be putting the test cases in a plt file and using :- load_test_files([]). in the main file. See: Prolog Unit Tests

If the code is based on other code with a license, you need to add the license.

Also show examples of how to use it, e.g. Here Peter showed how to use the code and because he did I was able to quickly get it working and then I modified my version to my style of work.

EDIT

I tried your code just from this post. It is not working. At this point I would walk away from this. :frowning_face:

This is what happened.

Details 
Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)
% This is on Windows 10

?- working_directory(_,'C:/Users/Eric/Documents').
true.

?- ['Wang''s Algorithm'].
ERROR: c:/users/eric/documents/wang's algorithm.pl:51:22: Syntax error: Operator expected   % formula_simpler(~ ⊥,       ⊤).
ERROR: c:/users/eric/documents/wang's algorithm.pl:52:22: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:53:25: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:54:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:55:24: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:56:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:57:24: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:58:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:59:25: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:60:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:61:25: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:62:26: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:63:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:64:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:65:26: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:66:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:67:26: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:68:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:69:29: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:84:21: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:103:32: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:109:55: Syntax error: Operator expected
true.

% Line 51 in my code is `formula_simpler(~ ⊥,       ⊤).`
% The line count difference is to do to some comments added at the start.

?- qw.
Reminder: your formula must *always* be into square brackets, e.g. [p => p].
|    [p -> p].

% 13,843 inferences, 0.000 CPU in 0.007 seconds (0% CPU, Infinite Lips)
ERROR: Unknown procedure: quine/1
ERROR: In:
ERROR:   [17] throw(error(existence_error(procedure,...),context(...,_31592)))
ERROR:   [15] catch(user:(\+ ...),error(existence_error(procedure,...),context(...,_31648)),prolog_statistics:(...,...)) at c:/program files/swipl/boot/init.pl:481
ERROR:   [14] setup_call_catcher_cleanup(system:true,prolog_statistics:catch(...,...,...),_31688,prolog_statistics:(_31720=true)) at c:/program files/swipl/boot/init.pl:562
ERROR:   [12] prolog_statistics:time(user:(\+ ...)) at c:/program files/swipl/library/statistics.pl:293
ERROR:   [11] getFormula((p->p)) at c:/users/eric/documents/projects/swi-prolog/discourse forum questions/swi-discourse_059/wang's algorithm.pl:124
ERROR:    [9] toplevel_call(user:user:qw) at c:/program files/swipl/boot/toplevel.pl:1113
ERROR: 
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
^  Exception: (14) setup_call_catcher_cleanup(system:true, prolog_statistics:catch(user:(\+quine((p->p))), _18978,  (report(t(1599730614.377056, 0.140625, 271533), 10), throw(_18978))), _32014, prolog_statistics:(_19000=true)) ? creep
   Call: (16) _19000=true ? abort
% Execution Aborted
?- help.
-----------------------------------------------------------

A Propositional Theorem Prover using both Quine's and Wang's Algorithms
by Joseph Vidal-Rosset from Ben Hudson's and Isabelle-Newbie's programs.

https://github.com/benhuds?tab=repositories 

https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in

-----------------------------------------------------------
To test the validity of your formula with Wang's algorithm:
- First, write "qw." and press Enter.
- Second, with this usual syntax: ~ a | a &  b | a v b | a => b| a <=> b| 
put your formula into square brackets (e.g. [p -> p]), press Enter.
That's it. Have fun!
true.

Realized I entered the example formula wrong. In retrying still does not work.

?- qw.
Reminder: your formula must *always* be into square brackets, e.g. [p => p].
|: [p => p].

% 13,446 inferences, 0.000 CPU in 0.007 seconds (0% CPU, Infinite Lips)
ERROR: Unknown procedure: quine/1
ERROR: In:
ERROR:   [17] throw(error(existence_error(procedure,...),context(...,_29726)))
ERROR:   [15] catch(user:(\+ ...),error(existence_error(procedure,...),context(...,_29782)),prolog_statistics:(...,...)) at c:/program files/swipl/boot/init.pl:481
ERROR:   [14] setup_call_catcher_cleanup(system:true,prolog_statistics:catch(...,...,...),_29822,prolog_statistics:(_29854=true)) at c:/program files/swipl/boot/init.pl:562
ERROR:   [12] prolog_statistics:time(user:(\+ ...)) at c:/program files/swipl/library/statistics.pl:293
ERROR:   [11] getFormula((p=>p)) at c:/users/eric/documents/projects/swi-prolog/discourse forum questions/swi-discourse_059/wang's algorithm.pl:124
ERROR:    [9] toplevel_call(user:user:qw) at c:/program files/swipl/boot/toplevel.pl:1113
ERROR: 
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
^  Exception: (14) setup_call_catcher_cleanup(system:true, prolog_statistics:catch(user:(\+quine((p=>p))), _17112,  (report(t(1599731658.67883, 0.140625, 269351), 10), throw(_17112))), _30148, prolog_statistics:(_17134=true)) ? creep
   Call: (16) _17134=true ?