A Decision Procedure for (Co)datatypes in SMT Solvers
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. PDF
Cite
Text
Reynolds and Blanchette. "A Decision Procedure for (Co)datatypes in SMT Solvers." International Joint Conference on Artificial Intelligence, 2016.Markdown
[Reynolds and Blanchette. "A Decision Procedure for (Co)datatypes in SMT Solvers." International Joint Conference on Artificial Intelligence, 2016.](https://mlanthology.org/ijcai/2016/reynolds2016ijcai-decision/)BibTeX
@inproceedings{reynolds2016ijcai-decision,
title = {{A Decision Procedure for (Co)datatypes in SMT Solvers}},
author = {Reynolds, Andrew and Blanchette, Jasmin Christian},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2016},
pages = {4205-4209},
url = {https://mlanthology.org/ijcai/2016/reynolds2016ijcai-decision/}
}