Willkommen, schön sind Sie da!
Logo Ex Libris

Automated Deduction - CADE-18

  • E-Book (pdf)
  • 540 Seiten
(0) Erste Bewertung abgeben
Alle Bewertungen ansehen
Inhalt Description Logics and Semantic Web.- Reasoning with Expressive Description Logics: Theory and Practice.- BDD-Based Decisio... Weiterlesen
CHF 133.90
Download steht sofort bereit
Informationen zu E-Books
E-Books eignen sich auch für mobile Geräte (sehen Sie dazu die Anleitungen).
E-Books von Ex Libris sind mit Adobe DRM kopiergeschützt: Erfahren Sie mehr.
Weitere Informationen finden Sie hier.
Bestellung & Lieferung in eine Filiale möglich



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.


Titel: Automated Deduction - CADE-18
Untertitel: 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings
EAN: 9783540456209
Format: E-Book (pdf)
Hersteller: Springer Berlin Heidelberg
Genre: IT & Internet
Veröffentlichung: 02.08.2003
Digitaler Kopierschutz: Wasserzeichen
Anzahl Seiten: 540

Weitere Bände aus der Buchreihe "Lecture Notes in Computer Science"