Automated Deduction - CADE-18 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings /

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

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...

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

• 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
• Recursive Path 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.