Skip to Main content Skip to Navigation
New interface
Conference papers

Superposition with Datatypes and Codatatypes

Abstract : The absence of a finite axiomatization of the first-order theory of data-types 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 non-branching 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Thursday, October 25, 2018 - 10:42:46 AM
Last modification on : Wednesday, July 6, 2022 - 4:18:53 AM
Long-term archiving on: : Saturday, January 26, 2019 - 1:32:19 PM


Files produced by the author(s)


  • HAL Id : hal-01904588, version 1


Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard. Superposition with Datatypes and Codatatypes. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. ⟨hal-01904588⟩



Record views


Files downloads