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.
|Title of host publication||Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence|
|Subtitle of host publication||IJCAI 2016, New York, NY, USA, 9-15 July 2016|
|Publication status||Published - 2016|
Reynolds, A., & Blanchette, J. C. (2016). A Decision Procedure for (Co)datatypes in SMT Solvers. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence: IJCAI 2016, New York, NY, USA, 9-15 July 2016 (pp. 4205-4209). IJCAI/AAAI Press.