A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds; J.C. Blanchette

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds
, J.C. Blanchette

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

60 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence
Subtitle of host publication	IJCAI 2016, New York, NY, USA, 9-15 July 2016
Publisher	IJCAI/AAAI Press
Pages	4205-4209
ISBN (Print)	978-1-57735-770-4
Publication status	Published - 2016
Externally published	Yes

Access to Document

sisterAccepted author manuscript, 131 KB

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{3874b1f75bf8426daf6847acde4c00cb,

title = "A Decision Procedure for (Co)datatypes in SMT Solvers",

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.",

author = "Andrew Reynolds and J.C. Blanchette",

year = "2016",

language = "English",

isbn = "978-1-57735-770-4",

pages = "4205--4209",

booktitle = "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence",

publisher = "IJCAI/AAAI Press",

}

A Decision Procedure for (Co)datatypes in SMT Solvers. / Reynolds, Andrew; Blanchette, J.C.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence: IJCAI 2016, New York, NY, USA, 9-15 July 2016. IJCAI/AAAI Press, 2016. p. 4205-4209.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A Decision Procedure for (Co)datatypes in SMT Solvers

AU - Reynolds, Andrew

AU - Blanchette, J.C.

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

M3 - Conference contribution

SN - 978-1-57735-770-4

SP - 4205

EP - 4209

BT - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence

PB - IJCAI/AAAI Press

ER -

A Decision Procedure for (Co)datatypes in SMT Solvers

Abstract

Access to Document

Persistent URL (handle)

Fingerprint

Cite this