Superposition with Datatypes and Codatatypes

Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard*

*Corresponding author for this work

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

27 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 languageEnglish
Title of host publicationAutomated Reasoning
Subtitle of host publication9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
EditorsDidier Galmiche, Stephan Schulz, Roberto Sebastiani
PublisherSpringer/Verlag
Pages370-387
Number of pages18
ISBN (Electronic)9783319942056
ISBN (Print)9783319942049
DOIs
Publication statusPublished - 2018
Event9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 14 Jul 201817 Jul 2018

Publication series

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

Conference

Conference9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/TerritoryUnited Kingdom
CityOxford
Period14/07/1817/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.

FundersFunder number
SYMCAR
Horizon 2020 Framework Programme639270, 713999
European Research Council
Austrian Science FundS11409-N23
VetenskapsrådetGenPro D0497701

    Fingerprint

    Dive into the research topics of 'Superposition with Datatypes and Codatatypes'. Together they form a unique fingerprint.

    Cite this