Automated deduction - CADE-16 : 16th International Conference on Automated Deduction Trento, Italy, July 7 10, 1999 : proceedings
Saved in:
| Corporate Author: | |
|---|---|
| Other Authors: | |
| Format: | Livre numérique |
| Language: | Anglais |
| Published: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Series: | Lecture notes in computer science. Lecture notes in artificial intelligence
1632 |
| Subjects: | |
| Online Access: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
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 16, 16th International; Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings, [edited by] Harald Ganzinger, 1999, New York, Springer, 1 vol. (XIV-428 p.), Lecture notes in computer science, 3-540-66222-7 • Automated Deduction - CADE-16, Texte imprimé, 9783662182055 |
Table of Contents:
- Session 1
- A Dynamic Programming Approach to Categorial Deduction
- Tractable Transformations from Modal Provability Logics into First-Order Logic
- Session 2
- Decision Procedures for Guarded Logics
- A PSpace Algorithm for Graded Modal Logic
- Session 3
- Solvability of Context Equations with Two Context Variables Is Decidable
- Complexity of the Higher Order Matching
- Solving Equational Problems Efficiently
- Session 4
- VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up
- A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers
- Presenting Proofs in a Human-Oriented Way
- Session 5
- On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
- Maslov s Class K Revisited
- Prefixed Resolution: A Resolution Method for Modal and Description Logics
- Session 6: System Descriptions
- System Description: Twelf A Meta-Logical Framework for Deductive Systems
- System Description: inka 5.0 - A Logic Voyager
- System Description: CutRes 0.1: Cut Elimination by Resolution
- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving
- System Description Using OBDD s for the Validationof Skolem Verification Conditions
- Fault-Tolerant Distributed Theorem Proving
- System Description: Waldmeister Improvements in Performance and Ease of Use
- Session 7
- Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems
- A Formalization of Static Analyses in System F
- On Explicit Reflection in Theorem Proving and Formal Verification
- Session 8: System Descriptions
- System Description: Kimba, A Model Generator for Many-Valued First-Order Logics
- System Description:Teyjus A Compiler and Abstract Machine Based Implementation of ?Prolog
- Vampire
- System Abstract: E 0.3
- Session 9
- Invited Talk: Rewrite-Based Deduction and Symbolic Constraints
- Towards an Automatic Analysis of Security Protocols in First-Order Logic
- Session 10
- A Confluent Connection Calculus
- Abstraction-Based Relevancy Testing for Model Elimination
- A Breadth-First Strategy for Mating Search
- Session 11: System Competitions
- The Design of the CADE-16 Inductive Theorem Prover Contest
- Session 12: System Descriptions
- System Description: Spass Version 1.0.0
- K : A Theorem Prover for K
- System Description: CYNTHIA
- System Description: MCS: Model-Based Conjecture Searching
- Session 13
- Embedding Programming Languages in Theorem Provers
- Extensional Higher-Order Paramodulation and RUE-Resolution
- Automatic Generation of Proof Search Strategies for Second-Order Logic.