The ATP Process

Specify the problem - the axioms and the conjecture
- Write the problem's axioms and conjecture in the domain language
- Write the problem in a logic
- Write the problem in a machine readable syntax (using a TPTP language).
- Check the syntax of the problem (using SystemB4TPTP)
  - Yes - move on to check the semantics of the problem
  - No - return to creating the machine readable file
- Check the semantics (types) of the problem (using SystemB4TPTP)
  - Yes - move on to check the consistency of the axioms
  - No - return to creating the machine readable file
Check the consistency of the axioms (using SystemOnTPTP)
- Establish that the axioms are satisfiable
  - Yes - move on to establish logical consequence
  - No - examine model/saturation, return to specify the problem
  - Unknown - establish that the axioms are unsatisfiable
- Establish that the axioms are unsatisfiable
  - Yes - examine the refutation (using IDV), return to specify the problem
  - No - move on to establish logical consequence
  - Unknown - move on to establish logical consequence (and worry)
Establish logical consequence (using SystemOnTPTP)
- Prove the theorem
  - Yes - move on to process the proof
  - No - return to specify the problem
  - Unknown - prove it's not a theorem
- Prove it's not a theorem
  - Yes - return to specify the problem
  - No - move on to processing the proof
  - Unknown - return to specify the problem
Process the proof
- Are the axioms are known to be SAT?
  - Yes - verify the proof
  - No - check if the conjecture is used in proof
  - If the axioms used in the proof are a subset of all the axioms, could check for their consistency.
- Check if the conjecture is used in proof
  - Yes - assume the axioms are OK, verify the proof
  - No - return to specify the problem
  - Unknown - ask if the ATP system is trusted
- Verify the proof (using GDV)
  - Yes - happiness
  - No - return to establish logical consequence with a different ATP system
  - Unknown - ask if the ATP system is trusted
- Is the ATP system trusted?
  - Yes - happiness
  - No - return to specify the problem
  - Unknown - confusion, return to specify the problem
Examples for the ATP Process