Due Monday, Jan 29 @ 5:00pm
Here is a slight variant of our definition of propositions:
P ::= P -> P | P /\ P | P \/ P | ~P
| true | false
| A
A ::= Symbol
We have specified that the atomic propositions are just Symbols because we do not care about their structure for this assignment.
Look at the lecture notes from Jan 23 to find out about interpretations. We used them in class (it was that undefined function α, all of whose possibilities we enumerated in the truth tables), but I didn't get a chance to talk about how to represent it in your ACL2 programs. I'll say more about that on Friday, but read the notes and get started on the assignment before that!
Design an ACL2 program valid? that consumes a proposition P and determines whether or not |= P.
Design an ACL2 program satisfiable? that consumes a proposition P and determines whether or not P is satisfiable.
Design an ACL2 program unsatisfiable? that determines if a given proposition is unsatisfiable.
Design an ACL2 program invalid? that determines if a given proposition is invalid.
Design a program find-satisfying-interpretation that gives a proposition and produces a satisfying interpretation if at least one exists. If none exist, produce nil.
Design a program find-counterexample that consumes a proposition and produces an interpretation that makes the proposition false.
When the propsition is valid, then no such interpretation exists. Produce nil in this case.
Hint: The design recipe should lead you to develop several helper functions for #1. If you do it properly, then the rest of the solutions should be relatively short and sweet. If you don't design properly, then you may find this assignment to be far more time-consuming than it ought to be.