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.
Type de document :
Communication dans un congrès
IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01904588
Contributeur : Jasmin Christian Blanchette <>
Soumis le : jeudi 25 octobre 2018 - 10:42:46
Dernière modification le : mercredi 12 décembre 2018 - 14:00:10

Fichier

supdata_paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

70

Téléchargements de fichiers

5