2009 | OriginalPaper | Chapter
External Sources of Axioms in Automated Theorem Proving
Authors : Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo
Published in: KI 2009: Advances in Artificial Intelligence
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.