Logic for Programming, Artificial Intelligence, and Reasoning: 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006. Proceedings

Front Matter....Pages -
Higher-Order Termination: From Kruskal to Computability....Pages 1-14
Deciding Satisfiability of Positive Second Order Joinability Formulae....Pages 15-29
SAT Solving for Argument Filterings....Pages 30-44
Inductive Decidability Using Implicit Induction....Pages 45-59
Matching Modulo Superdevelopments Application to Second-Order Matching....Pages 60-74
Derivational Complexity of Knuth-Bendix Orders Revisited....Pages 75-89
A Characterization of Alternating Log Time by First Order Functional Programs....Pages 90-104
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems....Pages 105-119
On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus....Pages 120-134
Modular Cut-Elimination: Finding Proofs or Counterexamples....Pages 135-149
An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf....Pages 150-166
A Semantic Completeness Proof for TaMeD....Pages 167-181
Saturation Up to Redundancy for Tableau and Sequent Calculi....Pages 182-196
Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints....Pages 197-211
Combining Supervaluation and Degree Based Reasoning Under Vagueness....Pages 212-226
A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes....Pages 227-241
A Local System for Intuitionistic Logic....Pages 242-256
CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions....Pages 257-271
Reducing Nondeterminism in the Calculus of Structures....Pages 272-286
A Relaxed Approach to Integrity and Inconsistency in Databases....Pages 287-301
On Locally Checkable Properties....Pages 302-316
Deciding Key Cycles for Security Protocols....Pages 317-331
Automating Verification of Loops by Parallelization....Pages 332-346
On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems....Pages 347-361
Verification Condition Generation Via Theorem Proving....Pages 362-376
An Incremental Approach to Abstraction-Carrying Code....Pages 377-391
Context-Sensitive Multivariant Assertion Checking in Modular Programs....Pages 392-406
Representation of Partial Knowledge and Query Answering in Locally Complete Databases....Pages 407-421
Sequential, Parallel, and Quantified Updates of First-Order Structures....Pages 422-436
Representing Defaults and Negative Information Without Negation-as-Failure....Pages 437-451
Constructing Camin-Sokal Phylogenies Via Answer Set Programming....Pages 452-466
Automata for Positive Core XPath Queries on Compressed Documents....Pages 467-481
Boolean Rings for Intersection-Based Satisfiability....Pages 482-496
Theory Instantiation....Pages 497-511
Splitting on Demand in SAT Modulo Theories....Pages 512-526
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis....Pages 527-541
Automatic Combinability of Rewriting-Based Satisfiability Procedures....Pages 542-556
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$ ....Pages 557-571
Lemma Learning in the Model Evolution Calculus....Pages 572-586
Back Matter....Pages -