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

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

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Pfenning, Frank (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
Σειρά:Lecture Notes in Computer Science, 4603
Θέματα:
Computer science.
Software engineering.
Computer logic.
Mathematical logic.
Artificial intelligence.
Computer Science.
Artificial Intelligence (incl. Robotics).
Mathematical Logic and Formal Languages.
Logics and Meanings of Programs.
Software Engineering.
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • 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.

Παρόμοια τεκμήρια