System Design and Architecture
- External axioms are positive ground facts
- External axioms are consistent, certain, precise, non-temporal
- External axioms can be repeated
- Retrieval from external sources can be incomplete
- External sources are comparatively slow
- External axioms requested on demand
- External axioms delivered in batches
- External axioms requested and delivered asynchronously
- No constraints on external source technology
System Architecture
- Based on SPASS' classic given-clause architecture
- Problem specification includes external specifications
- Requests and deliveries are mediated
- External axioms requested based on chosen clause literals
- External axioms integrated into the "Usable" list
- External requests are never duplicated
- TPTP-based syntax and protocols