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

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.

Original languageEnglish (US)
Title of host publicationKI 2009
Subtitle of host publicationAdvances in Artificial Intelligence - 32nd Annual German Conference on AI, Proceedings
Pages281-288
Number of pages8
DOIs
StatePublished - Dec 1 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

Other

Other32nd Annual German Conference on Artificial Intelligence, KI 2009
CountryGermany
CityPaderborn
Period9/15/099/18/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Suda, M., Sutcliffe, G., Wischnewski, P., Lamotte-Schubert, M., & De Melo, G. (2009). External sources of axioms in automated theorem proving. In KI 2009: Advances in Artificial Intelligence - 32nd Annual German Conference on AI, Proceedings (pp. 281-288). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5803 LNAI). https://doi.org/10.1007/978-3-642-04617-9_36