Logic for Programming, Artificial Intelligence, and Reasoning: 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007. Proceedings

Johann A. Makowsky (auth.), Nachum Dershowitz, Andrei Voronkov (eds.)3540755586, 9783540755586

This book constitutes the refereed proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007, held in Yerevan, Armenia, October 2007.

The 36 revised full papers presented together with 15 short papers and three invited talks were carefully reviewed and selected from 78 submissions. The papers address all current issues in logic programming, logic-based program manipulation, formal method, automated reasoning, and various kinds of AI logics.

---

Table of contents :
Front Matter….Pages –
From Hilbert’s Program to a Logic Toolbox….Pages 1-1
On the Notion of Vacuous Truth….Pages 2-14
Whatever Happened to Deductive Question Answering?….Pages 15-16
Decidable Fragments of Many-Sorted Logic….Pages 17-31
One-Pass Tableaux for Computation Tree Logic….Pages 32-46
Extending a Resolution Prover for Inequalities on Elementary Functions….Pages 47-61
Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic….Pages 62-76
Monadic Fragments of Gödel Logics: Decidability and Undecidability Results….Pages 77-91
Least and Greatest Fixed Points in Linear Logic….Pages 92-106
The Semantics of Consistency and Trust in Peer Data Exchange Systems….Pages 107-122
Completeness and Decidability in Sequence Logic….Pages 123-137
HORPO with Computability Closure: A Reconstruction….Pages 138-150
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs….Pages 151-165
Matching in Hybrid Terminologies….Pages 166-180
Verifying Cryptographic Protocols with Subterms Constraints….Pages 181-195
Deciding Knowledge in Security Protocols for Monoidal Equational Theories….Pages 196-210
Mechanized Verification of CPS Transformations….Pages 211-225
Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap….Pages 226-241
Protocol Verification Via Rigid/Flexible Resolution….Pages 242-256
Preferential Description Logics….Pages 257-272
On Two Extensions of Abstract Categorial Grammars….Pages 273-287
Why Would You Trust B ?….Pages 288-302
How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited….Pages 303-317
On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards….Pages 318-332
Data Complexity in the $mathcal{EL}$ Family of Description Logics….Pages 333-347
An Extension of the Knuth-Bendix Ordering with LPO-Like Properties….Pages 348-362
Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic….Pages 363-377
Integrating Inductive Definitions in SAT….Pages 378-392
The Separation Theorem for Differential Interaction Nets….Pages 393-407
Complexity of Planning in Action Formalisms Based on Description Logics….Pages 408-422
Faster Phylogenetic Inference with MXG….Pages 423-437
Enriched μ –Calculus Pushdown Module Checking….Pages 438-453
Approved Models for Normal Logic Programs….Pages 454-468
Permutative Additives and Exponentials….Pages 469-483
Algorithms for Propositional Model Counting….Pages 484-498
Completeness for Flat Modal Fixpoint Logics….Pages 499-513
$mathbb{FDNC}$ : Decidable Non-monotonic Disjunctive Logic Programs with Function Symbols….Pages 514-530
The Complexity of Temporal Logic with Until and Since over Ordinals….Pages 531-545
ATP Cross-Verification of the Mizar MPTP Challenge Problems….Pages 546-560
Back Matter….Pages –