Automated Deduction - CADE-18
Editat de Andrei Voronkoven Limba Engleză Paperback – 17 iul 2002
Preț: 335.05 lei
Preț vechi: 418.81 lei
-20%
Puncte Express: 503
Carte tipărită la comandă
Livrare economică 14-28 septembrie
Livrare prin curier în România Termenul estimat este afișat lângă disponibilitate.
Transport gratuit de la 400.00 lei Plată online sau ramburs, în funcție de opțiunile comenzii.
Retur gratuit în 14 zile Comandă securizată și suport în română.
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.