A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds, J.C. Blanchette

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.
Original languageEnglish
Title of host publicationProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence
Subtitle of host publicationIJCAI 2016, New York, NY, USA, 9-15 July 2016
PublisherIJCAI/AAAI Press
Pages4205-4209
ISBN (Print)978-1-57735-770-4
Publication statusPublished - 2016
Externally publishedYes

Fingerprint Dive into the research topics of 'A Decision Procedure for (Co)datatypes in SMT Solvers'. Together they form a unique fingerprint.

  • Cite this

    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.