A Decision Procedure for (Co)datatypes in SMT Solvers - Archive ouverte HAL Access content directly
Conference Papers Year :

A Decision Procedure for (Co)datatypes in SMT Solvers

(1) , (2, 3)
1
2
3

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.
Fichier principal
Vignette du fichier
sister.pdf (131.41 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01397082 , version 1 (15-11-2016)

Identifiers

  • HAL Id : hal-01397082 , version 1

Cite

Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016 - 25th International Joint Conference on Artificial Intelligence, Jul 2016, New York, United States. ⟨hal-01397082⟩
100 View
80 Download

Share

Gmail Facebook Twitter LinkedIn More