Automated Reasoning
Editat de David Basin, Michael Rusinowitchen Limba Engleză Paperback – 22 iun 2004
Preț: 632.79 lei
Preț vechi: 790.99 lei
-20%
Puncte Express: 949
Preț estimativ în valută:
111.87€ • 133.38$ • 97.03£
111.87€ • 133.38$ • 97.03£
Carte tipărită la comandă
Livrare economică 16-30 martie
Specificații
ISBN-13: 9783540223450
ISBN-10: 3540223452
Pagini: 512
Ilustrații: XII, 491 p.
Dimensiuni: 155 x 235 x 28 mm
Greutate: 0.77 kg
Ediția:2004
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540223452
Pagini: 512
Ilustrații: XII, 491 p.
Dimensiuni: 155 x 235 x 28 mm
Greutate: 0.77 kg
Ediția:2004
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Rewriting.- Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools.- A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting.- Efficient Checking of Term Ordering Constraints.- Improved Modular Termination Proofs Using Dependency Pairs.- Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure.- Saturation-Based Theorem Proving.- Redundancy Notions for Paramodulation with Non-monotonic Orderings.- A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards.- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures.- Combination Techniques.- Decision Procedures for Recursive Data Structures with Integer Constraints.- Modular Proof Systems for Partial Functions with Weak Equality.- A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics.- Verification and Systems.- Using Automated Theorem Provers to Certify Auto-generated Aerospace Software.- argo-lib: A Generic Platform for Decision Procedures.- The ICS Decision Procedures for Embedded Deduction.- System Description: E 0.81.- Reasoning with Finite Structure.- Second-Order Logic over Finite Structures – Report on a Research Programme.- Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains.- Tableaux and Non-classical Logics.- PDL with Negation of Atomic Programs.- Counter-Model Search in Gödel-Dummett Logics.- Generalised Handling of Variables in Disconnection Tableaux.- Applications and Systems.- Chain Resolution for the Semantic Web.- Sonic — Non-standard Inferences Go OilEd.- TeMP: A Temporal Monodic Prover.- Dr.Doodle: A Diagrammatic Theorem Prover.- Computer Mathematics.- SolvingConstraints by Elimination Methods.- Analyzing Selected Quantified Integer Programs.- Interactive Theorem Proving.- Formalizing O Notation in Isabelle/HOL.- Experiments on Supporting Interactive Proof Using Resolution.- A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.- Combinatorial Reasoning.- Automatic Generation of Classification Theorems for Finite Algebras.- Efficient Algorithms for Computing Modulo Permutation Theories.- Overlapping Leaf Permutative Equations.- Higher-Order Reasoning.- TaMeD: A Tableau Method for Deduction Modulo.- Lambda Logic.- Formalizing Undefinedness Arising in Calculus.- Competition.- The CADE ATP System Competition.
Caracteristici
Includes supplementary material: sn.pub/extras