External sources of axioms in automated theorem proving

Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard De Melo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationKI 2009
Subtitle of host publicationAdvances in Artificial Intelligence - 32nd Annual German Conference on AI, Proceedings
Number of pages8
StatePublished - 2009
Event32nd Annual German Conference on Artificial Intelligence, KI 2009 - Paderborn, Germany
Duration: Sep 15 2009Sep 18 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5803 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other32nd Annual German Conference on Artificial Intelligence, KI 2009

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'External sources of axioms in automated theorem proving'. Together they form a unique fingerprint.

Cite this