search for books and compare prices
Tables of Contents for Automated Deduction-Cade-18
Chapter/Section Title
Page #
Page Count
Session 1. Description Logics and Semantic Web
Reasoning with Expressive Description Logics: Theory and Practice
1
15
Ian Horrocks
BDD-Based Decision Procedures for K
16
15
Guoqiang Pan
Ulrike Sattler
Moshe Y. Vardi
Session 2. Proof-Carrying Code and Compiler Verification
Temporal Logic for Proof-Carrying Code
31
16
Andrew Bernard
Peter Lee
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code
47
16
Robert R. Schneck
George C. Necula
Formal Verification of a Java Compiler in Isabelle
63
15
Martin Strecker
Session 3. Non-classical Logics
Embedding Lax Logic into Intuitionistic Logic
78
16
Uwe Egly
Combining Proof-Search and Counter-Model Construction for Deciding Godel-Dummett Logic
94
17
Dominique Larchey-Wendling
Connection-Based Proof Search in Propositional BI Logic
111
18
Didier Galmiche
Daniel Mery
Session 4. System Descriptions
DDDLIB: A Library for Solving Quantified Difference Inequalities
129
5
Jesper B. Moller
An LCF-Style Interface between HOL and First-Order Logic
134
5
Joe Hurd
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
139
5
Jurgen Zimmer
Michael Kohlhase
Proof Development with ΩMEGA
144
6
Jorg Siekmann
Christoph Benzmuller
Vladimir Brezhnev
Lassaad Cheikhrouhou
Armin Fiedler
Andreas Franke
Helmut Horacek
Michael Kohlhase
Andreas Meier
Erica Melis
Markus Moschner
Immanuel Normann
Martin Pollet
Volker Sorge
Carsten Ullrich
Claus-Peter Wirth
Jurgen Zimmer
LearnΩmatic: System Description
150
6
Mateja Jamnik
Manfred Kerber
Martin Pollet
HyLoRes 1.0: Direct Resolution for Hybrid Logics
156
5
Carlos Areces
Juan Heguiabehere
Session 5. SAT
Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points
161
20
Eugene Goldberg
A Note on Symmetry Heuristics in SEM
181
14
Thierry Boy de la Tour
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions
195
16
Gilles Audemard
Piergiorgio Bertoli
Alessandro Cimatti
Artur Kornilowicz
Roberto Sebastiani
Session 6. Model Generation
Deductive Search for Errors in Free Data Type Specifications Using Model Generation
211
15
Wolfgang Ahrendt
Reasoning by Symmetry and Function Ordering in Finite Model Generation
226
15
Gilles Audemard
Belaid Benhamou
Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations
241
19
Bernhard Gramlich
Reinhard Pichler
Session 7.
A New Clausal Class Decidable by Hyperresolution
260
15
Lilia Georgieva
Ullrich Hustadt
Renate A. Schmidt
Session 8. CASC
Spass Version 2.0
275
5
Christoph Weidenbach
Uwe Brahm
Thomas Hillenbrand
Enno Keen
Christian Theobald
Dalibor Topic
System Description: GrAnDe 1.0
280
5
Stephan Schulz
Geoff Sutcliffe
The HR Program for Theorem Generation
285
5
Simon Colton
AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description
290
5
Michael Whalen
Johann Schumann
Bernd Fischer
CADE-CAV Invited Talk
The Quest for Efficient Boolean Satisfiability Solvers
295
19
Lintao Zhang
Sharad Malik
Session 9.
Recursive Path Orderings Can Be Context-Sensitive
314
18
Cristina Borralleras
Salvador Lucas
Albert Rubio
Session 10. Combination of Decision Procedures
Shostak Light
332
15
Harald Ganzinger
Formal Verification of a Combination Decision Procedure
347
16
Jonathan Ford
Natarajan Shankar
Combining Multisets with Integers
363
14
Calogero G. Zarba
Session 11. Logical Frameworks
The Reflection Theorem: A Study in Meta-theoretic Reasoning
377
15
Lawrence C. Paulson
Faster Proof Checking in the Edinburgh Logical Framework
392
16
Aaron Stump
David L. Dill
Solving for Set Variables in Higher-Order Theorem Proving
408
15
Chad E. Brown
Session 12. Model Checking
The Complexity of the Graded μ-Calculus
423
15
Orna Kupferman
Ulrike Sattler
Moshe Y. Vardi
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
438
18
Leonardo de Moura
Harald Rueb
Maria Sorea
Session 13. Equational Reasoning
Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation
456
15
Miquel Bofill
Albert Rubio
Basic Syntactic Mutation
471
15
Christopher Lynch
Barbara Morawska
The Next Waldmeister Loop
486
15
Thomas Hillenbrand
Bernd Lochner
Session 14. Proof Theory
Focussing Proof-Net Construction as a Middleware Paradigm
501
16
Jean Marc Andreoli
Proof Analysis by Resolution
517
16
Matthias Baaz
Author Index
533