


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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














