Automated Deduction - CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings

Front Matter....Pages I-XXVIII
Front Matter....Pages 1-1
History and Prospects for First-Order Automated Deduction....Pages 3-28
Stumbling Around in the Dark: Lessons from Everyday Mathematics....Pages 29-51
Front Matter....Pages 53-53
Automated Reasoning in the Wild....Pages 55-72
Automating Leibniz’s Theory of Concepts....Pages 73-97
Front Matter....Pages 99-99
Confluence Competition 2015....Pages 101-104
Termination Competition (termCOMP 2015)....Pages 105-108
Front Matter....Pages 109-109
Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent....Pages 111-126
CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems....Pages 127-136
Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies....Pages 137-151
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion....Pages 152-162
Reducing Relative Termination to Dependency Pair Problems....Pages 163-178
Front Matter....Pages 179-179
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers....Pages 181-196
A Decision Procedure for (Co)datatypes in SMT Solvers....Pages 197-213
Front Matter....Pages 214-228
A Formalisation of Finite Automata Using Hereditarily Finite Sets....Pages 229-229
SEPIA: Search for Proofs Using Inferred Automata....Pages 231-245
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3....Pages 246-255
Inductive Beluga: Programming Proofs....Pages 256-271
Front Matter....Pages 272-281
SMTtoTPTP – A Converter for Theorem Proving Formats....Pages 283-283
CTL Model Checking in Deduction Modulo....Pages 285-294
Front Matter....Pages 295-310
Quantifier-Free Equational Logic and Prime Implicate Generation....Pages 283-283
Quantomatic: A Proof Assistant for Diagrammatic Reasoning....Pages 311-325
Front Matter....Pages 326-336
Cooperating Proof Attempts....Pages 337-337
Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses....Pages 339-355
Beagle – A Hierarchic Superposition Theorem Prover....Pages 356-366
The Lean Theorem Prover (System Description)....Pages 367-377
System Description: E.T. 0.1....Pages 378-388
Playing with AVATAR....Pages 389-398
Front Matter....Pages 399-415
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited....Pages 417-417
Exploring Theories with a Model-Finding Assistant....Pages 419-433
Abstract Interpretation as Automated Deduction....Pages 434-449
Front Matter....Pages 450-464
A Uniform Substitution Calculus for Differential Dynamic Logic....Pages 465-465
Program Synthesis Using Dual Interpretation....Pages 467-481
Front Matter....Pages 482-497
Automated Theorem Proving for Assertions in Separation Logic with All Connectives....Pages 499-499
KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS....Pages 501-516
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems....Pages 517-526
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition....Pages 527-538
Front Matter....Pages 539-554
Regular Patterns in Second-Order Unification....Pages 555-555
Theorem Proving with Bounded Rigid E-Unification....Pages 557-571
Front Matter....Pages 572-587
Expressing Symmetry Breaking in DRAT Proofs....Pages 589-589
Front Matter....Pages 591-606
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers....Pages 589-589
Linear Integer Arithmetic Revisited....Pages 607-622
Back Matter....Pages 623-637
....Pages 639-640