Logic for Programming, Artificial Intelligence, and Reasoning
Editat de Robert Nieuwenhuis, Andrei Voronkoven Limba Engleză Paperback – 21 noi 2001
Preț: 647.43 lei
Preț vechi: 809.29 lei
-20%
Puncte Express: 971
Preț estimativ în valută:
114.42€ • 132.05$ • 99.79£
114.42€ • 132.05$ • 99.79£
Carte tipărită la comandă
Livrare economică 18 mai-01 iunie
Specificații
ISBN-13: 9783540429579
ISBN-10: 3540429573
Pagini: 760
Ilustrații: XV, 741 p.
Dimensiuni: 155 x 235 x 41 mm
Greutate: 1.13 kg
Ediția:2001
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540429573
Pagini: 760
Ilustrații: XV, 741 p.
Dimensiuni: 155 x 235 x 41 mm
Greutate: 1.13 kg
Ediția:2001
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Invited Talk.- Monodic Fragments of First-Order Temporal Logics: 2000–2001 A.D..- Verification.- On Bounded Specifications.- Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy.- Local Temporal Logic Is Expressively Complete for Cograph Dependence Alphabets.- Guarded Logics.- Games and Model Checking for Guarded Logics.- Computational Space Efficiency and Minimal Model Generation for Guarded Formulae.- Agents.- Logical Omniscience and the Cost of Deliberation.- Local Conditional High-Level Robot Programs.- A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents.- Automated Theorem Proving.- Proof and Model Generation with Disconnection Tableaux.- Counting the Number of Equivalent Binary Resolution Proofs.- Automated Theorem Proving.- Splitting through New Proposition Symbols.- Complexity of Linear Standard Theories.- Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving.- Non-classical Logics.- Unification in a Description Logic with Transitive Closure of Roles.- Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions.- Types.- Coherence and Transitivity in Coercive Subtyping.- A Type-Theoretic Approach to Induction with Higher-Order Encodings.- Analysis of Polymorphically Typed Logic Programs Using ACI-Unification.- Experimental Papers.- Model Generation with Boolean Constraints.- First-Order Atom Definitions Extended.- Automated Proof Support for Interval Logics.- Foundations of Logic.- The Functions Provable by First Order Abstraction.- A Local System for Classical Logic.- CSP and SAT.- Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae.- Permutation Problems and ChannellingConstraints.- Simplifying Binary Propositional Theories into Connected Components Twice as Fast.- Non-monotonic Reasoning.- Reasoning about Evolving Nonmonotonic Knowledge Bases.- Efficient Computation of the Well-Founded Model Using Update Propagation.- Semantics.- Indexed Categories and Bottom-Up Semantics of Logic Programs.- Functional Logic Programming with Failure: A Set-Oriented View.- Operational Semantics for Fixed-Point Logics on Constraint Databases.- Experimental Papers.- Efficient Negation Using Abstract Interpretation.- Certifying Synchrony for Free.- A Computer Environment for Writing Ordinary Mathematical Proofs.- Termination.- On Termination of Meta-programs.- A Monotonic Higher-Order Semantic Path Ordering.- Knowledge-Based Systems.- The Elog Web Extraction Language.- Census Data Repair: A Challenging Application of Disjunctive Logic Programming.- Analysis of Logic Programs.- Boolean Functions for Finite-Tree Dependencies.- How to Transform an Analyzer into a Verifier.- Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search.- Databases and Knowledge Bases.- Coherent Composition of Distributed Knowledge-Bases through Abduction.- Tableaux for Reasoning about Atomic Updates.- Termination.- Inference of Termination Conditions for Numerical Loops in Prolog.- Termination of Rewriting with Strategy Annotations.- Inferring Termination Conditions for Logic Programs Using Backwards Analysis.- Program Analysis and Proof Planning.- Reachability Analysis of Term Rewriting Systems with Timbuk.- Binding-Time Annotations without Binding-Time Analysis.- Concept Formation via Proof Planning Failure.
Caracteristici
Includes supplementary material: sn.pub/extras