Validation of the SZS Success Ontology

Background

• First step was model set relationships
• Second step was logical analysis
  • Inspired by reviewer ... "I think it inevitable that an evolving ontology would have some inconsistencies"
  • Axiomatize the ⟨Ax, C⟩ model set relationships in FOL
  • Prove ontology consistency and properties

The Logical Analysis

• The Axiomatization
• The Results

The ATP Technology

• Monolithic ATP systems (tried lots!) typically timed out or gave up
• SRASS very effective, using iProver and EP
• MANSEX used to find obvious relationships between values
• IDV used to analyse refutations