A Decision Procedure for (Co)datatypes in SMT Solvers

详细信息    查看全文

• 作者：Andrew Reynolds ; Jasmin Christian Blanchette
• 关键词：(Co)inductive datatypes ; Automatic theorem provers ; SMT solvers ; Decision procedures
• 刊名：Journal of Automated Reasoning
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：58
• 期：3
• 页码：341-362
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation;
• 出版者：Springer Netherlands
• ISSN：1573-0670
• 卷排序：58

文摘

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from formalizations developed with Isabelle demonstrates the potential of the procedure.