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

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

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

10 Citations (Scopus)

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 publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages116-130
Number of pages15
Volume5663 LNAI
DOIs
StatePublished - 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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Automated Theorem Proving
Theorem proving
Higher-order Logic
Infrastructure
Support Theorem
Theorem
Research and Development
Higher Order
First-order
Resources

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5663 LNAI, 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

Progress in the development of automated theorem proving for higher-order logic. / Sutcliffe, Geoffrey; Benzmüller, Christoph; Brown, Chad E.; Theiss, Frank.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5663 LNAI 2009. p. 116-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5663 LNAI).

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

Sutcliffe, G, Benzmüller, C, Brown, CE & Theiss, F 2009, Progress in the development of automated theorem proving for higher-order logic. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5663 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5663 LNAI, pp. 116-130, 22nd International Conference on Automated Deduction, CADE-22, Montreal, QC, Canada, 8/2/09. https://doi.org/10.1007/978-3-642-02959-2_8
Sutcliffe G, Benzmüller C, Brown CE, Theiss F. Progress in the development of automated theorem proving for higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5663 LNAI. 2009. p. 116-130. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02959-2_8
Sutcliffe, Geoffrey ; Benzmüller, Christoph ; Brown, Chad E. ; Theiss, Frank. / Progress in the development of automated theorem proving for higher-order logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5663 LNAI 2009. pp. 116-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{e5c1b7b3063342e3b14da0b50c1fa705,
title = "Progress in the development of automated theorem proving for higher-order logic",
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.",
author = "Geoffrey Sutcliffe and Christoph Benzm{\"u}ller and Brown, {Chad E.} and Frank Theiss",
year = "2009",
doi = "10.1007/978-3-642-02959-2_8",
language = "English (US)",
isbn = "3642029582",
volume = "5663 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "116--130",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

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

AU - Sutcliffe, Geoffrey

AU - Benzmüller, Christoph

AU - Brown, Chad E.

AU - Theiss, Frank

PY - 2009

Y1 - 2009

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

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

UR - http://www.scopus.com/inward/record.url?scp=69949119711&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=69949119711&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02959-2_8

DO - 10.1007/978-3-642-02959-2_8

M3 - Conference contribution

AN - SCOPUS:69949119711

SN - 3642029582

SN - 9783642029585

VL - 5663 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 116

EP - 130

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -