资源分类
》 资源 》论文》A Decision Procedure for (Co)datatypes in SMT Solvers

A Decision Procedure for (Co)datatypes in SMT Solvers

2019-11-25 | |  51 |   43 |   0
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.

上一篇：Generating Tests for Robotized Painting Using Constraint Programming

下一篇：Why Prices Need Algorithms

用户评价
全部评价

热门资源

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • The Variational S...

    Unlike traditional images which do not offer in...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Rating-Boosted La...

    The performance of a recommendation system reli...