Cover Image

Automated Deduction - CADE-21 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings /

Corporate Author: SpringerLink (Online service)
Other Authors: Pfenning, Frank. (Editor, http://id.loc.gov/vocabulary/relators/edt)
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2007.
Edition:1st ed. 2007.
Series:Lecture Notes in Artificial Intelligence ; 4603
Subjects:
Artificial intelligence.
Mathematical logic.
Computer logic.
Software engineering.
Artificial Intelligence.
Mathematical Logic and Formal Languages.
Logics and Meanings of Programs.
Software Engineering.
Online Access:https://doi.org/10.1007/978-3-540-73595-3
Table of Contents:
  • Session 1. Invited Talk: Colin Stirling
  • Games, Automata and Matching
  • Session 2. Higher-Order Logic
  • Formalization of Continuous Probability Distributions
  • Compilation as Rewriting in Higher Order Logic
  • Barendregt’s Variable Convention in Rule Inductions
  • Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
  • Session 3. Description Logic
  • Optimized Reasoning in Description Logics Using Hypertableaux
  • Conservative Extensions in the Lightweight Description Logic
  • An Incremental Technique for Automata-Based Decision Procedures
  • Session 4. Intuitionistic Logic
  • Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4
  • A Labelled System for IPL with Variable Splitting
  • Session 5. Invited Talk: Ashish Tiwari
  • Logical Interpretation: Static Program Analysis Using Theorem Proving
  • Session 6. Satisfiability Modulo Theories
  • Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
  • Efficient E-Matching for SMT Solvers
  • -Decision by Decomposition
  • Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
  • Session 7. Induction, Rewriting, and Polymorphism
  • Improvements in Formula Generalization
  • On the Normalization and Unique Normalization Properties of Term Rewrite Systems
  • Handling Polymorphism in Automated Deduction
  • Session 8. First-Order Logic
  • Automated Reasoning in Kleene Algebra
  • SRASS - A Semantic Relevance Axiom Selection System
  • Labelled Clauses
  • Automatic Decidability and Combinability Revisited
  • Session 9. Invited Talk: K. Rustan M. Leino
  • Designing Verification Conditions for Software
  • Session 10. Model Checking and Verification
  • Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
  • Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
  • The KeY system 1.0 (Deduction Component)
  • KeY-C: A Tool for Verification of C Programs
  • The Bedwyr System for Model Checking over Syntactic Expressions
  • System for Automated Deduction (SAD): A Tool for Proof Verification
  • Session 11. Invited Talk: Peter Baumgartner
  • Logical Engineering with Instance-Based Methods
  • Session 12. Termination
  • Predictive Labeling with Dependency Pairs Using SAT
  • Dependency Pairs for Rewriting with Non-free Constructors
  • Proving Termination by Bounded Increase
  • Certified Size-Change Termination
  • Session 13. Tableaux and First-Order Systems
  • Encoding First Order Proofs in SAT
  • Hyper Tableaux with Equality
  • System Description: E- KRHyper
  • System Description: Spass Version 3.0.

Similar Items