A Decision Procedure for (Co)datatypes in SMT Solvers

Abstract : Datatypes and codatatypes are useful to represent finite and potentially infinite objects. We describe a decision procedure to reason about such types. The procedure has been integrated into CVC4, a modern SMT (satisfiability modulo theories) solver, which can be used both as a constraint solver and as an automatic theorem prover. An evaluation based on formalizations developed in the Isabelle proof assistant shows the potential of the procedure.
Type de document :
Communication dans un congrès
IJCAI 2016, Jul 2016, New York City, United States. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01397082
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mardi 15 novembre 2016 - 14:15:02
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:23:53

Fichier

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

Identifiants

  • HAL Id : hal-01397082, version 1

Collections

Citation

Andrew Reynolds, Jasmin Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016, Jul 2016, New York City, United States. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016. 〈hal-01397082〉

Partager

Métriques

Consultations de la notice

89

Téléchargements de fichiers

40