Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
33
views
20
references
Top references
cited by
5
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
3,005
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Automated Deduction - CADE-25
A Decision Procedure for (Co)datatypes in SMT Solvers
other
Author(s):
Andrew Reynolds
,
Jasmin Christian Blanchette
Publication date
(Online):
July 25 2015
Publisher:
Springer International Publishing
Read this book at
Publisher
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Thermal Imaging in Social Decision Making
Most cited references
20
Record
: found
Abstract
: not found
Article
: not found
Results on the propositional μ-calculus
Dexter Kozen
(1983)
0
comments
Cited
209
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Simplification by Cooperating Decision Procedures
Greg Nelson
,
Derek Oppen
(1979)
0
comments
Cited
102
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Book Chapter
: not found
CVC4
Clark Barrett
,
Christopher Conway
,
Morgan Deters
…
(2011)
0
comments
Cited
61
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2015
Publication date (Online):
July 25 2015
Pages
: 197-213
DOI:
10.1007/978-3-319-21401-6_13
SO-VID:
ed909b37-eb0d-46ad-b333-40ce3a7c5a64
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 3
History and Prospects for First-Order Automated Deduction
pp. 29
Stumbling Around in the Dark: Lessons from Everyday Mathematics
pp. 55
Automated Reasoning in the Wild
pp. 73
Automating Leibniz’s Theory of Concepts
pp. 101
Confluence Competition 2015
pp. 105
Termination Competition (termCOMP 2015)
pp. 111
Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent
pp. 127
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems
pp. 137
Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies
pp. 152
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
pp. 163
Reducing Relative Termination to Dependency Pair Problems
pp. 181
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
pp. 197
A Decision Procedure for (Co)datatypes in SMT Solvers
pp. 214
Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux
pp. 231
A Formalisation of Finite Automata Using Hereditarily Finite Sets
pp. 246
SEPIA: Search for Proofs Using Inferred Automata
pp. 256
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3
pp. 272
Inductive Beluga: Programming Proofs
pp. 285
SMTtoTPTP – A Converter for Theorem Proving Formats
pp. 295
CTL Model Checking in Deduction Modulo
pp. 311
Quantifier-Free Equational Logic and Prime Implicate Generation
pp. 326
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
pp. 339
Cooperating Proof Attempts
pp. 356
Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
pp. 367
Beagle – A Hierarchic Superposition Theorem Prover
pp. 389
System Description: E.T. 0.1
pp. 399
Playing with AVATAR
pp. 419
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
pp. 434
Exploring Theories with a Model-Finding Assistant
pp. 450
Abstract Interpretation as Automated Deduction
pp. 467
A Uniform Substitution Calculus for Differential Dynamic Logic
pp. 482
Program Synthesis Using Dual Interpretation
pp. 501
Automated Theorem Proving for Assertions in Separation Logic with All Connectives
pp. 517
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS
pp. 539
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition
pp. 557
Regular Patterns in Second-Order Unification
pp. 572
Theorem Proving with Bounded Rigid E-Unification
pp. 591
Expressing Symmetry Breaking in DRAT Proofs
pp. 607
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
pp. 623
Linear Integer Arithmetic Revisited
Similar content
3,005
On the semantics of nested datatypes
Authors:
Clare Martin
,
Jeremy Gibbons
Processes functions and datatypes
Authors:
Vasco Vasconcelos
XML Schema Part 2: Datatypes
Authors:
V Biron P
See all similar
Cited by
5
Model Finding for Recursive Functions in SMT
Authors:
Andrew G Reynolds
,
Jasmin Christian Blanchette
,
Simon Cruanes
…
Induction with Generalization in Superposition Reasoning
Authors:
Márton Hajdú
,
Petra Hozzová
,
Laura Kovács
…
The Vampire and the FOOL
Authors:
,
,
…
See all cited by