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.
Andrew Reynolds, Jasmin Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016, Jul 2016, New York City, United States. ⟨hal-01397082⟩
