Progress in the development of automated theorem proving for higher-order logic

Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss

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

10 Scopus citations

Abstract

The Thousands of Problems for Theorem Provers (TPTP) problem library is the basis of a well established infrastructure supporting research, development, and deployment of first-order Automated Theorem Proving (ATP) systems. Recently, the TPTP has been extended to include problems in higher-order logic, with corresponding infrastructure and resources. This paper describes the practical progress that has been made towards the goal of TPTP support for higher-order ATP systems.

Original languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-22 - 22nd International Conference on Automated Deduction, Proceedings
Pages116-130
Number of pages15
DOIs
StatePublished - Sep 14 2009
Event22nd International Conference on Automated Deduction, CADE-22 - Montreal, QC, Canada
Duration: Aug 2 2009Aug 7 2009

Publication series

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

Other

Other22nd International Conference on Automated Deduction, CADE-22
CountryCanada
CityMontreal, QC
Period8/2/098/7/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Progress in the development of automated theorem proving for higher-order logic'. Together they form a unique fingerprint.

  • Cite this

    Sutcliffe, G., Benzmüller, C., Brown, C. E., & Theiss, F. (2009). Progress in the development of automated theorem proving for higher-order logic. In Automated Deduction - CADE-22 - 22nd International Conference on Automated Deduction, Proceedings (pp. 116-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5663 LNAI). https://doi.org/10.1007/978-3-642-02959-2_8