Front matter
1-18
Improving On-Demand Strategy Annotations
M. Alpuente, S. Escobar, B. Gramlich and S. Lucas
19-35
First-Order Logic as a Constraint Programming Language
K. R. Apt and C. F. M. Vermeulen
36-52
Maintenance of Formal Software Developments by Stratified Verification
Serge Autexier and Dieter Hutter
53-67
A Note on Universal Measures for Weak Implicit Computational Complexity
Arnold Beckmann
68-85
Extending Compositional Message Sequence Graphs
Benedikt Bollig, Martin Leucker and Philipp Lucas
86-101
Searching for Invariants Using Temporal Resolution
James Brotherston, Anatoli Degtyarev, Michael Fisher and Alexei Lisitsa
102-114
Proof Planning for Feature Interactions: A Preliminary Report
Claudio Castellini and Alan Smaill
115-129
An Extension of BDICTL with Functional Dependencies and Components
Mehdi Dastani and Leendert van der Torre
130-144
Binding Logic: Proofs and Models
Gilles Dowek, Thérèse Hardin and Claude Kirchner
145-159
Directed Automated Theorem Proving
Stefan Edelkamp and Peter Leven
160-174
A Framework for Splitting BDI Agents
Xiaocong Fan and John Yen
175-189
On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics
Mauro Ferrari, Camillo Fiorentini and Guido Fiorino
190-201
Using BDDs with Combinations of Theories
Pascal Fontaine and E. Pascal Gribomont
202-215
On Expressive Description Logics with Composition of Roles in Number Restrictions
Fabio Grandi
216-230
Query Optimization of Disjunctive Databases with Constraints through Binding Propagation
Gianluigi Greco, Sergio Greco, Irina Trubtsyna and Ester Zumpano
231-246
A Non-commutative Extension of MELL
Alessio Guglielmi and Lutz Straßburger
247-261
Procedural Semantics for Fuzzy Disjunctive Programs
Dušan Guller
262-277
Pushdown Specifications
Orna Kupferman, Nir Piterman and Moshe Y. Vardi
278-291
Theorem Proving with Sequence Variables and Flexible Arity Symbols
Temur Kutsia
292-310
Games, Probability, and the Quantitative μ-Calculus
qMμ
A. K. McIver and C. C. Morgan
311-326
Parallelism and Tree Regular Constraints
Joachim Niehren and Mateu Villaret
327-336
Gödel Logics and Cantor-Bendixon Analysis
Norbert Preining
337-351
A Semantics for Proof Plans with Applications to Interactive Proof Planning
Julian Richardson
352-366
An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction
José Espírito Santo
367-387
Proof Development with ΩMEGA: √2 Is Irrational
J. Siekmann, C. Benzmüller, A. Fiedler, A. Meier and M. Pollet
388-402
A Local System for Linear Logic
Lutz Straβburger
403-417
Investigating Type-Certifying Compilation with Isabelle
Martin Strecker
418-434
Automating Type Soundness Proofs via Decision Procedures and Guided Reductions
Don Syme and Andrew D. Gordon
435-449
Abox Satisfiability Reduced to Terminological Reasoning in Expressive Description Logics
Sergio Tessaris and Ian Horrocks
450-463
Fuzzy Prolog: A Simple General Implementation Using (
R
)
Claudio Vaucheret, Sergio Guadarrama and Susana Muñoz
Back matter