Logic Programming

Assignment - Satisfiability

Consider the representation of formulas of Boolean logic described in Chapter 12. You can assume that there are just three propositions p, q, and r, and you can assume that complex expressions are represented using not, and, and or.

Your goal in this assignment is to define a unary relation, called satisfiable, that is true of a propositional sentence represented in this way if and if the sentence is satisfiable, i.e. if and only if there is some truth assignment that makes it true.

Your definition should allow Sierra to determine the satisfiability of any given propositional sentence. For example, it should enable Sierra to determine that satisfiable(p) is true, satisfiable(not(p)) is true, satisfiable(or(p,not(p)))is true, and satisfiable(and(p,not(p))) is false.

Ideally, your definition should also allow Sierra to generate satisfiable sentences. For example, if you ask the Sierra query tool to return 5 results for the pattern P such that the query satisfiable(P) is true, it should generate 5 satisfiable sentences, such as p, q, r, not(p), not(q).

Extra credit: Create a version that works for an unspecified number of proposition constants. Okay to write unsafe rules so long as the Epilog interpreter returns the correct answer when asked to compute the satisfiability of a specific formula (i.e. there are no variables in the query).