A decision procedure for (co)datatypes in SMT solvers

DOI10.1007/S10817-016-9372-6MaRDI QIDQ2360873zbMATH OpenOpenAlexFDO

Authors Andrew Reynolds, Jasmin Christian Blanchette

Publication date 29 June 2017

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01643154/file/jour.pdf

zbMATH Keywords

automatic theorem proversdecision proceduresSMT solvers(co)inductive datatypes

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• A decision procedure for (co)datatypes in SMT solvers
• Witnessing (co)datatypes
• Superposition with datatypes and codatatypes
• Decision procedures for algebraic data types with abstractions
• scientific article; zbMATH DE number 1903374

Cites work

• A decision procedure for (co)datatypes in SMT solvers
• A formally verified compiler back-end
• An abstract decision procedure for a theory of inductive data types.
• Combining nonstably infinite theories
• Combining superposition and induction: a practical realization
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Computer Aided Verification
• Efficient E-Matching for SMT Solvers
• Extending Sledgehammer with SMT solvers
• Induction for SMT solvers
• Isabelle/HOL. A proof assistant for higher-order logic
• Model finding for recursive functions in SMT
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• On Rational Trees
• On equal -terms
• Quantifier instantiation techniques for finite model finding in SMT
• Results on the propositional \(\mu\)-calculus
• Sharing is caring: combination of theories
• Simplification by Cooperating Decision Procedures
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Theory of finite or infinite trees revisited
• Truly modular (co)datatypes for Isabelle/HOL
• Universal coalgebra: A theory of systems
• Verifying a Compiler for Java Threads
• Witnessing (co)datatypes

Cited in

(12)

• An abstract decision procedure for satisfiability in the theory of recursive data types
• Reasoning in the theory of heap: satisfiability and interpolation
• Witnessing (co)datatypes
• Adding decision procedures to SMT solvers using axioms with triggers
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Solving constrained Horn clauses over algebraic data types
• scientific article; zbMATH DE number 7453200 (Why is no real title available?)
• Datatypes with shared selectors
• Politeness for the theory of algebraic datatypes
• A decision procedure for (co)datatypes in SMT solvers
• Reasoning about algebraic data types with abstractions
• Polite combination of algebraic datatypes

Describes a project that uses

Uses Software

• Nunchaku
• Archive Formal Proofs
• Stern-Brocot Tree
• RADA
• CVC4
• StarExec
• Sledgehammer
• z3
• SMT-LIB
• Isabelle/HOL
• Nitpick

This page was built for publication: A decision procedure for (co)datatypes in SMT solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2360873)