Solutions

Required Properties of Proofs

• Derivations must be complete
  • Start at formulae from the problem
  • End at the conjecture or false
• Translations must be documented.
• Only relevant inference steps.
• Inference steps must document
  • Parent formulae
  • Inference rule used
  • Inferred formula.
• Inference steps reasonably fine-grained.
• Unsatisfiable set of ground instances of clauses is acceptable

Required Properties of Models

• Models must be complete
  • Domain
  • Function map
  • Predicate maps
• Explicit ground lists or clear, terminating algorithm