The ontology has recently been extended to include status values for problems that are unsolved, and to include a more comprehensive set of values describing the output from an ATP system. The latest version is given at the end of this document.
SZS status Unsatisfiable for SYN075+1or:
SZS status GaveUp for SYN075+1
SZS output start CNFRefutation for SYN075-1 ... SZS output end CNFRefutation for SYN075-1
-------------------------------------------------------------------------------
The SZS Problem Status Ontology
-------------------------------
The output from current ATP systems varies widely in quantity, quality, and
meaning. At the low end of the scale, systems that search for a refutation of
a set of clauses may output only an assurance that a refutation exists (the
wonderful "yes" output). At the high end of the scale a system may output a
natural deduction proof of a problem expressed in FOF. In some cases the
output is misleading, e.g., when a CNF based system claims that a FOF input
problem is "unsatisfiable" it typically means that the negated CNF of the
problem is unsatisfiable.
In order to use ATP systems' results, e.g., as input to other tools, it is
necessary that the ATP systems correctly and precisely specify what has been
established. To this end the SZS problem status ontology has been established.
The ontology was based on initial work done to establish communication
protocols for systems on the MathWeb Software Bus. The ontology is shown
below.
The ontology assumes that the input F is of the form Ax => C, where Ax is a
set (conjunction) of axioms and C is a single conjecture formula. This is a
common standard usage of ATP systems.
+ The status value indicates the relationship between Ax and C.
+ By showing that F is valid, an ATP system shows that C is a theorem (a
logical consequence) of Ax, i.e., Ax |= C, where |= is the standard first
order entailment.
+ If F is not valid, there are several other possible relationships between Ax
and C, as shown in the ontology.
If F is not of the form Ax => C, it is treated as a single monolithic
conjecture formula (even if it is an "axiom" or "set of axioms" from the user
view point). This is equivalent to Ax being TRUE. In this case not all of the
statuses are appropriate, and those that are possible are marked with a * in
the ontology.
+ Systems that report Theorem for a monolithic formula must have established
Tautology.
+ A set of axioms is treated as a conjecture formed from the conjunction of the
formulae.
+ This is the scenario for a set of clauses.
-------------------------------------------------------------------------------
The Ontology
------------
The solid lines can be followed up the hierarchy as isa links, e.g., an
ETH isa EQV isa (SAT anda THM). The dotted lines can be followed only
once, e.g., a UCA isa UNC, but not a CSA (although UCS isa CAX isa CTH).
The >X< means the >< line tunnels under the X line.
All status values are expressed as "OneWord" to make system output parsing
simple, and also have a three letter code. Associated with each possible
status are the possible outputs from the ATP system. See the explanations
below to expand the three letter status acronyms to the full meaningful
status.
Problem Status
|
------------------+------------------
/ \
Solved Unsolved
| |
--------+-------- {Unsolved Ontology}
/ \
{Deductive {Preserving
Ontology} Ontology}
-------------------------------------------------------------------------------
The Solved Ontology
-------------------
{Deductive {Preserving
Ontology} Ontology}
| |
+-----+--------+--------+-----+ +-----+-----+
| | | | | |
SAT THM CTH CSA SAP CSP
| \-->|<------NOC------>|<--/ | | |
| |\ /| | SAR CSR
+-----+-----+ +-----+ +-----+ +-----+-----+ | |
| | | | | | | | SAM CSM
WTH EQV TAC __CAX__ UNC CEQ WCT | |
/ : \ / :. / / \ \ .: \ / : \ SAB CSB
ETH : TAU TCA SCA SCC UCA UNS : ECT
:.......>:<..........: :
:....................:
Solved Statuses
---------------
+ Solved (SOL)
Solved by a system.
Deductive Statuses
------------------
+ Satisfiable (SAT)
Some interpretations are models of Ax
Some models of Ax are models of C
+ Shows: F is satisfiable; ~F is not valid; C is not a theorem of Ax
+ Output: Model or saturation of Ax and C
+ Theorem (THM)
All models of Ax are models of C
+ Shows: F is valid; C is a theorem of Ax
+ Output: Proof of C from Ax; Refutation of Ax U {~C}
+ Equivalent (EQV)
All models of Ax are models of C
All models of C are models of Ax
+ Shows: F is valid; C is a theorem of Ax; Ax is a theorem of C
+ Output: Proof of C from Ax and proof of Ax from C; Refutation of
Ax U {~C} and refutation of ~Ax U {C}
+ WeakerTheorem (WTH)
Some, but not all, interpretations are models of Ax
All models of Ax are models of C
Some models of C are not models of Ax
+ See THM
+ TautologousConclusion (TAC)
Some, but not all, interpretations are models of Ax
All interpretations are models of C
+ Shows: F is valid; C is a tautology
+ Output: Proof of C; Refutation of ~C
+ EquivalentTheorem (ETH)
Some, but not all, interpretations are models of Ax
All models of Ax are models of C
All models of C are models of Ax
+ See EQV
+ Tautology (TAU)
All interpretations are models of Ax
All interpretations are models of C
+ Shows: F is valid; ~F is unsatisfiable; C is a tautology
+ Output: Proof of C and proof of Ax; Refutation of ~C and refutation of ~Ax
+ ContradictoryAxioms (CAX)
No interpretations are models of Ax
+ Shows: F is valid; Anything is a theorem of Ax
+ Output: Refutation of Ax
+ SatisfiableConclusionContradictoryAxioms (SCA)
No interpretations are models of Ax
Some interpretations are models of C
+ See CAX
+ TautologousConclusionContradictoryAxioms (TCA)
No interpretations are models of Ax
All interpretations are models of C
+ See TAC and CAX
+ CounterSatisfiable (CSA)
Some interpretations are models of Ax
Some models of Ax are models of ~C
+ Shows: F is not valid; ~F is satisfiable; C is not a theorem of Ax
+ Output: Model or saturation of Ax and ~C
+ CounterTheorem (CTH)
All models of Ax are models of ~C
+ Shows: F is invalid; ~F is valid; ~C is a theorem of Ax; C cannot be
made into a theorem of Ax by extending Ax
+ Output: Proof of ~C from Ax; Refutation of Ax U {C}
+ CounterEquivalent (CEQ)
All models of Ax are models of ~C
All models of C are models of Ax
+ Shows: F is not valid; ~C is a theorem of Ax; All interpretations are
models of Ax xor models of C
+ Output: Proof of ~C from Ax and proof of Ax from ~C; Refutation of
Ax U {C} and refutation of ~Ax U {~C}
+ WeakerCounterTheorem (WCT)
Some, but not all, interpretations are models of Ax
All models of Ax are models of ~C
Some models of ~C are not models of Ax
+ See CSA
+ UnsatisfiableConclusion (UNC)
Some, but not all, interpretations are models of Ax
All interpretations are models of ~C
(No interpretations are models of C)
+ Shows: ~C is a tautology
+ Output: Proof of ~C; Refutation of C
+ EquivalentCounterTheorem (ECT)
Some, but not all, interpretations are models of Ax
All models of Ax are models of ~C
All models of ~C are models of Ax
+ See CEQ
+ Unsatisfiable (UNS)
All interpretations are models of Ax
All interpretations are models of ~C
(No interpretations are models of C)
+ Shows: F is unsatisfiable; ~F is valid; ~C is a tautology
+ Output: Refutation of F; Proof of ~F
+ SatisfiableCounterConclusionContradictoryAxioms (SCC)
No interpretations are models of Ax
Some interpretations are models of ~C
Some interpretations are models of C
+ See CAX
+ UnsatisfiableConclusionContradictoryAxioms (UCA)
No interpretations are models of Ax
All interpretations are models of ~C
(No interpretations are models of C)
+ See UNC and CAX
+ NoConsequence (NOC)
Some interpretations are models of Ax
Some models of Ax are models of C
Some models of Ax are models of ~C
+ Shows: F is not valid; F is satisfiable; ~F is not valid; ~F is
satisfiable; C is not a theorem of Ax
+ Output: Pair of models or saturations, one of Ax and C, one of Ax and ~C
Preserving Statuses
-------------------
+ SatisfiabilityBijection (SAB)
There is a bijection between the models of Ax (and there are some) and models
of C
+ Shows: F is satisfiable
+ Output:
+ Example: Skolemization, psuedo-splitting
+ SatisfiabilityMapping (SAM)
There is a mapping from the models of Ax (and there are some) to models of C
+ Shows: F is satisfiable
+ Output:
+ SatisfiabilityPartialMapping (SAR)
There is a partial mapping from the models of Ax (and there are some) to
models of C
+ Shows: Nothing about F
+ Output: Pairs of models or saturations
+ Example: Ax = {p | q}, C = p & r
+ SatisfiabilityPreserving (SAP)
If there exists a model of Ax then there exists a model of C
+ Shows: F is satisfiable
+ Output:
+ CounterSatisfiabilityPreserving (CSP)
If there exists a model of Ax then there exists a model of ~C
+ Shows: Nothing about F
+ Output:
+ CounterSatisfiabilityPartialMapping (CSR)
There is a partial mapping from the models of Ax (and there are some) to
models of ~C
+ Shows: Nothing about F
+ Output: Pairs of models
+ CounterSatisfiabilityMapping (CSM)
There is a mapping from the models of Ax (and there are some) to models of ~C
+ Shows: Nothing about F
+ Output:
+ CounterSatisfiabilityBijection (CSB)
There is a bijection between the models of Ax (and there are some) and models
of ~C
+ Shows: Nothing about F
+ Output:
-------------------------------------------------------------------------------
The Unsolved Ontology
--------------------
{Unsolved Ontology}
____|____
/ | \
Open Unknown Assumed(UnknownStatus,SolvedStatus)
________________|_______________
/ \
Stopped NotTested
/ | \ | \
Error Forced GaveUp___________________ | NotTestedYet
| | \ | | | \ |
InputError/ User ResourceOut Incomplete | Inappropriate
OSError | {Error}
TimeOut/
MemoryOut
Unsolved Statuses
-----------------
+ Unsolved (USD)
Not solved by a system.
+ Open (OPN)
Not solved at all
+ Unknown (UNK)
Not solved by a system, and no assumption made about the status.
+ Assumed (ASS)
System assumes that the problem has the SolvedStatus. The actual status
in unknown for the UnknownStatus reason.
+ Stopped (STP)
System attempted the problem, and stopped without a solved status.
+ Error (ERR)
System attempted the problem and crashed gracelessly due to an error.
+ InputError (INE)
System attempted the problem and crashed due to an input error.
+ OSError (OSE)
System attempted the problem and crashed due to an operating system error.
+ Forced (FOR)
System attempted the problem and was forced to stop by an external force.
+ User (USR)
System attempted the problem and was forced to stop by the user.
+ ResourceOut (RSO)
System attempted the problem and was forced to stop by the harness because
some resource ran out.
+ Timeout (TMO)
System attempted the problem and stopped because the CPU time limit ran out.
+ MemoryOut (MMO)
System attempted the problem and stopped because the RAM limit ran out.
+ GaveUp (GUP)
System attempted the problem and gave up of its own accord.
+ Incomplete (INC)
System attempted the problem and gave up of its own accord because it's
incomplete.
+ Inappropriate (IAP)
System cannot attempt this type of problem, in principle
+ NotTested (NTT)
System has not attempted the problem.
+ NotTestedYet (NTY)
System has not attempted the problem but might in the future.
-------------------------------------------------------------------------------
The Output Ontology
-------------------
Output Status
|_________________
| | \
Solution Assurance None
_______|_______
/ \
Derivation Model
__|__ ___|______
/ \ / | \
Proof Refutation Finite Infinite Saturation
| Model Model
CNFRefutation
+ Solution (Sln)
A solution
+ Derivation (Der)
A derivation
+ Proof (Prf)
A proof (derivation ending in the theorem)
+ Refutation (Ref)
A refutation (ending in $false)
+ CNFRefutation (CRf)
A refutation in clause normal form
+ Model (Mod)
A model
+ FiniteModel (FMo)
A model with a finite domain
+ InfiniteModel (IMo)
A model with an infinite domain
+ Saturation (Sat)
A saturating set of clauses
+ Assurance (Ass)
Only an assurance
+ None (Non)
Nothing
-------------------------------------------------------------------------------