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 metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01904588
Contributor : Jasmin Blanchette <>
Submitted on : Thursday, October 25, 2018 - 10:42:46 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Saturday, January 26, 2019 - 1:32:19 PM

File

supdata_paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01904588, version 1

Citation

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⟩

Share

Metrics

Record views

133

Files downloads

89