Lab: Propositional Logic in Scheme

CSC261 - Artificial Intelligence - Weinman

Summary:

We explore a representation of propositional logic in Scheme to prepare for implementing a model checking inference algorithm

Preparation

1. Make a directory for this lab.

   mkdir somewhere/propositional

   cd somewhere/propositional
2. Copy the starter files to your new direcdtory

   cp ~weinman/courses/CSC261/code/enumeration/*.scm .
3. Open your Scheme environment and create a new Scheme file called prep.scm in your new directory.
4. Load the utilities by adding

   (load "logic.scm")

   to the top of your new Scheme file.

Exercises

A: Representation

1. In the format given by the lab assignment, write a Scheme expression representing the propositional sentence !A (where ! represents the logical negation).
2. Define a Scheme expression representing the sentence AvB.
3. Define a Scheme expression representing the sentence D ^ true.
4. Define a Scheme expression representing the sentence AvBvC.
   Note: The specification allows only two sentences per or operation-it is a binary operator.
5. Define a Scheme expression representing the sentence (A ^ B) => (C v D).

B: Processing

1. Use get-symbols (from logic.scm) to extract the symbols from your conjunction in A.3.

   (define conjunction-symbols (get-symbols _______))

   Does it produce a result you expect?
2. Similarly, extract the symbols from your disjunction in A.4.

   (define disjunction-symbols (get-symbols _______))

   Are the results sensible?
3. Use list-union (also from logic.scm) to merge these two lists of symbols. Does it produce a result you expect?
4. Use a combination of list-union and get-symbols to get a list of all the symbols from A.4 and A.5. Does it produce a result you expect?

C: Interpreting

1. The simplest kind of atomic sentence is a boolean value. Write a Scheme expression to determine whether sentence is a boolean.
2. The next simplest atomic sentence is a positive literal representing a symbol. Write a Scheme expression to determine whether sentence is of this form.
3. Assuming your sentence is a symbol, write a Scheme expression to determine whether sentence holds for model . You may assume the symbol is defined in the model.
4. Write a Scheme expression (you may use let to bind values for clarity) to determine whether sentence is a negation.
5. Assuming the procedure pl-true? is defined, use it in a Scheme expression to determine whether the given sentence, now determined to have the form (not other-sentence), in fact holds for model.
   That is, evaluate whether other-sentence (which must be extracted from sentence) holds using pl-true?, and process the result accordingly to determine whether sentence in fact holds.
   Hint: You should begin using Scheme's built-in logical operators.
6. Write a Scheme expression (you may use let to bind values for clarity) to determine whether sentence is a conjunction.
7. Use it in a Scheme expression to determine whether the given sentence of the form (and arg1 arg2), in fact holds for model. That is, evaluate arg1 and arg2 (which must be extracted from sentence) using pl-true?, and process the results accordingly to determine whether sentence in fact holds.
   Hint: Use Scheme's built-in logical operators.

Lab Assignment