21. CADE 2007: Bremen, Germany

Frank Pfenning (Ed.): Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Lecture Notes in Computer Science 4603 Springer 2007, ISBN 978-3-540-73594-6 BibTeX

Session 1. Invited Talk: Colin Stirling

Colin Stirling:
Games, Automata and Matching. 1-2
Electronic Edition (link) BibTeX

Session 2. Higher-Order Logic

Osman Hasan, Sofiène Tahar:
Formalization of Continuous Probability Distributions. 3-18
Electronic Edition (link) BibTeX
Guodong Li, Konrad Slind:
Compilation as Rewriting in Higher Order Logic. 19-34
Electronic Edition (link) BibTeX
Christian Urban, Stefan Berghofer, Michael Norrish:
Barendregt's Variable Convention in Rule Inductions. 35-50
Electronic Edition (link) BibTeX
John Harrison:
Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. 51-66
Electronic Edition (link) BibTeX

Session 3. Description Logic

Boris Motik, Rob Shearer, Ian Horrocks:
Optimized Reasoning in Description Logics Using Hypertableaux. 67-83
Electronic Edition (link) BibTeX
Carsten Lutz, Frank Wolter:
Conservative Extensions in the Lightweight Description Logic EL. 84-99
Electronic Edition (link) BibTeX
Gulay Ünel, David Toman:
An Incremental Technique for Automata-Based Decision Procedures. 100-115
Electronic Edition (link) BibTeX

Session 4. Intuitionistic Logic

Samuli Heilala, Brigitte Pientka:
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. 116-131
Electronic Edition (link) BibTeX
Roger Antonsen, Arild Waaler:
A Labelled System for IPL with Variable Splitting. 132-146
Electronic Edition (link) BibTeX

Session 5. Invited Talk: Ashish Tiwari

Ashish Tiwari, Sumit Gulwani:
Logical Interpretation: Static Program Analysis Using Theorem Proving. 147-166
Electronic Edition (link) BibTeX

Session 6. Satisfiability Modulo Theories

Yeting Ge, Clark Barrett, Cesare Tinelli:
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. 167-182
Electronic Edition (link) BibTeX
Leonardo Mendonça de Moura, Nikolaj Bjørner:
Efficient E-Matching for SMT Solvers. 183-198
Electronic Edition (link) BibTeX
Maria Paola Bonacina, Mnacho Echenim:
T-Decision by Decomposition. 199-214
Electronic Edition (link) BibTeX
Viktor Kuncak, Martin C. Rinard:
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. 215-230
Electronic Edition (link) BibTeX

Session 7. Induction, Rewriting, and Polymorphism

Markus Aderhold:
Improvements in Formula Generalization. 231-246
Electronic Edition (link) BibTeX
Guillem Godoy, Sophie Tison:
On the Normalization and Unique Normalization Properties of Term Rewrite Systems. 247-262
Electronic Edition (link) BibTeX
Jean-Francois Couchot, Stéphane Lescuyer:
Handling Polymorphism in Automated Deduction. 263-278
Electronic Edition (link) BibTeX

Session 8. First-Order Logic

Peter Höfner, Georg Struth:
Automated Reasoning in Kleene Algebra. 279-294
Electronic Edition (link) BibTeX
Geoff Sutcliffe, Yury Puzis:
SRASS - A Semantic Relevance Axiom Selection System. 295-310
Electronic Edition (link) BibTeX
Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv:
Labelled Clauses. 311-327
Electronic Edition (link) BibTeX
Christopher Lynch, Duc-Khanh Tran:
Automatic Decidability and Combinability Revisited. 328-344
Electronic Edition (link) BibTeX

Session 9. Invited Talk: K. Rustan M. Leino

K. Rustan M. Leino:
Designing Verification Conditions for Software. 345
Electronic Edition (link) BibTeX

Session 10. Model Checking and Verification

Juan Antonio Navarro Pérez, Andrei Voronkov:
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. 346-361
Electronic Edition (link) BibTeX
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli:
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. 362-378
Electronic Edition (link) BibTeX
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt:
The KeY system 1.0 (Deduction Component). 379-384
Electronic Edition (link) BibTeX
Oleg Mürk, Daniel Larsson, Reiner Hähnle:
KeY-C: A Tool for Verification of C Programs. 385-390
Electronic Edition (link) BibTeX
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu:
The Bedwyr System for Model Checking over Syntactic Expressions. 391-397
Electronic Edition (link) BibTeX
Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich:
System for Automated Deduction (SAD): A Tool for Proof Verification. 398-403
Electronic Edition (link) BibTeX

Session 11. Invited Talk: Peter Baumgartner

Peter Baumgartner:
Logical Engineering with Instance-Based Methods. 404-409
Electronic Edition (link) BibTeX

Session 12. Termination

Adam Koprowski, Aart Middeldorp:
Predictive Labeling with Dependency Pairs Using SAT. 410-425
Electronic Edition (link) BibTeX
Stephan Falke, Deepak Kapur:
Dependency Pairs for Rewriting with Non-free Constructors. 426-442
Electronic Edition (link) BibTeX
Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp:
Proving Termination by Bounded Increase. 443-459
Electronic Edition (link) BibTeX
Alexander Krauss:
Certified Size-Change Termination. 460-475
Electronic Edition (link) BibTeX

Session 13. Tableaux and First-Order Systems

Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor:
Encoding First Order Proofs in SAT. 476-491
Electronic Edition (link) BibTeX
Peter Baumgartner, Ulrich Furbach, Björn Pelzer:
Hyper Tableaux with Equality. 492-507
Electronic Edition (link) BibTeX
Björn Pelzer, Christoph Wernhard:
System Description: E-KRHyper. 508-513
Electronic Edition (link) BibTeX
Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic:
System Description: SpassVersion 3.0. 514-520
Electronic Edition (link) BibTeX