


default search action
13th LPAR 2006: Phnom Penh, Cambodia
- Miki Hermann, Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings. Lecture Notes in Computer Science 4246, Springer 2006, ISBN 3-540-48281-4 - 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, Philippe 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 W. 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.