Extending a brainiac prover to lambda-free higher-order logic

Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, Stephan Schulz

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition-based prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higher-order logic.

LanguageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1
EditorsLijun Zhang, Tomáš Vojnar
PublisherSpringer Verlag
Pages192-210
Number of pages19
Volume1
ISBN (Electronic)9783030174620
ISBN (Print)9783030174613
DOIs
Publication statusPublished - 2019
Event25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019

Publication series

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

Conference

Conference25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19

Fingerprint

Higher-order Logic
Data structures
Algorithms and Data Structures
Higher Order
Theorem proving
Heuristics
Theorem Proving
Superposition
Calculus
Encoding
First-order
Partial

Cite this

Vukmirović, P., Blanchette, J. C., Cruanes, S., & Schulz, S. (2019). Extending a brainiac prover to lambda-free higher-order logic. In L. Zhang, & T. Vojnar (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1 (Vol. 1, pp. 192-210). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11427 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-17462-0_11
Vukmirović, Petar ; Blanchette, Jasmin Christian ; Cruanes, Simon ; Schulz, Stephan. / Extending a brainiac prover to lambda-free higher-order logic. Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1. editor / Lijun Zhang ; Tomáš Vojnar. Vol. 1 Springer Verlag, 2019. pp. 192-210 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c99b1b8584b84fca95125fded4cd60af,
title = "Extending a brainiac prover to lambda-free higher-order logic",
abstract = "Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition-based prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higher-order logic.",
author = "Petar Vukmirović and Blanchette, {Jasmin Christian} and Simon Cruanes and Stephan Schulz",
year = "2019",
doi = "10.1007/978-3-030-17462-0_11",
language = "English",
isbn = "9783030174613",
volume = "1",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "192--210",
editor = "Lijun Zhang and Tom{\'a}š Vojnar",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",

}

Vukmirović, P, Blanchette, JC, Cruanes, S & Schulz, S 2019, Extending a brainiac prover to lambda-free higher-order logic. in L Zhang & T Vojnar (eds), Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1. vol. 1, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11427 LNCS, Springer Verlag, pp. 192-210, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-17462-0_11

Extending a brainiac prover to lambda-free higher-order logic. / Vukmirović, Petar; Blanchette, Jasmin Christian; Cruanes, Simon; Schulz, Stephan.

Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1. ed. / Lijun Zhang; Tomáš Vojnar. Vol. 1 Springer Verlag, 2019. p. 192-210 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11427 LNCS).

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Extending a brainiac prover to lambda-free higher-order logic

AU - Vukmirović, Petar

AU - Blanchette, Jasmin Christian

AU - Cruanes, Simon

AU - Schulz, Stephan

PY - 2019

Y1 - 2019

N2 - Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition-based prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higher-order logic.

AB - Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition-based prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ -free higher-order logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higher-order logic.

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

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

U2 - 10.1007/978-3-030-17462-0_11

DO - 10.1007/978-3-030-17462-0_11

M3 - Conference contribution

SN - 9783030174613

VL - 1

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

SP - 192

EP - 210

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Zhang, Lijun

A2 - Vojnar, Tomáš

PB - Springer Verlag

ER -

Vukmirović P, Blanchette JC, Cruanes S, Schulz S. Extending a brainiac prover to lambda-free higher-order logic. In Zhang L, Vojnar T, editors, Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1. Vol. 1. Springer Verlag. 2019. p. 192-210. (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-17462-0_11