Accepted Papers LPAR 2006
- Carsten Schürmann and Mark-Oliver Stehr.
An Executable Formalization of the HOL/Nuprl Connection in
the Metalogical Framework Twelf
- Alvaro Cortes-Calabuig, Marc Denecker, Ofer Arieli and
Maurice Bruynooghe.
Representation of Partial Knowledge and Query Answering in
Locally Complete Databases
- Orna Kupferman, Yoad Lustig and Moshe Vardi.
On Locally Checkable Properties
- Kentaro Kikuchi.
On a Local-Step Cut-Elimination Procedure for the
Intuitionistic Sequent Calculus
- Guillaume Bonfante, Marion Jean-Yves and Romain Péchoux.
Characterization of Alogtime by first order functional
programs
- Sébastien Limet and Pierre Pillot.
Deciding Satisfiability of Positive Second Order Joinability
Formulae
- Peter Baumgartner, Alexander Fuchs and Cesare Tinelli.
Lemma Learning in the Model Evolution Calculus
- Philipp Rümmer.
Sequential, Parallel and Quantified Updates of First-Order
Structures
- Gilles Barthe, Benjamin Gregoire and Fernando Pastawski.
Type-based termination of recursive definitions in the
Calculus of Inductive Constructions
- Cortier Veronique and Eugen Zalinescu.
Deciding key cycles for security protocols
- Tobias Gedell and Reiner Hähnle.
Automating Verification of Loops by Parallelization
- Boris Motik and Ulrike Sattler.
A Comparison of Techniques for Querying Large Description
Logic ABoxes
- Agata Ciabattoni and Kazushige Terui.
Modular Cut-Elimination: Finding Proofs or Counterexamples
- Regis Gascon and Laura Bozzelli.
Branching Time Temporal Logic Extended with Presburger
Constraints
- Christel Baier, Nathalie Bertrand and Philippe
Schnoebelen.
On computing fixpoints in well-structured regular model
checking, with applications to lossy channel systems
- Barbara Fila and Siva Anantharaman.
Automata for Positive Core XPath Queries on Compressed
Documents
- Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon, René
Thiemann and Jürgen Giesl.
SAT Solving for Argument Filterings
- Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen,
Alberto Griggio and Roberto Sebastiani.
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability
Modulo Theories: a Comparative Analysis
- Hendrik Decker and Davide Martinenghi.
A Relaxed Approach to Integrity and Inconsistency in Databases
- John Matthews, J Moore, Sandip Ray and Daron Vroon.
Verification Condition Generation via Theorem Proving
- Richard Bonichon and Olivier Hermant.
A Semantic Completeness Proof for Tableaux Modulo
- Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen,
Alberto Griggio, Alessandro Santuari and Roberto
Sebastiani.
To Ackermann-ize or not to Ackermann-ize? On Efficiently
Handling Uninterpreted Function Symbols in SMT(EUF U T)
- Stephan Falke and Deepak Kapur.
Inductive Decidability using Implicit Induction
- Hélène Kirchner, Silvio Ranise, Christophe Ringeissen and
Duc-Khanh Tran.
Automatic Combinability of Rewriting Based Satisfiability
Procedures
- Martin Giese.
Saturation up to Redundancy for Tableau and Sequent Calculi
- Harald Ganzinger and Konstantin Korovin.
Theory Instantiation
- Ozan Kahramanogullari.
Reducing Nondeterminism in the Calculus of Structures
- Jonathan Kavanagh, David Mitchell, Eugenia Ternovska, Jan
Manuch, Xiaohong Zhao and Arvind Gupta.
Constructing Camin-Sokal Phylogenies Via Answer Set
Programming
- Clark Barrett, Robert Nieuwenhuis, Albert Oliveras and
Cesare Tinelli.
Splitting on Demand in Satisfiability Modulo Theories
- Germain Faure.
Matching modulo superdevelopments. Application to second-order
matching.
- Pablo Fillottrani and Guillermo Simari.
Representing defaults and negative information without
negation-as-failure
- Alwen Tiu.
A Local System for Intuitionistic Logic
- Christian Fermüller and Robert Kosik.
Combining supervaluation and degree based reasoning under
vagueness
- Elvira Albert, Puri Arenas and German Puebla.
An Incremental Approach to Abstraction-Carrying Code
- Pawel Pietrzak, Jesus Correas, German Puebla and Manuel
Hermenegildo.
Context-Sensitive Multivariant Assertion Checking in Modular
Programs
- Nachum Dershowitz, Jieh Hsiang, Guan-Shieng Huang and Daher
Kaiss.
Boolean Rings for Intersection-Based Satisfiability
- Georg Moser.
Derivational Complexity of Knuth-Bendix Orders revisited
- Frederic Blanqui and Colin Riba.
Combining typing and size constraints for checking the
termination of higher-order conditional rewrite systems
Last modified: Mon Jul 10 13:44:54 CEST 2006