Extending the TPTP language to higher-order logic with automated parser generation

Allen Van Gelder, Geoffrey Sutcliffe

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

7 Citations (Scopus)

Abstract

A stable proposal for extending the first-order TPTP (Thousands of Problems for Theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document into a lex scanner and yacc parser.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages156-161
Number of pages6
Volume4130 LNAI
StatePublished - 2006
EventThird International Joint Conference on Automated Reasoning, IJCAR 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4130 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

OtherThird International Joint Conference on Automated Reasoning, IJCAR 2006
CountryUnited States
CitySeattle, WA
Period8/17/068/20/06

Fingerprint

Theorem proving
Higher-order Logic
Specification languages
Language
Specifications
Lambda Calculus
Theorem Proving
Specification Languages
Calculi
Linux
Scanner
Theorem
Sharing
Research Personnel
Specification
First-order
Design

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Van Gelder, A., & Sutcliffe, G. (2006). Extending the TPTP language to higher-order logic with automated parser generation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4130 LNAI, pp. 156-161). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4130 LNAI).

Extending the TPTP language to higher-order logic with automated parser generation. / Van Gelder, Allen; Sutcliffe, Geoffrey.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4130 LNAI 2006. p. 156-161 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4130 LNAI).

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

Van Gelder, A & Sutcliffe, G 2006, Extending the TPTP language to higher-order logic with automated parser generation. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 4130 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4130 LNAI, pp. 156-161, Third International Joint Conference on Automated Reasoning, IJCAR 2006, Seattle, WA, United States, 8/17/06.
Van Gelder A, Sutcliffe G. Extending the TPTP language to higher-order logic with automated parser generation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4130 LNAI. 2006. p. 156-161. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Van Gelder, Allen ; Sutcliffe, Geoffrey. / Extending the TPTP language to higher-order logic with automated parser generation. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4130 LNAI 2006. pp. 156-161 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{944f9a3459af480c850383f32cf28858,
title = "Extending the TPTP language to higher-order logic with automated parser generation",
abstract = "A stable proposal for extending the first-order TPTP (Thousands of Problems for Theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document into a lex scanner and yacc parser.",
author = "{Van Gelder}, Allen and Geoffrey Sutcliffe",
year = "2006",
language = "English (US)",
isbn = "3540371877",
volume = "4130 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "156--161",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Extending the TPTP language to higher-order logic with automated parser generation

AU - Van Gelder, Allen

AU - Sutcliffe, Geoffrey

PY - 2006

Y1 - 2006

N2 - A stable proposal for extending the first-order TPTP (Thousands of Problems for Theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document into a lex scanner and yacc parser.

AB - A stable proposal for extending the first-order TPTP (Thousands of Problems for Theorem Provers) language to higher-order logic, based primarily on lambda-calculus expressions, is presented. The purpose of the system is to facilitate sharing of theorem-proving problems in higher-order logic among many researchers. Design goals are discussed. BNF2, a new specification language, is presented. Unix/Linux scripts translate the specification document into a lex scanner and yacc parser.

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

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

M3 - Conference contribution

AN - SCOPUS:33749544375

SN - 3540371877

SN - 9783540371878

VL - 4130 LNAI

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

SP - 156

EP - 161

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

ER -