Due: Wednesday May 6, 1998
Overview
In this assignment, you are asked to encode two problems in First-Order Predicate Logic (FOPL) using Situation Calculus, and then, for each problem, generate a proof using the automatic theorem prover called OTTER. Both of the problems address a simplified version of the Wumpus World. In this simplified Wumpus World, there are only three squares arranged in a linear sequence; the gold is located in the middle square. In the first problem, the agent is limited to two actions, goForward and grab, and his goal is to move from the starting square to the finish square picking up the gold on the way. In the second problem, in addition to picking up the gold, the agent to also expected to shoot a wumpus that is positioned in the middle square. For both problems, your assignment is to prove that the agent can achieve his goal. This will entail representing the problem (i.e., building a knowledge base) and the agent's goal in FOPL and then using OTTER to prove that the agent can reach the desired goal (i.e., showing that the goal can be inferred from the knowledge base). To help you get started, there is a representation of the simplified world in which the agent's only action is goForward (the gold is not included in this world). This example is worked using FOPL symbols that are recognized by OTTER. For this example, you are given both the OTTER input file and the OTTER output file.
The example, the definitions of the problems that you need to solve, the executable version of OTTER, and the user's manual for OTTER are included in the project3 subdirectory of the public directory for this class (i.e., /usr/local/csci/373). Also included in the project3 directory is a subdirectory called examples are other OTTER input files that show the encoding of several problems that do not involve the use of Situation Calculus. In the sections below, each aspect of this assignment is described in more detail.
OTTER
OTTER (Organized Techniques for Theorem-proving and Effective Research) is one of the better known automatic reasoning programs. It is a resolution style theorem prover and it is discussed briefly in chapter 10 of your class text. In addition to the material in your class text, you have access to the OTTER user's manual in the project3 directory described above. If you request it, I can also give you a handout on OTTER entitled ``A Tutorial on the Use of OTTER'' and. This is far more information than you need just to do this assignment.
In order to do this assignment you need to know how to write statements in first-order predicate logic using OTTER's syntax (e.g., how to represent the universal quantifier in OTTER's syntax). This information is provided in the user's manual for OTTER. OTTER accepts as input either statements in clause form or full first-order logic formulae. First-order logic formulae are translated to clause form (automatically by OTTER) before theorem proving begins. All of the examples in the examples subdirectory show only clause form input. Be aware that the list of usable clauses is designated ``list(usable).'' while the list of usable formulae is designated ``formula_list(usable).'' You also need to know how to run OTTER on your input and retrieve its output. There are several options but the basic mode is:
otter < input-file > output-file
The final thing that you need to know regarding OTTER is how to select a proof strategy. OTTER is very powerful in that it offers a wide range of resolution proof strategies and you can read about these in the handout entitled, ``A Tutorial on the Use of OTTER'' as well as in the user's manual. Both of the problems that you have been assigned can be solved using OTTER's autonomous mode. In this mode, OTTER automatically selects the strategy to be used in developing the proof. The Wumpus World example that you are given, and the file animals.in in the examples subdirectory both demonstrate how to specify the autonomous mode in an OTTER input file. The other files in the examples subdirectory designate other proof strategies. All files in the examples subdirectory are OTTER input files.
Your Assignment
You are asked to work two problems in this assignment. The problems are fully specified in the files problem1.desc and problem2.desc in the project3 directory described above. For each problem, you should hand in the input file that you submit to OTTER and the output file that OTTER generates. The output file should contain a proof showing that the agent can reach his goal. Both proofs should be proof by contradiction. The input file should be adequately commented. There is no single right answer to each of these problems, and all correct encodings and proofs will be considered equally acceptable.