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
- Make a directory for this lab.
-
mkdir somewhere/propositional
cd somewhere/propositional
- Copy the starter files to your new directory
-
cp -R ~weinman/courses/CSC261/code/enumeration/* ./
- Open your Scheme environment and create a new Scheme file called prep.scm
in your new directory:
-
touch prep.scm
drracket prep.scm &
- Load the utilities by adding
-
(load "logic.scm")
to the top of your new Scheme file.
Exercises
A: Representation
- In the format given by the lab assignment, write a Scheme expression
representing the propositional sentence !A (where ! represents
the logical negation).
- Define a Scheme expression representing the sentence AvB.
-
Define a Scheme expression representing
the sentence D ^ true.
-
Define a Scheme expression
representing the sentence AvBvC.
Note: The specification allows only two sentences per or
operation-it is a binary operator.
-
Define a Scheme expression representing
the sentence (A ^ B) => (C v D).
B: Processing
- 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?
- Similarly, extract the symbols from your disjunction in A.4.
-
(define disjunction-symbols (get-symbols _______))
Are the results sensible?
- Use list-union (also from logic.scm) to merge these
two lists of symbols. Does it produce a result you expect?
- 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
The routine PL-TRUE? is tasked with determining whether a sentence
holds for a given model. How can we make such a determination? First
we must figure out which of the seven kinds of sentences we have.
Then, we must also remember that a model is defined as an association
list, with symbols as the keys (cars) and boolean assignments
as the values (cdrs).
In these exercises, you'll begin building the pieces of an implementation
for (pl-true? sentence model).
- The simplest kind of atomic sentence is a boolean value. Write a Scheme
expression to determine whether sentence is a boolean.
- The next simplest atomic sentence is a positive literal representing
a symbol. Write a Scheme expression to determine whether sentence
is of this form.
- 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.
Note: Check the Scheme reference for details on using association
lists if you've forgotten.
- Write a Scheme expression (you may use let to bind values
for clarity) to determine whether sentence is a negation.
- Recall that you're assembling pieces for the procedure pl-true?,
which will have a recursive structure matching the definition of the
propositional sentence grammar given in the assignment. Write a "recursive"
call to pl-true? to determine whether the given sentence,
already 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 now begin using Scheme's built-in logical
operators.
- Write a Scheme expression (you may use let to bind values
for clarity) to determine whether sentence is a conjunction.
- Use 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.
D: Propositional inference
As you will learn, the Queen of Hearts is having quite a time trying
to bake tarts.
Here is some more salt, so now you can make the tarts,
said the King.
Can't, said the Queen. Somebody
stole my baking pan.
Baking pan! shouted the King. Well,
of course we'll have to get that back!
This time the search was narrowed down to the Frog-Footman, the Fish-Footman,
and the Knave of Hearts. They made the following statements at the
trial:
FROG-FOOTMAN: It was stolen by the Fish-Footman.
FISH-FOOTMAN: Your Majesty, I never stole it!
KNAVE OF HEARTS: I stole it!
A fine help you are! shouted
the King to the Knave. You usually lie through your
teeth!
Well, as it happened, at most one of them lied.1
- Using the symbols Frog-Lied, Fish-Lied, Knave-Lied,
define a Scheme expression of propositional logic called one-lied
representing the information that at most one of them lied.
- Adding the symbol Fish-Stole, define frog-statement
to represent the Frog-Footman's testimony in propositional logic
- Define fish-statement to represent the Fish-Footman's retort.
- Adding the symbol Knave-Stole, define knave-statement
to represent the Knave of Hearts's assertion.
- Combine one-lied and the three statements into a single knowledge
base called queens-pan-kb.
- After you complete tt-entails? in the homework, you will
be able to use it on on queens-pan-kb to determine who stole
the pan. In the meantime, you can use
-
(require "weinman-enumeration.scm")
to load a complete, pre-compiled version of tt-entails? to
use.
Lab Assignment
Between this lab and snippets in the assignment document, you now
have nearly all the pieces necessary to implement your own enumeration
model.
Open enumeration.scm (which you copied in the preparation),
study the documentation, and begin to implement the lab's assignment.
Copyright © 2011, 2013 Jerod
Weinman.
This work is licensed under a Creative
Commons Attribution-Noncommercial-Share Alike 3.0 United States License.
Footnotes:
1From R. Smullyan, "The Sixth Tale", Alice in Puzzle-Land,
Penguin Books (1982), pp. 13-14.