External Sources of Axioms in Automated Theorem Proving

Abstract. 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.

• Type: Conference
• Year: 2009
• Where: KI
• Authors: Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo
• Keywords: Artificial Intelligence, External Axioms, KI 2009, Logic Atp System, Normal Internal Axioms