External Sources of Axioms in Automated Theorem Proving

摘要

In recent years there has been a growing demand for Automated Theorem Proving (ATP) in large theories, which often have more axioms than can be handled effectively as normal internal axioms. This work addresses the issues of accessing external sources of axioms from a first-order logic ATP system, and presents an implemented ATP system that retrieves external axioms asynchronously, on demand.