## Midterm Review - CS 244/444

1. Vocabulary: understand the definition of the following terms:

- interpretation
- denotation
- variable assignment
- model
- satisfaction
- logical consequence
- unsatisfiable
- valid

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:

- L is transitive
- L has a least element
- The successor of different entities are different
- L is a total order

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:

- Disjointedness
- Subtypes
- Exhaustiveness
- Symmetry
- Inverses
- Type restrictions
- Full definitions

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:

- Does a statement follow from a FOL theory?
- Is a set of propositional clauses unsatisfiable?
- Is a set of propositional clauses satisfiable?
- Is a set of propositional clauses each of length 2 satisfiable?

11. Be able to state which SAT algorithm we've discussed uses the following, and why it is useful:

- Pure literal rule
- Noisy moves
- Unit propagation
- Branching heuristic

12. Be able to translate a STRIPS planning operator into clause schemas, using the conventions described in class on 10/19.