A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds, J.C. Blanchette

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

12 Downloads (Pure)

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

Cite this