Deductive Statuses

Theorem

• Every model of Ax is a model of C
  • Proof of C from Ax,
  • Refutation of Ax U {~C} or CNF(Ax U {~C})
• Common use: FOF theorems

Satisfiable

• Some models of Ax are models of C
  • Model
  • Saturation
• Common use: Satisfiable sets of FOF axioms, satisfiable sets of CNF

CounterSatisfiable

• Some models of Ax are models of ~C
  • Model
  • Saturation
• FOF non-theorems

Unsatisfiable

• Every interpretation is a model of Ax and ~C
  • Proof of ~F,
  • Refutation of F
• Unsatisfiable sets of CNF

ContradictoryAxioms

• No models of Ax
  • Refutation of Ax
• Common use: Contradictory axioms in a FOF problem