Automated Deduction - CADE-19 [electronic resource] : 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings / edited by Franz Baader.

1st ed. 2003.
Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
Computer Science (Springer-11645)
Lecture notes in computer science. Lecture notes in artificial intelligence 2741
Lecture Notes in Artificial Intelligence ; 2741
1 online resource (XII, 512 pages)
Artificial intelligence.
Programming languages (Electronic computers).
Computer logic.
Logic, Symbolic and mathematical.
Local subjects:
Artificial Intelligence. (search)
Programming Languages, Compilers, Interpreters. (search)
Logics and Meanings of Programs. (search)
Mathematical Logic and Formal Languages. (search)
System Details:
text file PDF
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; - 29 accepted technical papers; - 7 descriptions of automated reasoning systems. These proceedings also contain a short description of the automated theor- proving system competition (CASC-19) organized by Geo? Sutcli?e and Chr- tian Suttner. Despite many competing smaller conferences and workshops covering di?- entaspectsofautomateddeduction,CADEisstillthemajorforumfordiscussing new results on all aspects of automated deduction as well as presenting new s- tems and improvements of established systems. In contrast to the previous year, when CADE was one of the conferences participating in the Third Federated Logic Conference (FLoC 2002), and next year, when CADE will be part of the Second International Joint Conference on Automated Reasoning (IJCAR 2004), CADE-19 was organized as a stand-alone event.
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.
Baader, Franz, editor., Editor,
SpringerLink (Online service)
Contained In:
Springer eBooks
Other format:
Printed edition:
Printed edition:
Publisher Number:
10.1007/b11829 doi
Access Restriction:
Restricted for use by site license.
Location Notes Your Loan Policy
Description Status Barcode Your Loan Policy