The SZS Success Ontology

Background

• Inspired by ontology used for MathWeb (Z)
• Logical data a ⟨Ax, C⟩ 2-tuple
  • If not, treated as ⟨TRUE, C⟩
• Relationships between models sets of Ax and C

The Ontology

• The Models
• The Meanings

Commonly Useful Values

• FOF with conjecture: Theorem or CounterSatisfiable
• FOF without conjecture: Satisfiable or Unsatisfiable
• CNF: Satisfiable or Unsatisfiable