Multiple Answer Extraction with ATP

Questions and Answers

• Conjecture with outermost existentially quantified answer variables, e.g. ...
• Multiple proofs ... multiple answers (possibly)
• ATP support ... Otter, SNARK, Vampire-SUMO, ... ?
• TPTP standards for questions and answers

Basic Multiple Answer Extraction

• Single answers from ATP or TPTP Proof+OAESys
• Deny previous answers and repeat
  • Inequalities, e.g. ...
  • Incrementally axiomatize "looks different", e.g. ...
• Checking there are no more answers
• Inequality vs. "looks different" vs. multiple proofs

Optimistic Multiple Answer Extraction

• Not enough inequality information, e.g., UNA assumption
• Use "looks different" followed by equality reasoning
  Unequal Equal Not equal Not unequal Unknown, e.g. ...