Return To The Balladvanced series
Here is an exercise to check your understanding of the way clauses are read.
If you are doing the exercises in order, you will already have seen the Logicians’ Ball puzzle and probably solved it by writing the constraints as first order formulae—though as it does not require quantifiers, the logic is essentially propositional. Now you are to do it again, but using clauses instead of full propositional logic notation. Having done that, you are to re-express it by transforming the clauses into equivalents with some restrictions.
Start by turning on “clause form” from the Settings menu.
The key to it is that in any clause, a literal of the form “NOT (___)” may equivalently be moved over to the other side of the arrow and the “NOT” removed. Try to work out why that is the case from the definition of clauses on the “Clause form” page of the guide.
Clauses may not have the consequent side empty. However, the boolean constant “FALSE” may always be used to stand in for an empty consequent if desired.
1. Express the “Logicians’ Ball” puzzle from the “Advanced” list keeping the same sort and function symbols as you used when you did it the first time, but this time in pure clause form, without using the boolean operators “NOT”, “AND” and “OR”.
2. Having done that, now try expressing it without using AND or OR (NOT is allowed) and without any clauses with multiple consequents.
3. Finally, express it without “AND”, without “OR” and without using the arrow “->” in clauses.
Solver
Auto Parser Results
No errors found.