ACM Transactions on Computational Logic (TOCL)

Accepted Papers

• A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement Sharon Shoham and Orna Grumberg (Electronic Appendix)
• A Formally Verified Proof of the Prime Number Theorem Jeremy Avigad, Kevin Donnelly, David Gray and Paul Raff
• Polymorphic Type Inference for the Named Nested Relational Calculus Jan Van den Bussche and Stijn Vansummeren
• Predicate Abstraction with Indexed Predicates Shuvendu Lahiri and Randal Bryant
• Verifying Nondeterministic Probabilistic Channel Systems Against Omega-Regular Linear-Time Properties Christel Baier, Nathalie Bertrand and Philippe Schnoebelen
• A Concrete Framework for Environment Machines Malgorzata Biernacka and Olivier Danvy
• Outlier Detection by Logic Programming Fabrizio Angiulli, Gianluigi Greco and Luigi Palopoli (Electronic Appendix)

• A Comprehensive Combination Framework Silvio Ghilardi, Enrica Nicolini and Daniele Zucchelli
• Coordination in Answer Set Programming Chiaki Sakama and Katsumi Inoue
• Alternating Timed Automata Slawomir Lasota and Igor Walukiewicz
• Bounds on the Automata Size for Presburger Arithmetic Felix Klaedtke
• Durations and Parametric Model-Checking in Timed Automata Véronique Bruyère, Emmanuel Dall'Oli and Jean-Francois Raskin
• First-order Complete and Computationally Complete Query Languages for Spatio-Temporal Databases Sofie Haesevoets, Floris Geerts and Bart Kuijpers
• A Logic of Non-Monotone Inductive Definitions Marc Denecker and Eugenia Ternovska

• A Uniform Approach to Constraint-solving for Lists, Multisets, Compact Lists, and Sets Agostino Dovier, Carla Piazza, and Gianfranco Rossi
• Foundational Certified Code in the Twelf Metalogical Framework Karl Crary and Susmit Sarkar
• Inferring Non-Suspension Conditions for Logic Programs with Dynamic Scheduling Samir Genaim and Andy King
• Program Termination and Well Partial Orderings Andreas Blass and Yuri Gurevich
• Abstract State Machines Capture Parallel Algorithms: Correction and Extension Andreas Blass and Yuri Gurevich
• What Causes a System to Satisfy a Specification? Hana Chockler, Joseph Y. Halpern and Orna Kupferman
• Proof Search in Hajek's Basic Logic Simone Bova and Franco Montagna
• Conjunctive Query Containment and Answering under Description Logics Constraints Diego Calvanese, Giuseppe De Giacomo and Maurizio Lenzerini
• Contextual Modal Type Theory Aleksandar Nanevski, Frank Pfenning and Brigitte Pientka

• Complexity Results for Security Protocols with Diffie-Hellman Exponentiation and Commuting Public Key Encryption Yannick Chevalier, Ralf Kuesters, Michael Rusinowitch and Mathieu Turuani
• Undecidability of the Unification and Admissibility Problems for Modal and Description Logics Frank Wolter and Michael Zakharyaschev
• Open Answer Set Programming with Guarded Programs Stijn Heymans, Davy Van Nieuwenborgh and Dirk Vermeir
• Reasoning with Recursive Loops under the PLP Framework Yi-Dong Shen
• Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying Helmut Seidl and Kumar Neeraj Verma
• Verifiable Agent Interaction in Abductive Logic Programming: the SCIFF Framework Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello and Paolo Torroni

• Specifying Norm-Governed Computational Societies Alexander Artikis, Marek Sergot and Jeremy Pitt
• Arithmetic Complexity Lou van den Dries and Yiannis N. Moschovakis
• Certainty Closure: Reliable Constraint Reasoning with Incomplete or Erroneous Data Neil Yorke-Smith and Carmen Gervet
• New Results on Rewrite-based Satisfiability Procedures Alessandro Armando, Maria Paola Bonacina, Silvio Ranise and Stephan Schulz
• Reasoning about Actions with Sensing under Qualitative and Probabilistic Uncertainty Luca Iocchi, Thomas Lukasiewicz, Daniele Nardi and Riccardo Rosati
• A Finite Equational Base for CCS with Left Merge and Communication Merge Luca Aceto, Wan Fokkink, Anna Ingolfsdottir and Bas Luttik
• Logical Characterization of the Counting Hierarchy Juha Kontinen
• The Geometry of Linear Higher-Order Recursion Ugo Dal Lago
• Probabilistic Bisimulation as a Congruence Ruggero Lanotte and Simone Tini
• Extending the LOOP language with Higher-Order Procedural Variables T. Crolard, E. Polonowski and P. Valarcher
• Termination of Rewriting Strategies: a Generic Approach Isabelle Gnaedig and Hélène Kirchner (Electronic Appendix)
• A Compositional Semantics for CHR Maurizio Gabrielli and Maria Chiara Meo
• Proofs, Tests and Continuation Passing Style Stefano Guerrini and Andrea Masini
• A Flow Calculus of mwp-Bounds for Complexity Analysis Neil D. Jones and Lars Kristiansen
• PSPACE Bounds for Rank-1 Modal Logics Lutz Schröder and Dirk Pattinson
• Context Semantics, Linear Logic and Computational Complexity Ugo Dal Lago
• On the Proof Complexity of Deep Inference Paola Bruscoli and Alessio Guglielmi
• A New Function Algebra of EXPTIME Functions by Safe Nested Recursion Toshiyasu Arai and Naohi Eguchi
• Checking Timed Büchi Automata Emptiness on Simulation Graphs Stavros Tripakis
• LTL with the Freeze Quantifier and Register Automata Stéphane Demri and Ranko Lazic
• Generalizing Consistency and other Constraint Properties to Quantified Constraints Lucas Bordeaux, Marco Cadoli and Toni Mancini (Electronic Appendix)
• Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning Laura Giordano, Valentina Gliozzi, Nicola Olivetti, and Gian Luca Pozzato (Electronic Appendix)
• An Algebra of Quantum Processes Mingsheng Ying, Yuan Feng, Runyao Duan and Zhengfeng Ji (Electronic Appendix)
• Differential Recursion Akitoshi Kawamura
• Resource Control Graphs Jean-Yves Moyen
• Simultaneous Checking of Completeness and Ground Confluence for Algebraic Specifications Adel Bouhoula
• Tableau Calculus for Preference-Based Conditional Logics: CE and Its Extensions Laura Giordano, Valentina Gliozzi, Nicola Olivetti and Camilla Schwind
• Sup-Interpretations, a Semantic Method for Static Analysis of Program Resources Jean-Yves Marion and Romain Péchoux