Superposition with Datatypes and Codatatypes

Jasmin Christian Blanchette; Nicolas Peltier; Simon Robillard

doi:10.1007/978-3-319-94205-6_25

Superposition with Datatypes and Codatatypes

Jasmin Christian Blanchette
, Nicolas Peltier
, Simon Robillard^*

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

45 Downloads (Pure)

Abstract

The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We propose two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms. Both techniques are refutationally complete with respect to nonstandard models of datatypes and nonbranching codatatypes. They take into account the acyclicity of datatype values and the existence and uniqueness of cyclic codatatype values. We implemented them in the first-order prover Vampire and compare them experimentally.

Original language	English
Title of host publication	Automated Reasoning
Subtitle of host publication	9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
Editors	Didier Galmiche, Stephan Schulz, Roberto Sebastiani
Publisher	Springer/Verlag
Pages	370-387
Number of pages	18
ISBN (Electronic)	9783319942056
ISBN (Print)	9783319942049
DOIs	https://doi.org/10.1007/978-3-319-94205-6_25
Publication status	Published - 2018
Event	9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 14 Jul 2018 → 17 Jul 2018

Publication series

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

Conference

Conference	9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	14/07/18 → 17/07/18

Funding

Blanchette has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Robillard has received funding from the ERC Starting Grant 2014 SYMCAR 639270, the Wallenberg Academy Fellowship 2014 TheProSE, the Swedish Research Council grant GenPro D0497701, and the Austrian FWF research project RiSE S11409-N23.

Funders	Funder number
SYMCAR
Horizon 2020 Framework Programme	639270, 713999
European Research Council
Austrian Science Fund	S11409-N23
Vetenskapsrådet	GenPro D0497701

Access to Document

10.1007/978-3-319-94205-6_25

Superposition with Datatypes and CodatatypesFinal published version, 343 KBLicence: Article 25fa Dutch Copyright Act

Persistent URL (handle)

Persistent link

Cite this

Blanchette, J. C., Peltier, N., & Robillard, S. (2018). Superposition with Datatypes and Codatatypes. In D. Galmiche, S. Schulz, & R. Sebastiani (Eds.), Automated Reasoning : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (pp. 370-387). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI). Springer/Verlag. https://doi.org/10.1007/978-3-319-94205-6_25

Blanchette, Jasmin Christian ; Peltier, Nicolas ; Robillard, Simon. / Superposition with Datatypes and Codatatypes. Automated Reasoning : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. editor / Didier Galmiche ; Stephan Schulz ; Roberto Sebastiani. Springer/Verlag, 2018. pp. 370-387 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3fc2820f0fd64898ba1b2d32a1794257,

title = "Superposition with Datatypes and Codatatypes",

abstract = "The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We propose two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms. Both techniques are refutationally complete with respect to nonstandard models of datatypes and nonbranching codatatypes. They take into account the acyclicity of datatype values and the existence and uniqueness of cyclic codatatype values. We implemented them in the first-order prover Vampire and compare them experimentally.",

author = "Blanchette, \{Jasmin Christian\} and Nicolas Peltier and Simon Robillard",

year = "2018",

doi = "10.1007/978-3-319-94205-6\_25",

language = "English",

isbn = "9783319942049",

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

publisher = "Springer/Verlag",

pages = "370--387",

editor = "Didier Galmiche and Stephan Schulz and Roberto Sebastiani",

booktitle = "Automated Reasoning",

note = "9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 14-07-2018 Through 17-07-2018",

}

Blanchette, JC, Peltier, N & Robillard, S 2018, Superposition with Datatypes and Codatatypes. in D Galmiche, S Schulz & R Sebastiani (eds), Automated Reasoning : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10900 LNAI, Springer/Verlag, pp. 370-387, 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 14/07/18. https://doi.org/10.1007/978-3-319-94205-6_25

Superposition with Datatypes and Codatatypes. / Blanchette, Jasmin Christian; Peltier, Nicolas; Robillard, Simon.
Automated Reasoning : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. ed. / Didier Galmiche; Stephan Schulz; Roberto Sebastiani. Springer/Verlag, 2018. p. 370-387 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10900 LNAI).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Superposition with Datatypes and Codatatypes

AU - Blanchette, Jasmin Christian

AU - Peltier, Nicolas

AU - Robillard, Simon

PY - 2018

Y1 - 2018

N2 - The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We propose two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms. Both techniques are refutationally complete with respect to nonstandard models of datatypes and nonbranching codatatypes. They take into account the acyclicity of datatype values and the existence and uniqueness of cyclic codatatype values. We implemented them in the first-order prover Vampire and compare them experimentally.

AB - The absence of a finite axiomatization of the first-order theory of datatypes and codatatypes represents a challenge for automatic theorem provers. We propose two approaches to reason by saturation in this theory: one is a conservative theory extension with a finite number of axioms; the other is an extension of the superposition calculus, in conjunction with axioms. Both techniques are refutationally complete with respect to nonstandard models of datatypes and nonbranching codatatypes. They take into account the acyclicity of datatype values and the existence and uniqueness of cyclic codatatype values. We implemented them in the first-order prover Vampire and compare them experimentally.

UR - https://www.scopus.com/pages/publications/85049993287

UR - https://www.scopus.com/pages/publications/85049993287#tab=citedBy

U2 - 10.1007/978-3-319-94205-6_25

DO - 10.1007/978-3-319-94205-6_25

M3 - Conference contribution

AN - SCOPUS:85049993287

SN - 9783319942049

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

SP - 370

EP - 387

BT - Automated Reasoning

A2 - Galmiche, Didier

A2 - Schulz, Stephan

A2 - Sebastiani, Roberto

PB - Springer/Verlag

T2 - 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 14 July 2018 through 17 July 2018

ER -

Blanchette JC, Peltier N, Robillard S. Superposition with Datatypes and Codatatypes. In Galmiche D, Schulz S, Sebastiani R, editors, Automated Reasoning : 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings. Springer/Verlag. 2018. p. 370-387. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2018 Jun 30. doi: 10.1007/978-3-319-94205-6_25

Superposition with Datatypes and Codatatypes

Abstract

Publication series

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this