CS212
Problem SetsProblem Set 3 - Spring 1999
Predicate Calculus
CS212
Problem Sets
Problem Set 3 - Spring 1999
Predicate Calculus
As you can see, this problem set is quite lengthy and it may take you some time to familiarize yourself with the mathematical concepts that will be use throughout the problem set. However, we want to make it clear at the beginning that you are not responsible for all the math details. So don't feel nervous if you find yourself completely lost about the math. We only expect a brief understanding so that you know what's going on.
For this assignment, you can work in pairs. If you choose to work in pairs, you must only submit one copy of your solution using the online submission system.
If you have trouble with the course software or are generally stuck, come to our office hours or consulting hours. Alternatively, post a question to the newsgroup cornell.class.cs212. As a last resort, send email to cs212@cs.cornell.edu.
Boolean logic lies at the very heart of computer science. Indeed, the CPU you are using is composed of literally millions of relatively simple logic gates. In this problem set, we will implement a set of Scheme functions that will let us write propositional calculus (the simplest form of boolean logic) formulas and manipulate them in various ways.
The propositional calculus deals with propositions. A proposition is simply a statement that can be either true or false. Some examples of propositions are:
In the propositional calculus, we represent propositions using propositional variables, for example p, q, r.
We can combine several propositions together using logical connectives. Thus we define a propositional formula as either:
The constant true is a formula that is always true. The constant false is a formula that is never true.
In this problem set, we shall deal with the following connectives:
Here are some examples of formulas:
Suppose that p stood for "It is raining", r for "John Cleese is short", s for "John Cleese has a silly walk", a for "Today is Tuesday", b for "It is Thursday", and c for "I have CS212 today". Then the preceding formulas could be informally interpreted in English as:
We would like to determine whether a given formula f is true or false. This depends only upon whether the propositional variables within the formula are true or false. That is, if we are told whether or not the propositional variables p1,...,pn are true, and we have a formula f built out of those variables, then we can determine whether or not the entire formula is true. We do so by employing the following truth table which tells us how to determine true formulas built out of connectives and sub-formulas:
X Y X & Y X | Y X=>Y ~X
1. true true true true true false
2. true false false true false false
3. false true false true true true
4. false false false false true true
Read the first line as "if X is true and y is true, then X&Y is true, X|Y is true, X=>Y is true, and ~X is false." Similarly for the other lines. So, for instance if p is true and q is false, then the formula (p & (~p | q)) => q is true because:
Sometimes, we can determine that a formula is true regardless as to whether its propositional variables are true or false. For instance, no matter what p is, p | ~p is always true. When a formula is always true independent of its variables, we say the formula is valid.
We will represent propositional variables using symbols. (We will discuss symbols in sections so don't fret if you're not familiar with them yet.)
(variable? 'p) ; 'p is the symbol p -- kind of like the string "p" in Java ==> #t (variable? '(p r)) ; '(p q) is read as a list of the symbols 'p and 'q ==> #f (variable? 42) ==> #f (variable? #f) ==> #f (variable 'mimsy-borogrove) ==> #t
Formulas will be represented as lists. For example, the formula (((p & q) | (q & r)) => (~p | ~r)) would be represented as:
(define example-formula '(implies (or (and p q) (and q r))
(or (not p) (not r))))
This is equivalent to (and much more compact than):
(define example-formula (list 'implies (list 'or (list 'and 'p 'q)
(list 'and 'q 'r))
(list 'or (list 'not 'p)
(list 'not 'r))))
In addition, we have provided you with the following functions that would be helpful in implementing the rest of this problem set; to see how these are defined you should read the ps3.ss file that we have provided for you.
; formula? returns true if its argument looks like a formula: ie, if it is a list... (formula? '(and p q)) ==> #t (formula? 'p) ==> #f (formula? 42) ==> #f ; ...but the list can be something that doesn't look like a formula at all (formula? '(a b c)) ==> #t ; op returns the operator of a formula (op '(and p q)) ==> and (op '(implies (and a b) (or c d))) ==> implies ; terms returns the list of the immediate subformulas of a formula (ie, the terms of the operation) (terms '(and p q)) ==> (p q) (terms '(or (implies a b) (implies a (not b)))) ==> ((implies a b) (implies a (not b))) ;nary-op? returns true if the operator of the given formula is one of and, or, or implies (nary-op? '(or p q)) ==> #t (nary-op? '(not b)) ==> #f ;unary-op returns true if the operator of the given formula is not (unary-op? '(or p q)) ==> #f (unary-op? '(not b)) ==> #t
Please be sure to read the ps3.ss file, as it contains many other functions that will make the problem set a lot easier to implement.
Write the function wff? that takes a single parameter, and returns #t
if that parameter is a well-formed-formula, or #f otherwise. For the purposes of
this problem, a well-formed formula is the smallest set such that:
Here's some sample output:
(wff? 'foobar) ==> #t (wff? '(or p q)) ==> #t
(wff? 'true) ==> #t (wff? '(implies (or p q r) (not (and q r)) p) ==> #f (wff? '(foo bar)) ==> #f (wff? 42) ==> #f
What to turn in: For this problem, turn in your code for the function wff? as well as for any additional code that you may have written in implementing wff?. Important: Include an informal proof of correctness in the comments before your code. Make your code bullet proof -- it should not generate a run-time error regardless of the input.
Currently, we only consider unary uses of not and binary uses of and, or, and implies. not only makes sense with one argument, and one could argue about the correct meaning for n-ary implication, but the other connectives could easily take a higher number of arguments. The meaning for n-ary and (and similarly, or) is intuitive: (and e1 e2 ... en) is true iff e1 is true, e2 is true, ..., and en is true. You are responsible for supporting n-ary versions of all the binary connectives: and, or, implies. They should all associate to the right.
To allow us to use everything that you develop in this problem set on n-ary connectives without additional hassle, we'll simply introduce a translation from n-ary to binary forms. Write a function nary->binary that takes a formula with n-ary uses of these connectives, and returns a formula in which these uses have been reduced to binary form. (Note that you must produce a formula that passes the wff? test to solve this problem.)
Note: you should handle the cases (and x), (and), (or x), and (or) as well. Think about what these should mean, and handle them accordingly. (Hint: what does Scheme do with these cases? Why?) Again, make your code bullet proof.
In the tableau proof method for determining valid formulas (which we will see below), we will need a list of the propositional variables that occur in a formula. Write a function find-variables that takes a (well-formed, binary) formula and returns a list of all variables that occur in it. Each variable in the formula f should appear exactly once in the list returned by (find-variables f), regardless of how many times it appears in f. (The order of the variables does not matter.)
(find-variables 'x) ==> (x) (find-variables '(implies (and x (or y w)) (not z))) ==> (w x y z) (find-variables '(and x (and x (or x (implies x x))))) ==> (x) (find-variables '(or true false)) ==> (false true) (evaluate 'true (empty-var-assignment)) ==> #t (evaluate 'false (empty-var-assignment)) ==> #f
To do the tableau method of proof, we need to be able to determine when there is a contradiction, i.e., when a variable has been assigned both true and false in the same path. We could write down a very rigorous and detailed contract for a variable assignment (represented by rho), as follows:
(var-assigned? x (empty-var-assignment)) --> #f (var-assigned? x (extend x val rho)) --> #t (var-assigned? x (extend y val rho)) == (var-assigned? x rho) (var-value x (extend x val rho)) --> val (var-value x (extend y val rho)) == (var-value x rho) (var-value x (empty-var-assignment)) --> 'undefined
(Here x and y are assumed to be different symbols.) A more high-level description is this: empty-var-assignment creates a "blank" assignment in which no variables have been assigned to truth values, and extend adds a single variable-value binding to an existing assignment. var-assigned? determines whether a variable is bound within a truth assignment, and var-value returns the truth value bound to any assigned variable and undefined if no value has been assigned.
Given any variable x, an assignment rho assigns #t or #f to x, or has no value assigned to x. The code for this problem set implements this using association lists. You should understand how this works and what the precise roles of each of these functions is.
Without violating the abstraction barrier of the implementation of assignments (take a quick look at question 8, to see why), write a function evaluate that, given any variable assignment which has values for all free variables of a formula, determines the truth value of the entire formula under this assignment.
If you ever run across a variable that has no value in the assignment, return the symbol undefined.
(define rho (extend 'x #t (extend 'y #f (empty-var-assignment))) ==> ... (evaluate 'x rho) ==> #t (evaluate 'y rho) ==> #f (evaluate 'z rho) ==> undefined (evaluate '(and x y) rho) ==> #f (evaluate '(implies (or x y) (and x y)) rho) ==> #f
In some situations, it is desirable to take a "high-level" formula and translate it to a "lower-level" formula that is equivalent. By equivalent we mean that, no matter what truth values you assign to the variables of the formulas, when you evaluate them, you get the same thing. For example, some CMOS hardware chips only provide the functionality of not and and. But hardware designers want to express their logic using connectives like implies and or as well as not and and. So they need a tool to translate their high-level logic descriptions down to low-level formulas that can be implemented directly by the chips. (You'll learn more about this in CS314.) Of course, we can't translate away all of the connectives, but we can sure get rid of a lot of them.
For instance, we can encode the formula (X & Y) as ~((~X) | (~Y))) thereby eliminating and in favor of not and or. Using the truth table, it is easy to see that regardless as to whether or not the formulas X and Y are true, these two formulas evaluate to the same thing:
X Y X&Y ~X ~Y (~X | ~Y) ~(~X | ~Y) -- -- --- --- --- --------- ---------- #t #t #t #f #f #f #t #t #f #f #f #t #t #f #f #t #f #t #f #t #f #f #f #f #t #t #t #f
For this problem, you will write a function simplify that takes a well-formed (binary) formula and translates it to an equivalent formula that uses implies as the only connective. To do so, you must figure out how to replace formulae of the form ~X, X&Y, and X|Y with some combination of X, Y, true, false, and =>.
What to turn in: For this problem, turn in your code for simplify.
For this problem, please write a function conflicts? that takes a variable, a truth value, and a variable assignment and returns #t if the given variable is in the variable assignment and the truth value is different from the assignment that is passed to conflicts?. For example:
(conflicts? 'x #t (empty-var-assignment)) ==> #f (conflicts? 'x #t (extend 'x #t (empty-var-assignment))) ==> #f (conflicts? 'y #f (extend 'y #t (empty-var-assignment))) ==> #t (conflicts? 'z #f (extend 'borogrove #f (empty-var-assignment))) ==> #f (conflicts? 'false #t (empty-var-assignment)) ==> #t (conflicts? 'false #f (empty-var-assignment)) ==> #f
What to turn in: For this problem, please turn in your definition of conflicts? as well as any helper functions that you wrote that it calls.
One of the things which it is very useful to know about a propositional formulas is whether or not it is tautology -- that is, whether it is true for all possible truth assignments to its variables.
One way to decide whether a formula is a tautology is to consider all the possible truth assignments, and then to see if under at least one of them, the formula evaluates to false. If there exists such a falsifying assignment, then you know that the formula cannot possibly be a tautology.
The problem with that method, however, is that it always runs in exponential time in the number of free variables in the formula -- that's easy enough to see; it essentially tries to build a truth-table for the formula, and in the worst case it will have to try all 2n (where n is the number of propositional variables in the formula) combinations before it can prove that a formula is a tautology.
In this problem we consider an alternative method. In the worst case this method also runs in exponential time. However for most formulas, the modified block-tableau method will actually perform a lot faster than the truth-table method.
The tableau method concerns itself with signed formulas, that is, formulas adjoined with a truth value (written F[X] if X is a false formula, and T[X] if X is a true formula).
Given a signed formula, we can state certain facts about its immediate sub-formulae. For example, if the formula X | Y is false, then we know that both X and Y are false, because that is the only way that we can make the entire thing false. All in all there are the following inference rules (ie, given the a certain formula, we can deduce some things about the sub-formulas):
Here X and Y are formulas Know Can deduce Rule type T[(and X Y)] T[X] and T[Y] alpha F[(and X Y)] F[X] or F[Y] beta T[(or X Y)] T[X] or T[Y] beta F[(or X Y)] F[X] and F[Y] alpha T[(implies X Y)] F[X] or T[Y] beta F[(implies X Y)] T[X] and F[Y] alpha T[(not X)] F[X] F[(not X)] T[X]
Notice that there are two types of formula rules: these are called alpha-type formulas and beta-type formulas in the literature. alpha-type formulas are those for which you can conclude something about both sub-formulae, and the beta-type formulas are those where you can only conclude at least one of the statements about the sub-formulae.
The tableau method for determining tautologies is the following: in order to find a satisfying assignment for a formula (ie, one that makes the formula evaluate to true), we assume that the formula is true, then by recursively applying the tableau rules on the sub-formulae until we reach a point where either all the signed formulae are signed variables (in this case, the truth values of the variables are exactly what they're signed with), or until a contradiction falls out (ie, we try to assign both true and false to some variable).
In implementing block tableau, we simply keep a list of sub-formulae that we have not used yet, and an assignment which contains any variables that we have deduced. We take the top signed formula in the formula list, take the top formula off the list, and replace it by the sub-formulas, as follows:
An important thing to notice is that if we do as many alpha-type formulas first as possible, we can delay branching until the last possible minute. That way, it is possible that we will reach a contradiction in assignments earlier, without having to duplicate the work.
Example: consider the signed formula F[((p => q) & (q => r)) => (p => r)]. Here is what a tableau for trying to satisfy this formula would look like (in this tableau, we try to use all alpha-type rules as early as possible):
F[((p=>q) & (q=>r))=>(p=>r)]
T[(p=>q) & (q=>r)], F[p=>r] ;alpha rule F[X=>Y] |- T[X], F[Y]
T[p=>q], T[q=>r], F[p=>r] ;alpha rule T[X & Y] |- T[X], T[Y]
T[p],F[r],T[p=>q], T[q=>r] ;alpha rule F[p=>r] |- T[p], F[r]
T[p],F[r],F[p],T[q=>r] ;first branch of beta T[p=>q] |- F[p] or T[q]
;...and its a contradiction! p can't be both T and F
T[p],F[r],T[q],T[q=>r] ;second branch of beta T[p=>q] |- F[p] or T[q]
T[p],F[r],T[q],F[q] ;first branch of last beta rule: T[q=>r] |- F[q] or T[r]
...contradiction!
T[p],F[r],T[q],T[r] ;second branch of last beta rule...contradiction!
Since there are no more branches that we can take, we say that the tableau is closed, and that there is no such variable assignment that will make that formula false.
And here's is what the block tableau for this formula would look like if we applied the tableau rules in a haphazard manner (actually, this is the worst-case example of applying all the beta rules we can as early as possible:
F[((p=>q) & (q=>r))=>(p=>r)]
T[(p=>q] & (q=>r)), F[p=>r] ;alpha rule F[X=>Y] |- T[X], F[Y]
T[p=>q], T[q=>r], F[p=>r] ;alpha rule T[X & Y] |- T[X], T[Y]
F[p], T[q=>r], F[p=>r] ;first branch of beta rule T[p=>q] |- F[p] or T[q]
F[p],F[q],F[p=>r] ;first branch of beta rule T[q=>r] |- F[q] or T[r]
F[p],F[q],T[p] ;contradiction!
F[p],T[r],F[p=>r] ;second branch of beta rule T[q=>r] |- F[q] or T[r]
F[p],T[r],T[p] ;contradiction!
T[q], T[q=>r], F[p=>r] ;second branch of beta rule T[p=>q] |- F[p] or T[q]
T[q],F[q],F[p=>r] ;first branch of beta rule and a contradiction
T[q],T[r],F[p=>r] ;second branch
T[q],T[r],T[p],F[r] ;alpha rule and a contradiction!
For this problem, you are given functions alpha-type? and signed-terms which tell you whether a given signed formula is an alpha type or not and what the signed sub-terms of the formula are, respectively; you are to write a function satisfy that takes a formula (say X), and tries to find a satisfying assignment for it using the modified block-tableau method. (That is, it starts with the signed formula T[X] and tries to find a satisfying assignment by applying the tableau rules repeatedly). If there is no such assignment, the function should return #f.
If you want, you can write satisfy in such a way that it tries to apply all alpha rules that it can before trying any beta rules.
We have several helper functions written for you that you can use to keep track of variable assignments. Your function should notice when the formula it is operating on is just a simple signed variable, and check if the truth value of the variable contradicts the one in the current assignment; if not, the value should be added to the assignment, if it does, you know you've reached a contradiction and that tableau branch can be closed off.
In addition, we wrote a function tautology? that is implemented it terms of satisfy that returns #t if the formula is a tautology, otherwise it returns the assignment that makes the formula false.
(satisfy '(or p q)) ==> ((p #t)) [or ((q #t)) depending on your implementation] (satisfy '(and (or p (not q)) q)) ==> ((p #t) (q #t)) [or ((q #t) (p #t))] (tautology? '(implies (and (implies p q) (implies q r)) (implies p r))) ==> #t (tautology? '(implies (implies p q) p) ==> ((p #f)) [or ((p #f) (q #t))]
What to turn in: For this problem turn in all code related to the satisfy function that you wrote.
References: DLN's Automated Theorem Prover (it only works for Modified Block Tableaux, and please note that the syntax of DLN's ATP is different from this problem set).
In this problem, you will re-implement variable assignments, using functions instead of lists. Recall the contract for the variable assignment functions from question 4:
(var-assigned? x (empty-var-assignment)) ==> #f (var-assigned? x (extend x val rho)) ==> #t (var-assigned? x (extend y val rho)) == (var-assigned? x rho) (var-value x (extend x val rho)) ==> val (var-value x (extend y val rho)) == (var-value x rho) (var-value x (empty-var-assignment)) ==> undefined
Rewrite the functions empty-var-assignment, extend, var-assigned?, and var-value using functions instead of lists. Your representation of a variable assignment rho should maintain the invariant that
(rho 'x) ==> #t iff rho maps x to #t
(rho 'x) ==> #f iff rho maps x to #f
(rho 'x) ==> undefined otherwise