default search action
25th CADE 2015: Berlin, Germany
- Amy P. Felty, Aart Middeldorp:
Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science 9195, Springer 2015, ISBN 978-3-319-21400-9
Past, Present and Future of Automated Deduction
- David A. Plaisted:
History and Prospects for First-Order Automated Deduction. 3-28 - Ursula Martin
:
Stumbling Around in the Dark: Lessons from Everyday Mathematics. 29-51
Invited Talks
- Ulrich Furbach, Björn Pelzer, Claudia Schon:
Automated Reasoning in the Wild. 55-72 - Jesse Alama, Paul E. Oppenheimer
Automating Leibniz's Theory of Concepts. 73-97
Competition Descriptions
- Takahito Aoto, Nao Hirokawa
Confluence Competition 2015. 101-104 - Jürgen Giesl
Termination Competition (termCOMP 2015). 105-108
Rewriting
- Masahiko Sakai
Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent. 111-126 - Kiraku Shintani, Nao Hirokawa
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems. 127-136 - Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai
Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies. 137-151 - Haruhiko Sato, Sarah Winkler
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion. 152-162 - José Iborra, Naoki Nishida, Germán Vidal
Reducing Relative Termination to Dependency Pair Problems. 163-178
Decision Procedures
- Grant Olney Passmore:
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers. 181-196 - Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. 197-213 - Amélie David:
Deciding ATL*Satisfiability by Tableaux. 214-228
Interactive/Automated Theorem Proving and Applications
- Lawrence C. Paulson:
A Formalisation of Finite Automata Using Hereditarily Finite Sets. 231-245 - Thomas Gransden, Neil Walkinshaw
SEPIA: Search for Proofs Using Inferred Automata. 246-255 - Filip Maric, Predrag Janicic
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3. 256-271 - Brigitte Pientka, Andrew Cave:
Inductive Beluga: Programming Proofs. 272-281
New Techniques for Automating and Sharing Proofs
- Peter Baumgartner:
SMTtoTPTP - A Converter for Theorem Proving Formats. 285-294 - Kailiang Ji:
CTL Model Checking in Deduction Modulo. 295-310 - Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
Quantifier-Free Equational Logic and Prime Implicate Generation. 311-325 - Aleks Kissinger
Quantomatic: A Proof Assistant for Diagrammatic Reasoning. 326-336
Automating First-Order Logic
- Giles Reger
Cooperating Proof Attempts. 339-355 - Jan Gorzny
Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. 356-366 - Peter Baumgartner, Joshua Bax, Uwe Waldmann:
Beagle - A Hierarchic Superposition Theorem Prover. 367-377 - Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad
The Lean Theorem Prover (System Description). 378-388 - Cezary Kaliszyk
System Description: E.T. 0.1. 389-398 - Giles Reger
Playing with AVATAR. 399-415
Combinations
- Paula Daniela Chocron
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. 419-433 - Salman Saghafi, Ryan Danas, Daniel J. Dougherty:
Exploring Theories with a Model-Finding Assistant. 434-449 - Vijay D'Silva, Caterina Urban:
Abstract Interpretation as Automated Deduction. 450-464
Hybrid Sytems and Program Synthesis
- André Platzer
A Uniform Substitution Calculus for Differential Dynamic Logic. 467-481 - Ashish Tiwari, Adrià Gascón, Bruno Dutertre:
Program Synthesis Using Dual Interpretation. 482-497
Logics and Systems for Program Verification
- Zhe Hou
Automated Theorem Proving for Assertions in Separation Logic with All Connectives. 501-516 - Crystal Chang Din
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS. 517-526 - Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer:
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. 527-538 - Philippe Balbiani
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition. 539-554
Unification
- Tomer Libal
Regular Patterns in Second-Order Unification. 557-571 - Peter Backeman, Philipp Rümmer:
Theorem Proving with Bounded Rigid E-Unification. 572-587
SAT/SMT
- Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Expressing Symmetry Breaking in DRAT Proofs. 591-606 - Edward Zulkoski, Vijay Ganesh
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. 607-622 - Martin Bromberger, Thomas Sturm
Linear Integer Arithmetic Revisited. 623-637
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-22 18:47 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: