default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID25th 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, Edward N. Zalta:
Automating Leibniz's Theory of Concepts. 73-97
Competition Descriptions
- Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, Harald Zankl:
Confluence Competition 2015. 101-104 - Jürgen Giesl, Frédéric Mesnard, Albert Rubio, René Thiemann, Johannes Waldmann:
Termination Competition (termCOMP 2015). 105-108
Rewriting
- Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa:
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, Akihisa Yamada:
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, Rajeev Raman:
SEPIA: Search for Proofs Using Inferred Automata. 246-255 - Filip Maric, Predrag Janicic, Marko Malikovic:
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, Vladimir Zamdzhiev:
Quantomatic: A Proof Assistant for Diagrammatic Reasoning. 326-336
Automating First-Order Logic
- Giles Reger, Dmitry Tishkovsky, Andrei Voronkov:
Cooperating Proof Attempts. 339-355 - Jan Gorzny, Bruno Woltzenlogel Paleo:
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, Floris van Doorn, Jakob von Raumer:
The Lean Theorem Prover (System Description). 378-388 - Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil:
System Description: E.T. 0.1. 389-398 - Giles Reger, Martin Suda, Andrei Voronkov:
Playing with AVATAR. 399-415
Combinations
- Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen:
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, Rajeev Goré, Alwen Tiu:
Automated Theorem Proving for Assertions in Separation Logic with All Connectives. 501-516 - Crystal Chang Din, Richard Bubel, Reiner Hähnle:
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, Joseph Boudou:
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, Krzysztof Czarnecki:
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers. 607-622 - Martin Bromberger, Thomas Sturm, Christoph Weidenbach:
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 2026-01-29 02:21 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:
