The SZS ontologies (named after the authors of the original paper describing the success ontology [SZS03, SZS04, Sut08] provide status values to describe logical data. The SZS Success ontology provides status values to describe what is known or has been successfully established about the relationship between the axioms and conjectures in logical data. The SZS NoSuccess ontology provides status values to describe why a Success Ontology value has not been established. The SZS DataForm ontology provides status values to describe the nature of logical data. All status values are expressed as OneWord to make system output parsing simple, and also have a three letter mnemonic. In the figures many of the "OneWord" status values are abbreviated - see the lists below the figures for the official full "OneWord"s. The lines in the ontologies can be followed up the hierarchy as "isa" links, e.g., an EquivalentTheorem (ETH) isa Equivalent (EQV) isa Satisfiable (SAT) and isa SatisfiableAxiomsTheorem (STH).
The BNF of the ontologies is the ground truth.
The ontologies are very fine grained ontology, which have more status values and dataforms than are commonly used by ATP systems. Suitable subsets for practical purposes are as follows:
For SemanticSuccess
For problems with conjectures - report Theorem or ContradictoryAxioms or CounterSatisfiable
For problems without conjectures - report Satisfiable or Unsatisfiable
For NoSuccess
System stopped due to CPU limit - report Timeout
System gave up due to incompleteness - report GaveUp
System stopped due to an error - report Error
For DataForms
A generic proof - report Proof
A CNF refutation - report CNFRefutation
A generic model - report Model
A finite model - report FiniteModel
An infinite model - report InfiniteModel
A saturation - report Saturation
Success ontology values are also used in TPTP format proofs to record the relationship between the parents and inferred formula of each inference step. Commonly used values are:
The inferred formula is a theorem of the parents (logical consequences, e.g., resolvants, etc.) - report Theorem
The inferred and parent formulae are equisatisfiable (e.g., Skolemization) - report EquiSatisfiable
The negation of the inferred formula is a theorem of the parents (e.g., negating the conjecture in a proof by refutation) - report CounterTheorem
The solution status should be reported exactly once, in a line starting "% SZS status" (the leading '%' makes the line into a TPTP language comment). For examples:
% SZS status Unsatisfiable for SYN075+1
% SZS status GaveUp for SYN075+1
A Success or NoSuccess ontology value should be presented as early as possible, at least before any data (proof/model/whatever) is output to justify the value. The justifying DataForm should be reported exactly once, delimited by lines starting "% SZS output start" and "% SZS output end". For example:
% SZS output start CNFRefutation for SYN075-1
... in this case a CNF refutation goes here ...
% SZS output end CNFRefutation for SYN075-1
All "% SZS" lines can optionally have software specific information appended, separated by a :. For examples:
% SZS status GaveUp for SYN075+1 : Could not complete CNF conversion
% SZS output end CNFRefutation for SYN075-1 : Completed in CNF conversion
If you would like to cite the SZS ontologies, please use:
@InProceedings{Sut08-KEAPPA,
Author = "Sutcliffe, G.",
Year = "2008",
Title = "{The SZS Ontologies for Automated Reasoning Software}",
Editor = "Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev, B. and Schulz, S.",
BookTitle = "{Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and
Proof Assistants, and the 7th International Workshop on the Implementation of
Logics}",
Place = "Doha, Qatar",
Series = "CEUR Workshop Proceedings",
Number = "418",
Pages = "38-49"
}