TSTP System States

Logical States

• F of the form Ax => C
  • F valid means C is a logical consequence of Ax
  • F not valid means ...
• Conservative states
  • Example: Satisfiable: Some models of Ax (and there are some) are models of C
• Extension states
  • Example: Satisfiability mapping: There is a mapping from the models of Ax (and there are some) to models of C
• The hierarchy

             _____________________________________________________
            /               |          |          |               \
     Satisfiability         |       Vacuous       |       Counter satisfiability
       preserving           |                     |            preserving
           |                |                     |                |
     Satisfiability    Satisfiable             Counter    Counter satisfiability
     partial mapping        |     \          satisfiable      partial mapping
           |                |      \   &   /      |                |
     Satisfiability      Theorem    Neither    Counter    Counter satisfiability
        mapping             |                  theorem          mapping
           |                |                     |                |
     Satisfiability    Tautologies          Unsatisfiable Counter satisfiability
       bijection                                               bijection
  

• Only a few used by current ATP

Failure States

• 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