Automated deduction CADE-19 : 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 August 2, 2003 : proceedings
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 a...
Enregistré dans:
| Institution som forfatter: | |
|---|---|
| Andre forfattere: | |
| Format: | Livre numérique |
| Sprog: | Anglais |
| Udgivet: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serier: | Lecture notes in computer science. Lecture notes in artificial intelligence
2741 |
| Fag: | |
| Online adgang: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Kommentar: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Automated deduction, CADE-19, 19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28-August 2, 2003, proceedings, Franz Baader (ed.), Berlin, Springer, 2003, 1 vol. (XII-502 p.), Lecture notes in computer science, 3-540-40559-3 • Automated Deduction - CADE-19, Texte imprimé, 9783662188224 |
Indholdsfortegnelse:
- 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 ModelEvolution 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.