Numbers

Due: November 2 at 11:59 PM
Please submit your code via WebWork (click here for directions). For questions about the assignment contact Ryan Riegel.

The assignment is worth (TBD)% of your final grade.

Why?

This project is intended to familiarize you with the use of computers to answer questions about propositional and first-order logic. You will code portions of established reasoning algorithms as well as encode a logic puzzle in a format that a computer can understand. The hope is that, as you work on this assignment, you will see that logical reasoning can be rendered into a relatively simple methodical process.

This project is to be completed in LISP. By now, you should all have enough experience with the language that the following will not pose to much difficulty with regards to programming.

Part I: Syntax Specifications (0%)

1. Propositional Logic:

   s	->	atom | complex
   atom	->	symbol | value
   symbol	->	p | q_3 | isRaining | ...
   value	->	t | nil
   complex	->	(_not s) | (_and s s) | (_or s s) | (_implies s s) | (_iff s s)

   Example: (_iff (_implies p q_3) (_not (_and p (_not isRaining))))

2. Models for PL:

   m	->	(pairs)
   pairs	->	&epsilon | pair pairs
   pair	->	(symbol value)

   Example: ((p t) (q_3 nil) (isRaining nil))

   Note that &epsilon is used to express nothingness in context-free grammars; the above simply indicates that models are represented with lists of pairs.

3. First-Order Logic (simplified: no functions, variables assumed universal):

   s	->	atom | complex
   atom	->	(predicate terms) | (_equals term term)
   predicate	->	Brother | OnHead | Evil | ...
   terms	->	epsilon | term terms
   term	->	(_const constant) | variable
   constant	->	John | Crown | M_1 | ...
   variable	->	x | y | z | ...
   complex	->	(_not s) | (_and s s) | (_or s s) | (_implies s s) | (_iff s s)

Part II: Model Checking (30%)

1. (10%) We'll start off with some handy (and relatively simple) functions for working in the domain of logic. These functions will be useful later in the assignment, so it is important that they work correctly.
   1. Write a function pl-true that decides if a sentence in propositional logic is true under a given model. For instance,

      (pl-true '(_implies (_or a b) c) '((a t) (b nil) (c t)))

      should return t (or any non-nil value), but

      (pl-true '(_or a (_and b c)) '((a nil) (b nil) (c t)))

      should return nil. You can assume that the model will always contain all of the symbols used in the sentence.

   2. Write a function pl-symbols that finds all of the symbols used in a list of sentences. For instance,

      (pl-symbols '((_implies x y) (_or z (_implies y z)) (_or (_not z) nil) w))

      should return the list (x y z w). The order of returned symbols does not matter.

2. (10%) A simple but effective approach to proving entailment and logical equivalence is to enumerate all possible valuations of the involved symbols. Because a number of tasks can be accomplished by enumeration, we will attempt to be completely general. Write a function mc-fold that accumulates the result of applying an input function to each possible model for a given list of symbols. The function should accept arguments of the form:

   (mc-fold f acc0 symbols)

   If symbols is '(a b), the result of the above should be equivalent to:

   (f '((a nil) (b nil))
      (f '((a nil) (b t))
         (f '((a t) (b nil))
            (f '((a t) (b t)) acc0))))

   The order in which models are processed does not matter. Also note that any input function f used with mc-fold should expect a model for its first argument and the accumulator (a return value of the previous call to f) for its second.

   Because there are O(2ⁿ) models for n symbols, this function will have an exponential running time. You should, however, try to implement the function such that its space complexity is only O(n) provided that the size of f's results don't grow as the chain shown above evaluates. In other words, use recursion to generate and process possible models rather than creating all models upfront and applying f to them in series. Look at the TT-Entails? function on page 209 of Russell/Norvig for inspiration.

3. (5%) The mc-fold function is highly versatile. To get a feel for its uses, define functions:
   1. count-worlds, which simply calls mc-fold with an input function that ignores the model and adds 1 to the accumulator. The result should be 2ⁿ, where n is the number of symbols.

      (count-worlds '(x y z u v)) => 32

   2. enumerate, which calls mc-fold with a familiar built-in to generate a list of all possible worlds.

      (enumerate '(a b)) => (((a nil) (b nil))
                             ((a nil) (b t))
                             ((a t) (b nil))
                             ((a t) (b t)))

   3. filter, which generates a list of models in which a given sentence is true.

      (filter '(_implies p (_and q r)) '(p q r))) => (((p nil) (q nil) (r nil))
                                                      ((p nil) (q nil) (r t))
                                                      ((p nil) (q t) (r nil))
                                                      ((p nil) (q t) (r t))
                                                      ((p t) (q t) (r t)))

      This function should not rely on enumerate to work, but should instead call mc-fold directly with a slightly more complicated input function.

4. (5%) Recall that a Knowledge Base (KB) is said to entail a sentence if, whenever all sentences within the KB are true, the sentence in question is also true. Further, a sentence is said to be valid if it is true under all possible worlds.
   1. Again using mc-fold, write a function mc-entails that tests whether a KB (encoded as a list of sentences) entails a given sentence. This function should have linear space complexity for all inputs.

      (mc-entails '((_or x (_or y z)) (_not x) (_implies y z)) 'z) => t
      (mc-entails '((_implies a b) (_implies b c) a) '(_or c d)) => t
      (mc-entails '(p (_implies q p)) '(_iff p q)) => nil

   2. Define a function mc-valid that tests whether an input sentence is valid with a simple call to mc-entails.

      (mc-valid '(_or a (_not a))) => t
      (mc-valid '(_implies (_implies (_implies p q) p) p)) => t
      (mc-valid '(_iff (_and x (_or y z)) (_or (_and x y) z))) => nil

Part III: Resolution (35%)

1. (10%) Recall that Conjunctive Normal Form (CNF) is a special form of sentences that consists strictly of a conjunction of disjunctions of literals (i.e., clauses of symbols or not-symbols all or'd together, which are themselves and'd together), and that every sentence in propositional logic has an equivalent sentence in CNF.
   1. Define a function cnf that converts an arbitrary sentence in propositional logic into Conjunctive Normal Form. This accomplished in three steps:
      1. Eliminate all implications and biconditionals by replacing them with combinations of conjunctions, disjunctions, and negations.
      2. Push all negations as deep as possible using the de Morgan laws. Don't forget to eliminate double negations.
      3. Distribute disjunctions over conjunctions as frequently as possible.

      Some examples of the function's behavior are as follows:

      (cnf '(_and (_implies a b) c)) => (_and (_or (_not a) b) c)
      (cnf '(_not (_or (_not p) q))) => (_and p (_not q))
      (cnf '(_or x (_and y (_and z w)))) => (_and (_or x y) (_and (_or x z) (_or x w)))

   2. Because it is often more convenient to work with lists rather than trees, and because conjunctions and disjunctions are both associative, define a function cnf-list that converts an arbitrary sentence into a list of lists of literals, representing CNF. The examples above change as follows:

      (cnf-list '(_and (_implies a b) c)) => (((_not a) b) (c))
      (cnf-list '(_not (_or (_not p) q))) => ((p) ((_not q)))
      (cnf-list '(_or x (_and y (_and z w)))) => ((x y) (x z) (x w))

      Note that the inner lists in this representation (the disjunctions) are refered to as clauses in later parts of this assignment. At this point it is fairly easy to remove meaningless duplicates of the same literal in each clause; you should do this. If you are an over-achiever, go ahead and remove entire clauses if they contain both positive and negative literals for the same symbol, as well as duplicate clauses if they occur.

2. (15%) Resolution is a more advanced technique than model checking for determining entailment, validity, etc. While its running time is still exponential in general, it can be much quicker than model checking in many situations, and unlike other inference methods, its process is particularly simple. For this assignment, you will not fully implement resolution, but instead will implement the subtask of detecting and handling clashes between clauses in CNF sentences.

   Two clauses are said to clash on a literal when they contain complementary versions of that literal (e.g., one contains a, and the other (_not a)), and are resolved by unioning all other literals within the clauses. Write a function clash that returns a list of all possible clash resolutions between two clauses, or the empty list if there are none.

   (clash '(p q r) '((_not p) q (_not s))) => ((q r (_not s)))
   (clash '((_not x) y) '(x (_not y))) => ((y (_not y)) ((_not x) x))
   (clash '(a b) '(c (_not d))) => ()
   (clash '((_not p)) '(p)) => (())

   Note that the last two terms are very different from each other. The former indicates that no clashes were possible, with minimal significance to the process of resolution, while the later indicates that the clash resulted in box (yet another way of saying the empty list), meaning that the sentence considered by resolution is in fact unsatisfiable.

3. (10%) Code for the rest of the resolution algorithm is provided to you in utils3.lisp. Using the pl-resolution function, write functions:
   1. res-entails, which determines if a KB entails a given sentence.
   2. res-valid, which determines if the input sentence is valid.

   These two functions should accept the same arguments as their model checking counterparts, and should have the same behavior. If you're feeling adventurous, compare running times between to two versions for various inputs. Also, keep in mind that resolution is officially a satisfiability checker that operates on a single list of clauses (as returned by cnf-list), so you'll have to process the above inputs in some way before you can pass them off to the pl-resolution function.

Part IV: First-Order Logic (35%)

1. (15%) Unification is the process of finding a variable substitution for two sentences in first-order logic that makes them look identical, and is instrumental in first-order logic inference algorithms. Define a function unify that accepts two sentences and returns either a list of substitution pairs or the LISP symbol failure if unification is impossible. Note that this function cannot return nil to indicate failure because nil, the empty list, actually indicates no substitutions are needed because the sentences are already identical.

   (unify '(Knows (_const Bill) (_const Bob)) '(Knows y (_const Bob))) => ((y (_const Bill)))
   (unify '(Knows (_const Bill) x) '(Knows y (_const Ted))) => ((x (_const Ted)) (y (_const Bill)))
   (unify '(Gaseous a) '(Gaseous b)) => ((a b))
   (unify '(_and (Cat x) (Owns y x)) '(_and (Cat x) (Owns y x))) => nil
   (unify '(_and (Cat x) (Owns y x)) '(_or (Cat z) (Owns w z))) => failure

   Look at page 278 of Russell/Norvig for the specifics of this algorithm. Note that in our representation of sentences makes compounds (uses of logical symbols and predicates) look very similar to argument lists. You may want to define a helper function to handle lists, rather than use type checking as indicated in the book. Also, don't worry about standardizing apart; you can assume this is done before your unify function is called. Lastly, keep in mind that you should only substitue variables with terms (in our syntax, this means constants or other variables, but in general function applications are included as well); the structure of sentences in first-order logic should prevent other substitutions from being considered, so you don't need to worry about this too much.

2. (15%) The next logical step is to have you program forward-chaining, but this assignment is already long enough, so this function is provided as fol-fc-ask in utils3.lisp. Your task is instead to make use of this function to solve the logic puzzle provided in puzzle.txt.

   First off, the puzzle provided to you is in English! Define a parameter puzzle-kb that expresses the puzzle as a list of first-order definite clauses (needed for forward-chaining to work). Recall that a definite clause is a disjunction that contains at most one positive term (i.e., only one term that isn't precluded by _not). Alternately, definite clauses may be represented as an implication of a single term by a conjunction of terms, where all terms are positive. In other words, it should either look like

   (_or (_or (_or (_not (Fungus x)) (_not (Orange x))) (_not (Slimy x))) (Poisonous x))

   or like

   (_implies (_and (_and (Fungus x) (Orange x)) (Slimy x)) (Poisonous x))

   Also,

   (Consumed (_const Bob) (_const TheMushroom))

   is considered a definite clause because it is, after all, just one positive term.

   The fol-fc-ask function actually operates on list structures that represent definite clauses, but there is a provided function definite-list that converts either of the above into an acceptable format. Make sure to use it in your solve-puzzle function below. Students who have read ahead might find some of this function's components useful in defining cnf. Also note that you must not use any numbers as variable names in your KB; fol-fc-ask uses numbers to standardize apart, and your use of them could cause conflicts. It's okay to use numbers in variables names, just not as them.

3. (5%) Use the fol-fc-ask function and the KB you specified above to define a function solve-puzzle that solves the puzzle for each unknown variable. Note that fol-fc-ask accepts a list of query terms and works to answer each of them in parallel.

   (solve-puzzle) => ((Murderer ???) (MurderWeapon ???) (SceneOfTheCrime ???))