CS 291 Exam Two Terms and Concepts

Hein Section 7.1 First-Order Predicate Calculus

• Understand predicates, existential quantifiers and universal quantifiers over a domain.
• Know what a well-formed formula (wff) is and all the standard terminology associated with this idea.
• Be familiar with scope of quantified variables and how to distinguish bound from free variables.
• Know the concepts of valid, unsatisfiable and satisfiable as applied to wffs.

Hein Section 7.2 Equivalent Formulas

• Be familiar with the concept of logical equivalence.
• Be able to do various manipulations to show that one logical form is equivalent to another logical form.
• Know about prenex normal form and how to to through the steps to put a wff into this form.
• Beyond this, be able to put wffs into disjunctive normal form and conjunctive normal form.
• Be able to formalize English sentences into wffs and find natural sounding English sentences that are equivalent to wffs.

Hein Section 7.3 Formal Proofs in Predicate Calculus

• Know how to do formal conditional proofs in FOL using natural deduction.
• Be familiar with universal instantiation (UI), existential generalization (EG), existential instantiation (EI), and universal generalization (UG).
• Be able to take English sentences, translate them into formal wffs and go through the process of doing a formal proof.

Hein Section 7.4 Equality

• There are various proofs in this section that I won't expect you do do much with.
• You should know the Equal for Equals (EE) rule well enough to use it in proofs.
• You should extend your ability to formalize English sentences in FOL to include aspects of equality, as in the homework problems.

Hein Section 8.1 Program Correctness

• You should understand the {P} S {Q} syntax used in program correctness proofs.
• Know the Assignment Axiom and the Consequence Rules and how to use them in proofs.
• Be familiar with the Composition Rule and the If-Then Rule and If-Then-Else Rule and how to use them in proofs. If I expected you to use any of these three rules in proofs, I would give them to you on the exam.
• I do not expect you to be able to do correctness proofs with the While Rule or any of the array assignment stuff or program termination proofs.

Hein Section 8.2 Higher-Order Logics

• Nothing from this section.

Hein Section 8.3 Automatic Reasoning

• I expect you to be able to take logical wffs and put them in clausal form, including Skolemization as necessary. This includes being able to carefully apply Skolem's Rule.
• You should be able to do resolution proofs, both with propositional logic clauses and first-order logic clauses.
• Understand substitution and unification and how they are used in resolution proofs.
• Be able to use Robinson's Unification Algorithm to find most general unifiers (mgus).
• To restate, be able to do full blown first-order logic resolution proofs from beginning to end.