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 a 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

                                  System
                                  Status
                                     |
                   ------------------+------------------
                 /                                       \
             Success                                   Error
             Status                                    Status
                |
        --------+--------
      /                   \
 Unknown                 Known
 Formula                Formula
 Status                 Status
    |                      |
  Open             --------+--------
                 /                   \
            Deductive            Preserving
             Status                Status


                                 Deductive
                                  Status
                                     |
                   ------------------+------------------
                 /                                       \
            Satisfiable* ------------&-------------    Counter
                |                   No               Satisfiable*
                |               Consequence               |
                |                                         |
             Theorem ----------------&---------------- Counter
                |              Contradictory           Theorem
                |                 Axioms                  |
        --------+--------                         --------+--------
      /                   \                     /                   \  
 Tautologous          Equivalent             Counter           Unsatisfiable
 Conclusion                |                Equivalent          Conclusion 
      \                   /                     \                   /
        --------+--------                         --------+--------
                |                                         |
            Tautology*                              Unsatisfiable*



                                Preserving
                                  Status
                                     |
                   ------------------+------------------
                 /                                       \
          Satisfiability                         Counter Satisfiability
            Preserving                                Preserving 
                |                                         |
          Satisfiability                         Counter Satisfiability
          Partial Mapping                            Partial Mapping  
                |                                         |
          Satisfiability                         Counter Satisfiability
             Mapping                                   Mapping  
                |                                         |
          Satisfiability                         Counter Satisfiability
            Bijection                                 Bijection 

                                   Error 
                                   Status
                                     |
           --------------------------+--------------------------
          /               |                     |               \
    Input error        Gave up             Resource Out       Unknown
                          |                 /        \
                      (Reason)          Timeout    (Other)

All status values are expressed as "one word" 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.

Deductive Statuses

Tautology (TAU)
Every interpretation is a model of Ax and a model of C
- Shows
  - F is valid,
  - ~F is unsatisfiable,
  - C is a tautology
- Expected output
  - Assurance
  - Proof of F
  - Refutation of ~F
Tautologous Conclusion (TAC)
Every interpretation is a model of C
- Shows
  - F is valid,
  - C is a tautology
- Expected output
  - Assurance
  - Proof of C
  - Refutation of ~C
Equivalent (EQV)
Ax and C have the same models (and there are some)
- Shows
  - F is valid
  - C is a theorem of Ax
- Expected output
  - Assurance
  - Proof of C from Ax and proof of Ax from C
  - Refutation of Ax U {~C} and refutation of ~Ax U {C}
  - Refutation of CNF(Ax U {~C}) and refutation of CNF(~Ax U {C})
Theorem (THM)
Every model of Ax (and there are some) is a model of C
- Shows
  - F is valid
  - C is a theorem of Ax
- Expected output
  - Assurance
  - Proof of C from Ax
  - Refutation of Ax U {~C}
  - Refutation of CNF(Ax U {~C})
Satisfiable (SAT)
Some models of Ax (and there are some) are models of C
- Shows
  - F is satisfiable
  - ~F is not valid
  - C is not a theorem of Ax
- Expected output
  - Assurance
  - Model of Ax and C
  - Saturation
ContradictoryAxioms (CAX)
There are no models of Ax
- Shows
  - F is valid
  - Anything is a theorem of Ax
- Expected output
  - Assurance
  - Refutation of Ax
  - Refutation of CNF(Ax)
NoConsequence (NOC)
Some models of Ax (and there are some) are models of C, and some 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
- Expected output
  - Assurance
  - Pair of models, one of Ax and C, and one of Ax and ~C
  - Pair of saturations
CounterSatisfiable (CSA)
Some models of Ax (and there are some) are models of ~C
- Shows
  - F is not valid
  - ~F is satisfiable
  - C is not a theorem of Ax
- Expected output
  - Assurance
  - Model Ax and ~C
  - Saturation
CounterTheorem (CTH)
Every model of Ax (and there are some) is a model 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,
- Expected output
  - Assurance
  - Proof of ~C from Ax
  - Refutation of Ax U {C}
  - Refutation of CNF(Ax U {C})
CounterEquivalent (CEQ)
Ax and ~C have the same models (and there are some)
- Shows
  - F is not valid
  - ~C is a theorem of Ax
  - Every interpretation is a model of Ax xor a model of C
- Expected output
  - Assurance
  - Proof of ~C from Ax and proof of Ax from ~C
  - Refutation of Ax U {C} and refutation of ~Ax U {~C}
  - Refutation of CNF(Ax U {C}) and refutation of CNF(~Ax U {~C})
Unsatisfiable Conclusion (UNC)
Every interpretation is a model of ~C
- Shows
  - ~C is a tautology
- Expected output
  - Assurance
  - Proof of ~C
  - Refutation of C
Unsatisfiable (UNS)
Every interpretation is a model of Ax and a model of ~C
- Shows
  - F is unsatisfiable,
  - ~F is valid
  - ~C is a tautology
- Expected output
  - Assurance
  - Refutation of F
  - Proof of ~F

Preserving Statuses

SatisfiabilityBijection (SAB)
There is a bijection between the models of Ax (and there are some) and models of C
- Example: Skolemization, psuedo-splitting
- Shows
  - Nothing about F
- Expected output
  - Assurance
SatisfiabilityMapping (SAM)
There is a mapping from the models of Ax (and there are some) to models of C
- Shows
  - Nothing about F
- Expected output
  - Assurance
SatisfiabilityPartialMapping (SAR)
There is a partial mapping from the models of Ax (and there are some) to models of C
- Example: Ax = {p | q}, C = p & r
- Shows
  - Nothing about F
- Expected output
  - Assurance
  - Pairs of models
  - Pairs of saturations
SatisfiabilityPreserving (SAP)
If there exists a model of Ax then there exists a model of C
- Shows
  - Nothing about F
- Expected output
  - Assurance
CounterSatisfiabilityPreserving (CSP)
If there exists a model of Ax then there exists a model of ~C
- Shows
  - Nothing about F
- Expected output
  - Assurance
CounterSatisfiabilityPartialMapping (CSR)
There is a partial mapping from the models of Ax (and there are some) to models of ~C
- Shows
  - Nothing about F
- Expected output
  - Assurance
  - 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
- Expected output
  - Assurance
CounterSatisfiabilityBijection (CSB)
There is a bijection between the models of Ax (and there are some) and models of ~C
- Shows
  - Nothing about F
- Expected output
  - Assurance

Error Statuses

Timeout - System ran past user imposed CPU time limit
GaveUp - System gave up before the time limit
InputError - System exited due to an error in its input
ResourceOut - System exited due to running out of some non-time resource
Unknown - System exited before the time limit for unknown reason

Precise Output Forms

Output Value	TSTP Code
Assurance	`Ass`
Refutation	`Ref`
CNFRefutation	`CRf`
Proof	`Prf`
Model	`Mod`
Saturation	`Sat`