Prototype Choices

• Positive ground facts (ground atoms)
  • Database is necessarily consistent
  • Plan for consistency with internal axioms

• Stored in an SQL database
  • Sound retrieval
  • No uncertainty or imprecision

• Interfaces to external data
  • TPTP format for indicating external data
  • TPTP Q&A standards for questions and answers
  • SZS standards (may need to be extended) for status information
  • Local process access

• Search-time retrieval
  • Synchronous and asynchronous with ATP saturation loop
  • Pull based on negative selected literal
  • Batch retrieval with number limit
  • No uniqueness requirements

• Retention of external data
  • All retrieved data stored persistently (modulo ATP simplification)