I get errors when I run FOLTester on the file equip1.txt from
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
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!