Automated Deduction - CADE-19 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Baader, Franz (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
• Έκδοση: 1st ed. 2003.
• Σειρά: Lecture Notes in Artificial Intelligence ; 2741
• Θέματα: Artificial intelligence.; Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Artificial Intelligence.; Programming Languages, Compilers, Interpreters.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.

This volume contains the papers presented at the 19th International Conference on Automated Deduction (CADE-19) held 28 July-2 August 2003 in Miami Beach, Florida, USA. They are divided into the following categories: - 4 contributions by invited speakers: one full paper and three short abstracts; -...

Πίνακας περιεχομένων:

• Session 1: Invited Talk
• SAT-Based Counterexample Guided Abstraction Refinement in Model Checking
• Session 2
• Equational Abstractions
• Deciding Inductive Validity of Equations
• Automating the Dependency Pair Method
• An AC-Compatible Knuth-Bendix Order
• Session 3
• The Complexity of Finite Model Reasoning in Description Logics
• Optimizing a BDD-Based Modal Solver
• A Translation of Looping Alternating Automata into Description Logics
• Session 4
• Foundational Certified Code in a Metalogical Framework
• Proving Pointer Programs in Higher-Order Logic
• ?
• Subset Types and Partial Functions
• Session 5
• Reasoning about Quantifiers by Matching in the E-graph
• Session 6
• A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols
• Superposition Modulo a Shostak Theory
• Canonization for Disjoint Unions of Theories
• Matching in a Class of Combined Non-disjoint Theories
• Session 7
• Reasoning about Iteration in Gödel's Class Theory
• Algorithms for Ordinal Arithmetic
• Certifying Solutions to Permutation Group Problems
• Session 8: System Descriptions
• TRP++ 2.0: A Temporal Resolution Prover
• IsaPlanner: A Prototype Proof Planner in Isabelle
• 'Living Book' :- 'Deduction', 'Slicing', 'Interaction'
• The Homer System
• Session 9: CASC-19 Results
• The CADE-19 ATP System Competition
• Session 10: Invited Talk
• Proof Search and Proof Check for Equational and Inductive Theorems
• Session 11: System Descriptions
• The New WALDMEISTER Loop at Work
• About VeriFun
• How to Prove Inductive Theorems? QuodLibet!
• Session 12: Invited Talk
• Reasoning about Qualitative Representations of Space and Time
• Session 13
• Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation
• The Model Evolution Calculus
• Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
• Efficient Instance Retrieval with Standard and Relational Path Indexing
• Session 14
• Monodic Temporal Resolution
• A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
• Schematic Saturation for Decision and Unification Problems
• Session 15
• Unification Modulo ACUI Plus Homomorphisms/Distributivity
• Source-Tracking Unification
• Optimizing Higher-Order Pattern Unification
• Decidability of Arity-Bounded Higher-Order Matching.