Automated Deduction – CADE-20 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings /

Automated Deduction – CADE-20 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Nieuwenhuis, Robert (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2005.
Σειρά:Lecture Notes in Computer Science, 3632
Θέματα:
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
Πίνακας περιεχομένων:
  • What Do We Know When We Know That a Theory Is Consistent?
  • Reflecting Proofs in First-Order Logic with Equality
  • Reasoning in Extensional Type Theory with Equality
  • Nominal Techniques in Isabelle/HOL
  • Tabling for Higher-Order Logic Programming
  • A Focusing Inverse Method Theorem Prover for First-Order Linear Logic
  • The CoRe Calculus
  • Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures
  • Privacy-Sensitive Information Flow with JML
  • The Decidability of the First-Order Theory of Knuth-Bendix Order
  • Well-Nested Context Unification
  • Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules
  • The OWL Instance Store: System Description
  • Temporal Logics over Transitive States
  • Deciding Monodic Fragments by Temporal Resolution
  • Hierarchic Reasoning in Local Theory Extensions
  • Proof Planning for First-Order Temporal Logic
  • System Description: Multi A Multi-strategy Proof Planner
  • Decision Procedures Customized for Formal Verification
  • An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
  • Connecting Many-Sorted Theories
  • A Proof-Producing Decision Procedure for Real Arithmetic
  • The MathSAT 3 System
  • Deduction with XOR Constraints in Security API Modelling
  • On the Complexity of Equational Horn Clauses
  • A Combination Method for Generating Interpolants
  • sKizzo: A Suite to Evaluate and Certify QBFs
  • Regular Protocols and Attacks with Regular Knowledge
  • The Model Evolution Calculus with Equality
  • Model Representation via Contexts and Implicit Generalizations
  • Proving Properties of Incremental Merkle Trees
  • Computer Search for Counterexamples to Wilkie’s Identity
  • KRHyper – In Your Pocket.

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