Loading...
conference paper
A Decision Procedure for (Co)datatypes in SMT Solvers
2015
Automated Deduction - Cade-25
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.
Use this identifier to reference this record
Type
conference paper
Web of Science ID
WOS:000363947500013
Authors
Editors
Felty, Ap
•
Middeldorp, A
Publication date
2015
Publisher
Published in
Automated Deduction - Cade-25
ISBN of the book
978-3-319-21401-6
978-3-319-21400-9
Publisher place
Berlin
Total of pages
17
Series title/Series vol.
Lecture Notes in Artificial Intelligence
Volume
9195
Start page
197
End page
213
Peer reviewed
REVIEWED
EPFL units
Event name | Event place | Event date |
Berlin, GERMANY | AUG 01-07, 2015 | |
Available on Infoscience
December 2, 2015