This book constitutes the refereed proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002, held in Tbilisi, Georgia in October 2002.
The 30 revised full papers presented were carefully reviewed and selected from 68 submissions. Among the topics covered are constraint programming, formal software enginering, formal verification, resolution, unification, proof planning, agent splitting, binary decision diagrams, binding, linear logic, Isabelle theorem prover, guided reduction, etc.
Author(s): M. Alpuente, S. Escobar, B. Gramlich (auth.), Matthias Baaz, Andrei Voronkov (eds.)
Series: Lecture Notes in Computer Science 2514 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2002
Language: English
Pages: 470
Tags: Computer Science, general; Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics)
Improving On-Demand Strategy Annotations....Pages 1-18
First-Order Logic as a Constraint Programming Language....Pages 19-35
Maintenance of Formal Software Developments by Stratified Verification....Pages 36-52
A Note on Universal Measures for Weak Implicit Computational Complexity....Pages 53-67
Extending Compositional Message Sequence Graphs....Pages 68-85
Searching for Invariants Using Temporal Resolution....Pages 86-101
Proof Planning for Feature Interactions: A Preliminary Report....Pages 102-114
An Extension of BDI CTL with Functional Dependencies and Components....Pages 115-129
Binding Logic: Proofs and Models....Pages 130-144
Directed Automated Theorem Proving....Pages 145-159
A Framework for Splitting BDI Agents....Pages 160-174
On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics....Pages 175-189
Using BDDs with Combinations of Theories....Pages 190-201
On Expressive Description Logics with Composition of Roles in Number Restrictions....Pages 202-215
Query Optimization of Disjunctive Databases with Constraints through Binding Propagation....Pages 216-230
A Non-commutative Extension of MELL....Pages 231-246
Procedural Semantics for Fuzzy Disjunctive Programs....Pages 247-261
Pushdown Specifications....Pages 262-277
Theorem Proving with Sequence Variables and Flexible Arity Symbols....Pages 278-291
Games, Probability, and the Quantitative μ-Calculus qMμ ....Pages 292-310
Parallelism and Tree Regular Constraints....Pages 311-326
Gödel Logics and Cantor-Bendixon Analysis....Pages 327-336
A Semantics for Proof Plans with Applications to Interactive Proof Planning....Pages 337-351
An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction....Pages 352-366
Proof Development with ΩMEGA: √2 Is Irrational....Pages 367-387
A Local System for Linear Logic....Pages 388-402
Investigating Type-Certifying Compilation with Isabelle....Pages 403-417
Automating Type Soundness Proofs via Decision Procedures and Guided Reductions....Pages 418-434
Abox Satisfiability Reduced to Terminological Reasoning in Expressive Description Logics....Pages 435-449
Fuzzy Prolog: A Simple General Implementation Using ( R )....Pages 450-463
