Grunge: A grand unified ATP challenge

Chad E. Brown; Thibault Gauthier; Cezary Kaliszyk; Geoff Sutcliffe; Josef Urban

doi:10.1007/978-3-030-29436-6_8

Grunge: A grand unified ATP challenge

Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

5 Scopus citations

Abstract

This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possi-bly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.

Original language	English (US)
Title of host publication	Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings
Editors	Pascal Fontaine
Publisher	Springer
Pages	123-141
Number of pages	19
ISBN (Print)	9783030294359
DOIs	https://doi.org/10.1007/978-3-030-29436-6_8
State	Published - 2019
Event	27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil Duration: Aug 27 2019 → Aug 30 2019

Publication series

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

Conference

Conference	27th International Conference on Automated Deduction, CADE 2019
Country	Brazil
City	Natal
Period	8/27/19 → 8/30/19

Keywords

First-order logic
Higher-order logic
Many-sorted logic
Theorem proving

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-29436-6_8

Fingerprint Dive into the research topics of 'Grunge: A grand unified ATP challenge'. Together they form a unique fingerprint.

Cite this

Brown, C. E., Gauthier, T., Kaliszyk, C., Sutcliffe, G., & Urban, J. (2019). Grunge: A grand unified ATP challenge. In P. Fontaine (Ed.), Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings (pp. 123-141). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI). Springer. https://doi.org/10.1007/978-3-030-29436-6_8

Grunge : A grand unified ATP challenge. / Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef.

Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. ed. / Pascal Fontaine. Springer, 2019. p. 123-141 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Brown, CE, Gauthier, T, Kaliszyk, C, Sutcliffe, G & Urban, J 2019, Grunge: A grand unified ATP challenge. in P Fontaine (ed.), Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11716 LNAI, Springer, pp. 123-141, 27th International Conference on Automated Deduction, CADE 2019, Natal, Brazil, 8/27/19. https://doi.org/10.1007/978-3-030-29436-6_8

Brown CE, Gauthier T, Kaliszyk C, Sutcliffe G, Urban J. Grunge: A grand unified ATP challenge. In Fontaine P, editor, Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. Springer. 2019. p. 123-141. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-29436-6_8

Brown, Chad E. ; Gauthier, Thibault ; Kaliszyk, Cezary ; Sutcliffe, Geoff ; Urban, Josef. / Grunge : A grand unified ATP challenge. Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. editor / Pascal Fontaine. Springer, 2019. pp. 123-141 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7b468537115e462880afea84c0124131,

title = "Grunge: A grand unified ATP challenge",

abstract = "This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possi-bly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.",

keywords = "First-order logic, Higher-order logic, Many-sorted logic, Theorem proving",

author = "Brown, {Chad E.} and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban",

note = "Funding Information: Supported by the ERC grant no. 649043 AI4REASON and no. 714034 SMART, by the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15 003/0000466, the European Regional Development Fund, and the National Science Foundation Grant 1730419-?CI-SUSTAIN: StarExec: Cross-Community Infrastructure for Logic Solving?.; 27th International Conference on Automated Deduction, CADE 2019 ; Conference date: 27-08-2019 Through 30-08-2019",

year = "2019",

doi = "10.1007/978-3-030-29436-6_8",

language = "English (US)",

isbn = "9783030294359",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "123--141",

editor = "Pascal Fontaine",

booktitle = "Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings",

}

TY - GEN

T1 - Grunge

T2 - 27th International Conference on Automated Deduction, CADE 2019

AU - Brown, Chad E.

AU - Gauthier, Thibault

AU - Kaliszyk, Cezary

AU - Sutcliffe, Geoff

AU - Urban, Josef

N1 - Funding Information: Supported by the ERC grant no. 649043 AI4REASON and no. 714034 SMART, by the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15 003/0000466, the European Regional Development Fund, and the National Science Foundation Grant 1730419-?CI-SUSTAIN: StarExec: Cross-Community Infrastructure for Logic Solving?.

PY - 2019

Y1 - 2019

N2 - This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possi-bly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.

AB - This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possi-bly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.

KW - First-order logic

KW - Higher-order logic

KW - Many-sorted logic

KW - Theorem proving

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

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

U2 - 10.1007/978-3-030-29436-6_8

DO - 10.1007/978-3-030-29436-6_8

M3 - Conference contribution

AN - SCOPUS:85076987302

SN - 9783030294359

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

SP - 123

EP - 141

BT - Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings

A2 - Fontaine, Pascal

PB - Springer

Y2 - 27 August 2019 through 30 August 2019

ER -