Automated Deduction - CADE-18
Editat de Andrei Voronkoven Limba Engleză Paperback – 17 iul 2002
Preț: 334.04 lei
Preț vechi: 417.55 lei
-20% Nou
Puncte Express: 501
Preț estimativ în valută:
59.12€ • 69.33$ • 51.83£
59.12€ • 69.33$ • 51.83£
Carte tipărită la comandă
Livrare economică 26 ianuarie-09 februarie 26
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783540439318
ISBN-10: 3540439315
Pagini: 552
Ilustrații: XII, 540 p.
Dimensiuni: 155 x 235 x 30 mm
Greutate: 0.83 kg
Ediția:2002
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540439315
Pagini: 552
Ilustrații: XII, 540 p.
Dimensiuni: 155 x 235 x 30 mm
Greutate: 0.83 kg
Ediția:2002
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
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.
Caracteristici
Includes supplementary material: sn.pub/extras