ATP's Use of External Axioms

Interface to External Axioms

• Specification of availablity
• Roles ... axiom, lemma, conjecture, ...
• Syntax and protocol for requests and delivery
• External manifestation

When to Retrieve External Axioms

• Advance is same as internal axioms
• Deduction-time requires integration
  • Synchronous or asynchronous
  • Pull or push

Criteria for Requesting External Axioms

• Based on conjecture, chosen clause, selected literal
• Based on formulae and search space of ATP system

Granularity for Delivering External Axioms

• One-at-a-time, batches
• Limitations on batches - number, uniqueness, order

Storage and Retention of External Axioms

• Where (esp. wrt internal axioms)
• Persistence