1. Vocabulary: understand the definition of the following terms:
2. Given a small set of FOL axioms that involve a single function symbol s (think of "successor"), a predicate L (think of "less than"), and axioms that assert facts such as:
be able to determine if the theory has only finite models, both finite and infinite models, or only infinite models.
3. Be able to represent the following kinds of terminological facts:
4. Be able to convert a relation that uses 3 or more arguments to a set of relations that only have two arguments by using abstract individuals.
5. Be able to state what makes a proof theory correct or complete according to a given model theory.
6. Be able to convert general propositional and FOL formulas into CNF. Be able to use Skolem functions as necessary.
7. Be able to resolve two FOL clauses, handling unification properly.
8. Be able to create small propositional and FOL resolution refutation proofs, including FOL with answer extraction, by hand.
9. Be able to name and briefly describe the theorem that allows FOL reasoning to be reduced to propositional reasoning (perhaps over an infinite theory), and explain why this theorem shows that resolution is complete.
10. Know the complexity (decidable, undecidable, semi-decidable, NP-complete, co-NP-complete, solvable in polynomial time) for the following problems:
11. Be able to state which SAT algorithm we've discussed uses the following, and why it is useful:
12. Be able to translate a STRIPS planning operator into clause schemas, using the conventions described in class on 10/19.