自动演绎－CADE-18/会议录 Automated deduction-CADE-18

出版时间：2002-12  出版社：1 edition (2002年9月1日)  作者：Andrei Voronkov  页数：534  

内容概要

This book constitutes the refereed proceedings of the 18th International Conference on Automated Deduction, CADE - 18, held in Copenhagen, Denmark, in July 2002.The 27 revised full papers and 10 system descriptions presented together with three invited contributions were carefully reviewed and selected from 70 submissions. The book offers topical sections on description logics and the semantic Web, proofcarrying code and compiler verifications, non-classical logics, system descriptions, SAT, model generation, CASC, combination and decision procedures, logical frameworks, model checking, equational reasoning, and proof theory.

书籍目录

Session 1. Description Logics and Semantic Web　Reasoning with Expressive Description Logics: Theory and Practice .　BDD-Based Decision Procedures for KSession 2. 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 IsabelleSession 3. Non-classical Logics　Embedding Lax Logic into Intuitionistic Logic　Combining Proof-Search and Counter-Model Construction for　Deciding GSdel-Dummett Logic　Connection-Based Proof Search in Propositional BI LogicSession 4. 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 LogicsSession 5. 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 PropositionsSession 6. 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 Modelg Represented by Ground　Atoms with Ground EquationsSession 7.　A New Clausal Class Decidable by HyperresolntionSession 8.CASCSession 9.Session 10.Combination of Decision ProceduressSession 11.Logical FrameworksSession 12. Model CheckingSession 13.Epuational ReasoningSession 14.Prllf TheoryAuthor Index