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