13. LPAR 2006: Phnom Penh, Cambodia

• Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio:
  Higher-Order Termination: From Kruskal to Computability. 1-14
  
• Sébastien Limet, Pierre Pillot:
  Deciding Satisfiability of Positive Second Order Joinability Formulae. 15-29
  
• Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, René Thiemann, Jürgen Giesl:
  SAT Solving for Argument Filterings. 30-44
  
• Stephan Falke, Deepak Kapur:
  Inductive Decidability Using Implicit Induction. 45-59
  
• Germain Faure:
  Matching Modulo Superdevelopments Application to Second-Order Matching. 60-74
  
• Georg Moser:
  Derivational Complexity of Knuth-Bendix Orders Revisited. 75-89
  
• Guillaume Bonfante, Jean-Yves Marion, Romain Péchoux:
  A Characterization of Alternating Log Time by First Order Functional Programs. 90-104
  
• Frédéric Blanqui, Colin Riba:
  Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. 105-119
  
• Kentaro Kikuchi:
  On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus. 120-134
  
• Agata Ciabattoni, Kazushige Terui:
  Modular Cut-Elimination: Finding Proofs or Counterexamples. 135-149
  
• Carsten Schürmann, Mark-Oliver Stehr:
  An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. 150-166
  
• Richard Bonichon, Olivier Hermant:
  A Semantic Completeness Proof for TaMeD. 167-181
  
• Martin Giese:
  Saturation Up to Redundancy for Tableau and Sequent Calculi. 182-196
  
• Laura Bozzelli, Régis Gascon:
  Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints. 197-211
  
• Christian G. Fermüller, Robert Kosik:
  Combining Supervaluation and Degree Based Reasoning Under Vagueness. 212-226
  
• Boris Motik, Ulrike Sattler:
  A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes. 227-241
  
• Alwen Tiu:
  A Local System for Intuitionistic Logic. 242-256
  
• Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
  CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. 257-271
  
• Ozan Kahramanogullari:
  Reducing Nondeterminism in the Calculus of Structures. 272-286
  
• Hendrik Decker, Davide Martinenghi:
  A Relaxed Approach to Integrity and Inconsistency in Databases. 287-301
  
• Orna Kupferman, Yoad Lustig, Moshe Y. Vardi:
  On Locally Checkable Properties. 302-316
  
• Véronique Cortier, Eugen Zalinescu:
  Deciding Key Cycles for Security Protocols. 317-331
  
• Tobias Gedell, Reiner Hähnle:
  Automating Verification of Loops by Parallelization. 332-346
  
• Christel Baier, Nathalie Bertrand, Ph. Schnoebelen:
  On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems. 347-361
  
• John Matthews, J. Strother Moore, Sandip Ray, Daron Vroon:
  Verification Condition Generation Via Theorem Proving. 362-376
  
• Elvira Albert, Puri Arenas, Germán Puebla:
  An Incremental Approach to Abstraction-Carrying Code. 377-391
  
• Pawel Pietrzak, Jesús Correas, Germán Puebla, Manuel V. Hermenegildo:
  Context-Sensitive Multivariant Assertion Checking in Modular Programs. 392-406
  
• Alvaro Cortés-Calabuig, Marc Denecker, Ofer Arieli, Maurice Bruynooghe:
  Representation of Partial Knowledge and Query Answering in Locally Complete Databases. 407-421
  
• Philipp Rümmer:
  Sequential, Parallel, and Quantified Updates of First-Order Structures. 422-436
  
• Pablo R. Fillottrani, Guillermo Ricardo Simari:
  Representing Defaults and Negative Information Without Negation-as-Failure. 437-451
  
• Jonathan Kavanagh, David G. Mitchell, Eugenia Ternovska, Ján Manuch, Xiaohong Zhao, Arvind Gupta:
  Constructing Camin-Sokal Phylogenies Via Answer Set Programming. 452-466
  
• Barbara Fila, Siva Anantharaman:
  Automata for Positive Core XPath Queries on Compressed Documents. 467-481
  
• Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang, Daher Kaiss:
  Boolean Rings for Intersection-Based Satisfiability. 482-496
  
• Harald Ganzinger, Konstantin Korovin:
  Theory Instantiation. 497-511
  
• Clark Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
  Splitting on Demand in SAT Modulo Theories. 512-526
  
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani:
  Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. 527-541
  
• Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran:
  Automatic Combinability of Rewriting-Based Satisfiability Procedures. 542-556
  
• Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani:
  To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). 557-571
  
• Peter Baumgartner, Alexander Fuchs, Cesare Tinelli:
  Lemma Learning in the Model Evolution Calculus. 572-586