Automated deduction - CADE-18 : 18th International Conference on Automated Deduction Copenhagen, Denmark, July 27 30, 2002 : proceedings
The First CADE in the Third Millennium This volume contains the papers presented at the Eighteenth International C- ference on Automated Deduction (CADE-18) held on July 27 30th, 2002, at the University of Copenhagen as part of the Federated Logic Conference (FLoC 2002). Despite a large number of de...
Guardat en:
| Autor corporatiu: | |
|---|---|
| Altres autors: | |
| Format: | Livre numérique |
| Idioma: | Anglais |
| Publicat: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Col·lecció: | Lecture notes in computer science. Lecture notes in artificial intelligence
2392 |
| Matèries: | |
| Accés en línia: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
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-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, Andrei Voronkov (ed.), Berlin, Springer, 2002, 1 vol. (XII-534 p.), Lecture notes in computer science, 3-540-43931-5 • Automated Deduction - CADE-18, Texte imprimé, 9783662194904 |
Taula de continguts:
- Description Logics and Semantic Web
- Reasoning with Expressive Description Logics: Theory and Practice
- BDD-Based Decision Procedures for
- Proof-Carrying Code and Compiler Verification
- Temporal Logic for Proof-Carrying Code
- A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code
- Formal Verification of a Java Compiler in Isabelle
- Non-classical Logics
- Embedding Lax Logic into Intuitionistic Logic
- Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic
- Connection-Based Proof Search in Propositional BI Logic
- System Descriptions
- DDDLIB: A Library for Solving Quantified Difference Inequalities
- An LCF-Style Interface between HOL and First-Order Logic
- System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning
- Proof Development with ?mega
- Learn?matic: System Description
- HyLoRes 1.0: Direct Resolution for Hybrid Logics
- SAT
- Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points
- A Note on Symmetry Heuristics in SEM
- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions
- Model Generation
- Deductive Search for Errors in Free Data Type Specifications Using Model Generation
- Reasoning by Symmetry and Function Ordering in Finite Model Generation
- Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations
- Session 7
- A New Clausal Class Decidable by Hyperresolution
- CASC
- Spass Version 2.0
- System Description: GrAnDe 1.0
- The HR Program for Theorem Generation
- AutoBayes/CC Combining Program Synthesis with Automatic Code Certification System Description
- CADE-CAV Invited Talk
- The Quest for Efficient Boolean Satisfiability Solvers
- Session 9
- RecursivePath Orderings Can Be Context-Sensitive
- Combination of Decision Procedures
- Shostak Light
- Formal Verification of a Combination Decision Procedure
- Combining Multisets with Integers
- Logical Frameworks
- The Reflection Theorem: A Study in Meta-theoretic Reasoning
- Faster Proof Checking in the Edinburgh Logical Framework
- Solving for Set Variables in Higher-Order Theorem Proving
- Model Checking
- The Complexity of the Graded ?-Calculus
- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains
- Equational Reasoning
- Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation
- Basic Syntactic Mutation
- The Next Waldmeister Loop
- Proof Theory
- Focussing Proof-Net Construction as a Middleware Paradigm
- Proof Analysis by Resolution.