Improving Wang's algorithm in Prolog

Help! Algorithm
70

@EricGT . Thanks for your comment.

In the file, there is an help command (that should be inside any program, I agree):

?- true.

?- 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.

?-

Now, I would be pleased to add tests, but again, it is hard for me to understand the documentation, in spite of the examples that are given. I am very sorry to be so slow.

72

@EricGT

You wrote:

[p -> p].

instead of :

[p => p].

Hence the errors.

1 Like
73

Yes. You are right.

I noticed that also and updated the earlier post.

Still getting errors. :frowning_face:

76

@j4n_bur53
The use of square brackets is not mine, it is in Ben Hudson’s program for Wang’s prover. I would be glad to find another option, adapted for any Prolog, but I do not know how to do. If the problem is only the level of priority given to => , that’s another point that could be easily solved, I guess.

77

(post deleted by author)

78

If I understand you well, the correct input should be :

p => p.

and never

[p => p].

Right ?
I will have a look again on Ben Hudson’s program with your suggestion, maybe this afternoon. But I am not sure to understand. For example the square brackets in this rule :

prove(L --> R):-
	member(A & B,L),
	del(A & B,L,NewL),
	nl,write(' \t'),write([A,B|NewL] --> R),
	write('  \t (by and/left)'),
	prove([A,B|NewL] --> R).

should be changed, or not?

79

(post deleted by author)

80

Yes, there is a second comment “flagged by the community”. I don’t see any obvious reasons for that. Maybe it is because it repeats things that were already discussed in the linked github issue?? Maybe it has something to do with the diabolical symbolism of the issue number? Is it triggering a bot? I am also confused.

82

Your point why this is problematic is clear (to me). JanW’s point as to why he won’t fix it as you suggest is also clear (to me). What remains mystery is why the hidden posts, or how I can “vote” to unhide them, if I don’t consider them to be that offensive or otherwise breaking the rules of the forum. It would be also nice if a hidden/flagged post comes with a reason why.

PS: “Flagged by the community” smells of all kinds of things that I feel very icky about.

83

(post deleted by author)

84

Fine, but do you know that or are you guessing? I still would appreciate an explicit reason for flagging posts, visible to everyone. Because I did not flag whatever you wrote: does that mean I am definitely not part of the community? Either way, this opens all kinds of questions that have nothing to do with the technical aspects.

85

(post deleted by author)

87

I now read the FAQ. There is a lot of room for interpretation, so basically we are at the mercy of those who interpret the rules. Welcome to the Brave New World! :slight_smile:

1 Like
88

@j4n_bur53
I am very sorry that in providing to me help on Ben Hudson’s program for Wang algorithm, you have been involved in a more general discussion that does not seem to me very friendly. I must say that, in general, I do not understand censoring. But that is my philosophical contention and it is not the topic of this web-page.

I will do my best to solve the brackets problem in this program. If I am definitely too weak, I will ask help again.

2 Likes
89

See: So What Exactly Happens when you “Flag”?

As for the message “flagged by the community” I can find no setting that will allow for the changing of the message.

91

@j4n_bur53 Really I would be glad to avoid to users the use of square-brackets, but all my tentative fail at the moment. I do not succeed to get Ben Hudson working without input formulas inside square-brackets. It has been easy for Quine Isabelle-Newbie program to get back to the normal situation (i.e. input formulas free of square brackets) but for Wang part, it is not so easy, at least for me…

92

Done !

go([] --> [Formula]).

That’s it !

93

@EricGT

Is it true that Jan Burse has been blocked here? @j4n_bur53 I am worry about this possibility.

95

I am reassured. Thanks !

97

This still does not work with SWI-Prolog for me.