A Decision Procedure for (Co)datatypes in SMT Solvers

Reynolds, Andrew; Blanchette, Jasmin Christian

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds, Jasmin Christian Blanchette

Download BibTeX Cite

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 4205-4208.

Abstract

Datatypes and codata types 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.

Andrew Reynolds, and Jasmin Christian Blanchette. 2016. A Decision Procedure for (Co)datatypes in SMT Solvers. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16. IJCAI, 4205–4208. https://ijcai.org/proceedings/2016/631

@inproceedings{ijcai2016p631,
  title     = {A Decision Procedure for (Co)datatypes in SMT Solvers},
  author    = {Reynolds, Andrew and Blanchette, Jasmin Christian},
  booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
               Artificial Intelligence, {IJCAI-16}},
  publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
  editor    = {Subbarao Kambhampati},
  pages     = {4205--4208},
  year      = {2016},
  month     = {7},
  url       = {https://ijcai.org/proceedings/2016/631},
}

TY  - CPAPER
TI  - A Decision Procedure for (Co)datatypes in SMT Solvers
AU  - Reynolds, Andrew
AU  - Blanchette, Jasmin Christian
T2  - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16
PB  - AAAI Press / International Joint Conferences on Artificial Intelligence
PY  - 2016
SP  - 4205
EP  - 4208
UR  - https://ijcai.org/proceedings/2016/631
ER  -