Publication

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Joseph Reynolds
2015
Conference Papers

Abstract

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 theories developed with Isabelle demonstrates the potential of the procedure.

Official source

https://infoscience.epfl.ch/entities/publication/a02917e5-2cf6-494e-9c3a-80c1179333e7

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

A Decision Procedure for (Co)datatypes in SMT Solvers

Chat with Graph Search

Monotonicity Reasoning in the Age of Neural Foundation Models

Decision Procedures for Program Synthesis and Verification

Evaluating Cases in Legal Disputes as Rival Theories