# 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
• Check the semantics (types) of the problem (using SystemB4TPTP)
• Yes - move on to check the consistency of the axioms

• Check the consistency of the axioms (using SystemOnTPTP)
• Establish that the axioms are satisfiable
• Yes - move on to establish logical consequence
• 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
• Unknown - prove it's not a theorem
• Prove it's not a theorem
• No - move on to processing the proof

• 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