[ Home ] --- [ Syllabus ] --- [ Project 1] 6.825 - Techniques in Artificial Intelligence, Fall '06

# Project 1b: FAQ

## Questions and hints

• Cat example: axioms here
• I get errors when I run FOLTester on the file equip1.txt from part b.
The resolution-refutation proof checker for part b and the model-checking code for part a expect input files in slightly different formats. The parser in part a expects one logical sentence, which is why you have to put a conjunction after every axiom. For example, the file equip1.txt is to be used with part b of project 1, not part a. The part a parser concludes that since there is no operator at the end of the first line, there is nothing more to parse, so it will just give an assignment for the first sentence.

• What do I need to include in the proof sketches?
We're looking for an English description of how you proved what you were trying to prove. In other words, something that will show you did not arrive at your conclusion by trying resolution steps at random. You should comment on the proof in general and then comment on each few steps of the proof. Here's an example of the sort of thing we're looking for:
I'm going to show that the chicken came before the egg by showing that there exist no eggs that did not come from a chicken and then showing that every chicken lays at least one egg.
...
Here, we establish that there exists a chicken such that there is an egg inside the chicken.
...
Now, the result of the laying of an egg, etc.

• The movement dynamics "On" axiom of equip2.txt uses a biconditional but the movement dynamics in equip1.txt uses an implication. Is this intentional?
Yes, this is intentional. You can think of the movement dynamics in task 5 of On(a,w2,S2) as expressing that "a" could be on "w2" in S2. The biconditional is necessary in at least 1 possible proof solution for task 5.

## Other good stuff

• Dan Roy wrote a perl script that converts the output of RRPC "Output Proof" into a latex table, which makes the proofs look pretty. The links for the script and the instructions are below. Make sure the script doesn't get converted to DOS when you download, because DOS-style carriage returns will break it. Thanks, Dan!

The script: http://web.mit.edu/droy/www/other/proof2latex
Instructions: here.