Lab: Propositional Inference and First-order Logic

CSC261 - Artificial Intelligence - Weinman

Summary:

We use your enumeration algorithm to identify a thief and check our work with a resolution-based proof.

Preparation

1. Go to the directory containing your enumeration algorithm from the previous lab assignment.

   cd somewhere/propositional
2. Open your Scheme environment and create a new Scheme file called plinference.scm in your new directory.
3. Load your inference algorithm by adding

   (load "enumeration.scm")

   to the top of your new Scheme file.

Exercises

A: Propositional inference

"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.
2. Adding the symbol Fish-Stole, define frog-statement to represent the Frog-Footman's testimony in propositional logic
3. Define fish-statement to represent the Fish-Footman's retort.
4. Adding the symbol Knave-Stole, define knave-statement to represent the Knave of Hearts's assertion.
5. Combine one-lied and the three statments into a single knowledge base called queens-pan-kb.
6. Use tt-entails? on queens-pan-kb to determine who stole the pan.

B: CNF and resolution

1. Using pen and paper, rewrite one-lied and the three statements in CNF. Record the results of applying each of the four steps (biconditional elimination, implication elimination, literal negation, and disjunction distribution.
2. Use resolution to prove the conclusion you found in A.6.

C: First-order translation

1. Complete AIMA Exercise 18.28 (e)-(h).

Lab Assignment

Footnotes: