-------------------------------------------------------------------------------
The SZS Problem Status Ontology
-------------------------------

The output from 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. The SZS ontology provides a fine grained ontology of result and 
output forms that are used to specify what has been established about a given 
ATP problem.

The ontology assumes that the input is a 2-tuple 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. (The ontology also provides the interpretation
for the input as a single formula F, of the form Ax => C.) If the input is not 
of the form <Ax, C>, it is treated as a single conjecture formula (even if it 
is a "set of axioms" from the user view point, e.g., a set of clauses), and 
the 2-tuple is <TRUE, C>. In this case not all statuses are appropriate. 

Commonly Used Ontology Values
-----------------------------
This is a very fine grained ontology, which has more status values and
output forms than are commonly used by ATP systems. A suitable subset for 
practical purposes is as follows:
+ Status values for Success
  - FOF problems with a conjecture - report Theorem or CounterSatisfiable
  - FOF problems without a conjecture - report Satisfiable or Unsatisfiable
  - CNF problems - report Satisfiable or Unsatisfiable
+ Status values 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
  - Any other cases - report Unknown
+ Output forms
  - A generic proof - report Proof
  - A refutation - report Refutation
  - A CNF refutation - report CNFRefutation
  - A generic model - report Model
  - A finite model - report FiniteModel
  - An infinite mode - report InfiniteModel
  - A saturation - report Saturation

Standard Output of Ontology Values
----------------------------------
Solution status should be reported in a line starting "SZS status". For 
example:
    SZS status Unsatisfiable for SYN075+1
or:
    SZS status GaveUp for SYN075+1
The solution status should be reported as early as possible (before the 
solution output).

Solution output should be delimited by strings that specify the output form 
named in the SZS ontology, using lines starting "SZS output start" and 
"SZS output end". For example:
    SZS output start CNFRefutation for SYN075-1
      ...
    SZS output end CNFRefutation for SYN075-1

Lines my have a : to indicate the start of system/task specific
information. For example:
    SZS status GaveUp for SYN075+1 : Could not complete CNF conversion
or:
    SZS output end CNFRefutation for SYN075-1 : Completed in CNF conversion

-------------------------------------------------------------------------------
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
                                      |
                    ------------------+------------------
                  /                                       \
              Success                                  NoSuccess 
                 |                                         |
         --------+--------                         {NoSuccess Ontology}
       /                   \
  {Deductive          {Preserving
   Ontology}            Ontology}
            
-------------------------------------------------------------------------------
The Success Ontology
--------------------
                              {Deductive Ontology}
                                       |
              +----------+-------------+-------------+----------+
              |          |                           |          |
         Satisfiable  Theorem                     Counter    Counter
              |    \     |                        Theorem  Satisfiable
              |     \--->|<----- NoConclusion ------>|<---/     |
              |          |\                         /|          |
   +----------+----------+ +----------+ +----------+ +----------+----------+
   |          |          |            | |            |          |          |
 Weaker   Equivalent Tautologous  Contradictory  Unsat'ble   Counter    Weaker
Theorem      /:\     Conclusion      Axioms     Conclusion  Equivalent  Counter
            / : \   /    :          /  |   \         :    \   / : \     Theorem
  Equivalent  : Tautology: Satisfiable | Satisfiable :Unsat'ble :  Equivalent
     Theorem  :          :  Conclusion | Counter     :          :  Counter
              :          :   Contrad'y | Conclusion  :          :  Theorem
              :          :      Axioms | Contrad'y   :          :
              :          :             | Axioms      :          :
              :          :.           / \         ...:          :
              :            Tautologous   Unsat'ble              :
              :             Conclusion   Conclusion             :
              :          Contradictory   Contradictory          :
              :                 Axioms   Axioms                 :
              :.....................>:<..:                      :
                                     :..........................:


                              {Preserving Ontology}
                                       |
                         +-------------+-------------+
                         |                           |
             SatisfiabilityPreserving     CounterSatisfiabilityPreserving
                         |                           |
         SatisfiabilityPartialMapping     CounterSatisfiabilityPartialMapping
                         |                           |
                SatisfiabilityMapping     CounterSatisfiabilityMapping
                         |                           |
              SatisfiabilityBijection     CounterSatisfiabilityBijection

Success Statuses
----------------
+ Success (SUC)
  System successful.

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
  + 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 NoSuccess Ontology
----------------------

                          {NoSuccess Ontology}
                               ____|____
                              /    |    \
                          Open  Unknown  Assumed(UnknownStatus,SolvedStatus)
                   ________________|_____________________
                  /                                      \
              Stopped ______                           NotTested
            /          |    \                             |  \
       Error        Forced   GaveUp__________________     |   NotTestedYet
     /       \         |  \    |           |       | \    |   
OSError  InputError  User  ResourceOut  Incomplete | Inappropriate
           /    \             /    \             {Error}
       Syntax  Semantic  TimeOut  MemoryOut
       Error    Error     


No Success Statuses
----------------
+ NoSuccess (NOS)
  System not successful (yet)
+ 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 crashed gracelessly due to an error.
+ OSError (OSE)
  System crashed/gave up due to an operating system error.
+ InputError (INE)
  System crashed/gave up due to an input error.
+ SyntaxError (SYE)
  System crashed/gave up due to an input syntax error
+ SemanticError (SEE)
  System crashed/gave up due to an input semantic error
+ Forced (FOR)
  System was forced to stop by an external force.
+ User (USR)
  System was forced to stop by the user.
+ ResourceOut (RSO)
  System was forced to stop by the harness because some resource ran out.
+ Timeout (TMO)
  System stopped because the CPU time limit ran out.
+ MemoryOut (MMO)
  System stopped because the RAM limit ran out.
+ GaveUp (GUP)
  System gave up of its own accord.
+ Incomplete (INC)
  System 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
              ____________|____________               |
             /                         \        CNFRefutation
          Proof                       Model      (~FOF->CNF)
          __|__                   ______|______
         /     \                 /      |      \
 Derivation   Refutation     Finite  Infinite  Saturation
                  |          Model     Model
             CNFRefutation
                             
+ Solution (Sln)
  A solution
+ Proof (Prf)
  A proof
+ Derivation (Der)
  A derivation (proof ending in the theorem)
+ Refutation (Ref)
  A refutation (sarting at the problem formulae and ending in $false)
+ CNFRefutation (CRf)
  A refutation in clause normal form (a CNF refutation for a FOF problem,
  without the FOF to CNF translation, is only an Assurance)
+ 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
-------------------------------------------------------------------------------
