Logic for Programming, Artificial Intelligence, and Reasoning

Front Matter

From Hilbert’s Program to a Logic Toolbox

• Johann A. Makowsky

On the Notion of Vacuous Truth

• Marko Samer, Helmut Veith

Whatever Happened to Deductive Question Answering?

• Richard Waldinger

Decidable Fragments of Many-Sorted Logic

• Aharon Abadi, Alexander Rabinovich, Mooly Sagiv

One-Pass Tableaux for Computation Tree Logic

• Pietro Abate, Rajeev Goré, Florian Widmann

Extending a Resolution Prover for Inequalities on Elementary Functions

• Behzad Akbarpour, Lawrence C. Paulson

Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic

• Roland Axelsson, Martin Lange

Monadic Fragments of Gödel Logics: Decidability and Undecidability Results

• Matthias Baaz, Agata Ciabattoni, Christian G. Fermüller

Least and Greatest Fixed Points in Linear Logic

• David Baelde, Dale Miller

The Semantics of Consistency and Trust in Peer Data Exchange Systems

• Leopoldo Bertossi, Loreto Bravo

Completeness and Decidability in Sequence Logic

• Marc Bezem, Tore Langholm, Michał Walicki

HORPO with Computability Closure: A Reconstruction

• Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

• Richard Bonichon, David Delahaye, Damien Doligez

Matching in Hybrid Terminologies

• Sebastian Brandt

Verifying Cryptographic Protocols with Subterms Constraints

• Yannick Chevalier, Denis Lugiez, Michaël Rusinowitch

Deciding Knowledge in Security Protocols for Monoidal Equational Theories

• Véronique Cortier, Stéphanie Delaune

Mechanized Verification of CPS Transformations

• Zaynah Dargaye, Xavier Leroy

Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap

• Francien Dechesne, MohammadReza Mousavi, Simona Orzan

Protocol Verification Via Rigid/Flexible Resolution

• Stépphanie Delaune, Hai Lin, Christopher Lynch