Table of contents for issues of ACM Transactions on Computational Logic

Last update: Fri Mar 2 12:31:08 MST 2018                Valid HTML 3.2!

Volume 1, Number 1, July, 2000
Volume 1, Number 2, 2000
Volume 2, Number 1, 2001
Volume 2, Number 2, 2001
Volume 2, Number 3, 2001
Volume 2, Number 4, October, 2001
Volume 3, Number 1, January, 2002
Volume 3, Number 2, April, 2002
Volume 3, Number 3, July, 2002
Volume 3, Number 4, October, 2002
Volume 4, Number 1, January, 2003
Volume 4, Number 2, April, 2003
Volume 4, Number 3, July, 2003
Volume 4, Number 4, October, 2003
Volume 5, Number 1, January, 2004
Volume 5, Number 2, April, 2004
Volume 5, Number 3, July, 2004
Volume 5, Number 4, October, 2004
Volume 6, Number 1, January, 2005
Volume 6, Number 2, April, 2005
Volume 6, Number 3, July, 2005
Volume 6, Number 4, October, 2005
Volume 7, Number 1, January, 2006
Volume 7, Number 2, April, 2006
Volume 7, Number 3, July, 2006
Volume 7, Number 4, October, 2006
Volume 8, Number 1, January, 2007
Volume 8, Number 2, April, 2007
Volume 8, Number 3, July, 2007
Volume 8, Number 4, August, 2007
Volume 9, Number 1, December, 2007
Volume 9, Number 2, March, 2008
Volume 9, Number 3, June, 2008
Volume 9, Number 4, August, 2008
Volume 10, Number 1, January, 2009
Volume 10, Number 2, February, 2009
Volume 10, Number 3, April, 2009
Volume 10, Number 4, August, 2009
Volume 11, Number 1, October, 2009
Volume 11, Number 2, January, 2010
Volume 11, Number 3, May, 2010
Volume 11, Number 4, July, 2010
Volume 12, Number 1, October, 2010
Volume 12, Number 2, January, 2011
Volume 12, Number 3, May, 2011
Volume 12, Number 4, July, 2011
Volume 13, Number 1, January, 2012
Volume 13, Number 2, April, 2012
Volume 13, Number 3, August, 2012
Volume 13, Number 4, October, 2012
Volume 14, Number 1, February, 2013
Volume 14, Number 2, June, 2013
Volume 14, Number 3, August, 2013
Volume 14, Number 4, November, 2013
Volume 15, Number 1, February, 2014
Volume 15, Number 2, April, 2014
Volume 15, Number 3, September, 2014
Volume 15, Number 4, September, 2014
Volume 16, Number 1, March, 2015
Volume 16, Number 2, February, 2015
Volume 16, Number 3, July, 2015
Volume 16, Number 4, November, 2015
Volume 17, Number 1, December, 2015
Volume 17, Number 2, March, 2016
Volume 17, Number 3, July, 2016
Volume 17, Number 4, November, 2016
Volume 18, Number 1, April, 2017
Volume 18, Number 2, June, 2017
Volume 18, Number 3, August, 2017
Volume 18, Number 4, December, 2017
Volume 19, Number 1, February, 2018


ACM Transactions on Computational Logic
Volume 1, Number 1, July, 2000

            Lawrence C. Paulson   Mechanizing UNITY in Isabelle  . . . . . 3--32
                  Leonid Libkin   Logics with counting and local
                                  properties . . . . . . . . . . . . . . . 33--59
                   Dexter Kozen   On Hoare logic and Kleene algebra with
                                  tests  . . . . . . . . . . . . . . . . . 60--76
                  Yuri Gurevich   Sequential abstract-state machines
                                  capture sequential algorithms  . . . . . 77--111
               Martin Grohe and   
              Thomas Schwentick   Locality of order-invariant first-order
                                  formulas . . . . . . . . . . . . . . . . 112--130
               Paolo Liberatore   Compilability and compact
                                  representations of revision of Horn
                                  knowledge bases  . . . . . . . . . . . . 131--161
                 Adnan Aziz and   
               Kumud Sanwal and   
             Vigyan Singhal and   
                 Robert Brayton   Model-checking continuous-time Markov
                                  chains . . . . . . . . . . . . . . . . . 162--170
                Ernie Cohen and   
                   Dexter Kozen   A note on the complexity of
                                  propositional Hoare logic  . . . . . . . 171--174

ACM Transactions on Computational Logic
Volume 1, Number 2, 2000

               Nir Friedman and   
          Joseph Y. Halpern and   
                  Daphne Koller   First-order conditional logic for
                                  default reasoning revisited  . . . . . . 175--207
            Jürgen Dix and   
                Mirco Nanni and   
             V. S. Subrahmanian   Probabilistic agent programs . . . . . . 208--246
        Alessio R. Lomuscio and   
         Ron van der Meyden and   
                      Mark Ryan   Knowledge in multiagent systems: initial
                                  configurations and broadcast . . . . . . 247--284
      Pascal van Hentenryck and   
             Laurent Perron and   
     Jean-François Puget   Search and strategies in OPL . . . . . . 285--320


ACM Transactions on Computational Logic
Volume 2, Number 1, 2001

              Andreas Blass and   
                  Yuri Gurevich   Inadequacy of computable loop invariants 1--11
             Michael Fisher and   
                Clare Dixon and   
                    Martin Peim   Clausal temporal resolution  . . . . . . 12--56
            Sofie Verbaeten and   
           Danny De Schreye and   
           Konstantinos Sagonas   Termination proofs for logic programs
                                  with tabling . . . . . . . . . . . . . . 57--92
           Randal E. Bryant and   
              Steven German and   
              Miroslav N. Velev   Processor verification using efficient
                                  reductions of the logic of uninterpreted
                                  functions to propositional logic . . . . 93--134
                  Leonid Libkin   Logics capturing local properties  . . . 135--153

ACM Transactions on Computational Logic
Volume 2, Number 2, 2001

             Tatiana Rybina and   
                Andrei Voronkov   A decision procedure for term algebras
                                  with queues  . . . . . . . . . . . . . . 155--181
                Andrei Voronkov   How to optimize proof-search in modal
                                  logics: new methods of proving
                                  redundancy criteria for sequent calculi  182--215
           Joost Engelfriet and   
          Hendrik Jan Hoogeboom   MSO definable string transductions and
                                  two-way finite-state transducers . . . . 216--254
          Grigoris Antoniou and   
           David Billington and   
          Guido Governatori and   
               Michael J. Maher   Representation results for defeasible
                                  logic  . . . . . . . . . . . . . . . . . 255--287

ACM Transactions on Computational Logic
Volume 2, Number 3, 2001

             Thomas Lukasiewicz   Probabilistic logic programming with
                                  conditional constraints  . . . . . . . . 289--339
                   Uwe Egly and   
                   Hans Tompits   Proof-complexity results for
                                  nonmonotonic reasoning . . . . . . . . . 340--387
                Rajeev Alur and   
            Kousha Etessami and   
         Salvatore La Torre and   
                    Doron Peled   Parametric temporal logic for ``model
                                  measuring''  . . . . . . . . . . . . . . 388--407
             Orna Kupferman and   
                 Moshe Y. Vardi   Weak alternating automata are not that
                                  weak . . . . . . . . . . . . . . . . . . 408--429

ACM Transactions on Computational Logic
Volume 2, Number 4, October, 2001

           Krzysztof R. Apt and   
           Antonis C. Kakas and   
                   Fariba Sadri   Editorial  . . . . . . . . . . . . . . . 431--431
                     Ray Reiter   On knowledge-based programming with
                                  sensing in the situation calculus  . . . 433--457
              Nada Lavra\vc and   
                 Peter A. Flach   An extended transformation approach to
                                  inductive logic programming  . . . . . . 458--494
        Giuseppe De Giacomo and   
         Hector J. Levesque and   
       Sebastian Sardiña   Incremental execution of guarded
                                  theories . . . . . . . . . . . . . . . . 495--525
         Vladimir Lifschitz and   
               David Pearce and   
        Agustín Valverde   Strongly equivalent logic programs . . . 526--541
     Luigia Carlucci Aiello and   
                 Fabio Massacci   Verifying security protocols as planning
                                  in logic programming . . . . . . . . . . 542--580
                   Marek Sergot   A computational theory of normative
                                  positions  . . . . . . . . . . . . . . . 581--622
              Marc Denecker and   
         Maurice Bruynooghe and   
                   Victor Marek   Logic programming revisited: Logic
                                  programs as inductive definitions  . . . 623--654


ACM Transactions on Computational Logic
Volume 3, Number 1, January, 2002

        Gerald Lüttgen and   
                Michael Mendler   The intuitionism behind Statecharts
                                  steps  . . . . . . . . . . . . . . . . . 1--41
              Georg Gottlob and   
          Erich Grädel and   
                   Helmut Veith   Datalog LITE: a deductive query language
                                  with linear time model checking  . . . . 42--79
        Raymond C. McDowell and   
                 Dale A. Miller   Reasoning with higher-order abstract
                                  syntax in a logical framework  . . . . . 80--136
             Andrea Asperti and   
                   Luca Roversi   Intuitionistic Light Affine Logic  . . . 137--175

ACM Transactions on Computational Logic
Volume 3, Number 2, April, 2002

        Francesco M. Donini and   
              Daniele Nardi and   
                Riccardo Rosati   Description logics of minimal knowledge
                                  and negation as failure  . . . . . . . . 177--225
       Piero Andrea Bonatti and   
                Nicola Olivetti   Sequent calculi for propositional
                                  nonmonotonic logics  . . . . . . . . . . 226--278
               J. V. Tucker and   
                   J. I. Zucker   Abstract computability and algebraic
                                  specification  . . . . . . . . . . . . . 279--333

ACM Transactions on Computational Logic
Volume 3, Number 3, July, 2002

        Martín Abadi and   
              Leonid Libkin and   
                 Frank Pfenning   Editorial  . . . . . . . . . . . . . . . 335--335
               Martin Grohe and   
                   Luc Segoufin   On first-order topological queries . . . 336--358
              Vincent Danos and   
              Russell S. Harmer   Probabilistic game semantics . . . . . . 359--382
               Klaus Aehlig and   
          Helmut Schwichtenberg   A syntactical analysis of
                                  non-size-increasing polynomial time
                                  computation  . . . . . . . . . . . . . . 383--401
             Samuel R. Buss and   
                Bruce M. Kapron   Resource-bounded continuity and
                                  sequentiality for type-two functionals   402--417
          Erich Grädel and   
               Colin Hirsch and   
                    Martin Otto   Back and forth between guarded and modal
                                  logics . . . . . . . . . . . . . . . . . 418--463

ACM Transactions on Computational Logic
Volume 3, Number 4, October, 2002

             Mario Bravetti and   
               Roberto Gorrieri   Deciding and axiomatizing weak ST
                                  bisimulation for a process algebra with
                                  recursion and action refinement  . . . . 465--520
               Robert Givan and   
               David Mcallester   Polynomial-time computation via local
                                  inference relations  . . . . . . . . . . 521--541
           Michael Kaminski and   
                        Guy Rey   Revisiting quantification in
                                  autoepistemic logic  . . . . . . . . . . 542--561
               Viviana Bono and   
           Michele Bugliesi and   
                   Silvia Crafa   Typed interpretations of extensible
                                  objects  . . . . . . . . . . . . . . . . 562--603
           Randal E. Bryant and   
              Miroslav N. Velev   Boolean satisfiability with transitivity
                                  constraints  . . . . . . . . . . . . . . 604--627


ACM Transactions on Computational Logic
Volume 4, Number 1, January, 2003

              Philip Wadler and   
                 Peter Thiemann   The marriage of effects and monads . . . 1--32
               Hubert Comon and   
          Paliath Narendran and   
         Robert Nieuwenhuis and   
            Michael Rusinowitch   Deciding the confluence of ordered term
                                  rewrite systems  . . . . . . . . . . . . 33--55
              James Harland and   
                      David Pym   Resource-distribution via Boolean
                                  constraints  . . . . . . . . . . . . . . 56--90
              Zbigniew Lonc and   
        Miroslaw Truszczy\'nski   Fixed-parameter complexity of semantics
                                  for logic programs . . . . . . . . . . . 91--119
      M. Dezani-Ciancaglini and   
                 F. Honsell and   
                      F. Alessi   A complete characterization of complete
                                  intersection-type preorders  . . . . . . 120--147

ACM Transactions on Computational Logic
Volume 4, Number 2, April, 2003

          Fabrizio Angiulli and   
  Rachel Ben-Eliyahu-Zohary and   
       Giovambattista Ianni and   
                 Luigi Palopoli   Computational properties of metaquerying
                                  problems . . . . . . . . . . . . . . . . 149--180
               Doron Bustan and   
                  Orna Grumberg   Simulation-based minimization  . . . . . 181--206
               Fred Mesnard and   
             Salvatore Ruggieri   On proving left termination of
                                  constraint logic programs  . . . . . . . 207--259
                Oliver Kutz and   
               Frank Wolter and   
               Holger Sturm and   
           Nobu-Yuki Suzuki and   
          Michael Zakharyaschev   Logics of metric spaces  . . . . . . . . 260--294

ACM Transactions on Computational Logic
Volume 4, Number 3, July, 2003

          Erich Grädel and   
          Joseph Y. Halpern and   
          Radha Jaghadeesan and   
                 Adolfo Piperno   LICS 2001 special issue  . . . . . . . . 295--295
                Micah Adler and   
                  Neil Immerman   An $n!$ lower bound on formula size  . . 296--314
                  Noga Alon and   
                  Tova Milo and   
                Frank Neven and   
                  Dan Suciu and   
                   Victor Vianu   Typechecking XML views of relational
                                  databases  . . . . . . . . . . . . . . . 315--354
               Dexter Kozen and   
                   Jerzy Tiuryn   Substructural logic and partial
                                  correctness  . . . . . . . . . . . . . . 355--378
               Antonino Salibra   Topological incompleteness and order
                                  incompleteness of the lambda calculus    379--401
                  Jeremy Avigad   Eliminating definitions and Skolem
                                  functions in first-order logic . . . . . 402--415

ACM Transactions on Computational Logic
Volume 4, Number 4, October, 2003

               Yi-Dong Shen and   
               Jia-Huai You and   
                Li-Yan Yuan and   
          Samuel S. P. Shen and   
                     Qiang Yang   A dynamic approach to characterizing
                                  termination of general logic programs    417--430
                  Leonid Libkin   Variable independence for first-order
                                  definable constraints  . . . . . . . . . 431--451
              Jeremy Bryans and   
              Howard Bowman and   
                   John Derrick   Model checking stochastic automata . . . 452--492
         Alberto Momigliano and   
                 Frank Pfenning   Higher-order pattern complement and the
                                  strict $\lambda$-calculus  . . . . . . . 493--529
              Peter Buneman and   
                 Wenfei Fan and   
                Scott Weinstein   Interaction between path and type
                                  constraints  . . . . . . . . . . . . . . 530--577
              Andreas Blass and   
                  Yuri Gurevich   Abstract state machines capture parallel
                                  algorithms . . . . . . . . . . . . . . . 578--651


ACM Transactions on Computational Logic
Volume 5, Number 1, January, 2004

                Rajeev Alur and   
             Salvatore La Torre   Deterministic generators and games for
                                  Ltl fragments  . . . . . . . . . . . . . 1--25
                 Bard Bloom and   
                Wan Fokkink and   
            Rob J. Van Glabbeek   Precongruence formats for decorated
                                  trace semantics  . . . . . . . . . . . . 26--78
            Rocco De Nicola and   
                 Michele Loreti   A modal logic for mobile agents  . . . . 79--128
               Stefan Brass and   
            Jürgen Dix and   
         Teodor C. Przymusinski   Super logic programs . . . . . . . . . . 129--176

ACM Transactions on Computational Logic
Volume 5, Number 2, April, 2004

           Slim Abdennadher and   
             Christophe Rigotti   Automatic generation of rule-based
                                  constraint solvers over finite domains   177--205
               Thomas Eiter and   
             Wolfgang Faber and   
               Nicola Leone and   
             Gerald Pfeifer and   
                  Axel Polleres   A logic programming approach to
                                  knowledge-state planning: Semantics and
                                  complexity . . . . . . . . . . . . . . . 206--263
                Stefan Ratschan   Convergent approximate solving of
                                  first-order constraints by approximate
                                  quantifiers  . . . . . . . . . . . . . . 264--281
                 Anuj Dawar and   
          Erich Grädel and   
               Stephan Kreutzer   Inflationary fixed points in modal logic 282--315
                   K. Subramani   Optimal length tree-like resolution
                                  refutations for 2SAT formulas  . . . . . 316--320
              Guillem Godoy and   
         Robert Nieuwenhuis and   
                  Ashish Tiwari   Classes of term rewrite systems with
                                  polynomial confluence problems . . . . . 321--331
      Aleksandar Ignjatovic and   
                    Arun Sharma   Some applications of logic to
                                  feasibility in higher types  . . . . . . 332--350
             Laurent Michel and   
          Pascal Van Hentenryck   A decomposition-based implementation of
                                  search strategies  . . . . . . . . . . . 351--383

ACM Transactions on Computational Logic
Volume 5, Number 3, July, 2004

               Pawel Mielniczuk   Basic theory of feature trees  . . . . . 385--402
                Frank Neven and   
          Thomas Schwentick and   
                   Victor Vianu   Finite state machines for strings over
                                  infinite alphabets . . . . . . . . . . . 403--435
                 Marco Bernardo   Symbolic semantic rules for producing
                                  compact STGLAs from value passing
                                  process descriptions . . . . . . . . . . 436--469
             Annalisa Bossi and   
              Sandro Etalle and   
               Sabina Rossi and   
                Jan-Georg Smaus   Termination of simply moded logic
                                  programs with dynamic scheduling . . . . 470--507
                 Yann Loyer and   
           Nicolas Spyratos and   
                 Daniel Stamate   Hypothesis-based semantics of logic
                                  programs in multivalued logics . . . . . 508--527
                David Basin and   
              Manuel Clavel and   
           José Meseguer   Reflective metalogical frameworks  . . . 528--576

ACM Transactions on Computational Logic
Volume 5, Number 4, October, 2004

            David Griffioen and   
               Frits Vaandrager   A theory of normed simulations . . . . . 577--610
               J. V. Tucker and   
                   J. I. Zucker   Abstract versus concrete computation on
                                  metric partial algebras  . . . . . . . . 611--668
                   Carsten Lutz   NEXP TIME-complete description logics
                                  with concrete domains  . . . . . . . . . 669--705
           Frank S. De Boer and   
        Maurizio Gabbrielli and   
               Maria Chiara Meo   Proving correctness of timed concurrent
                                  constraint programs  . . . . . . . . . . 706--731
Frédéric Benhamou and   
Frédéric Goualard and   
Éric Languénou and   
                  Marc Christie   Interval constraint solving for camera
                                  control and motion planning  . . . . . . 732--767


ACM Transactions on Computational Logic
Volume 6, Number 1, January, 2005

        Thomas A. Henzinger and   
             Rupak Majumdar and   
    Jean-François Raskin   A classification of symbolic transition
                                  systems  . . . . . . . . . . . . . . . . 1--32
         Roberto Giacobazzi and   
          Francesco Ranzato and   
             Francesca Scozzari   Making abstract domains condensing . . . 33--60
              Robert Harper and   
                 Frank Pfenning   On equivalence and canonical forms in
                                  the LF type theory . . . . . . . . . . . 61--101
               Rakesh Verma and   
                Ara Hayrapetyan   A new decidability technique for ground
                                  term rewriting systems with applications 102--123
                Churn-Jung Liau   A modal logic framework for multi-agent
                                  belief fusion  . . . . . . . . . . . . . 124--174
               Wim H. Hesselink   Eternity variables to prove simulation
                                  of specifications  . . . . . . . . . . . 175--201

ACM Transactions on Computational Logic
Volume 6, Number 2, April, 2005

                  Chiaki Sakama   Induction from answer sets in
                                  nonmonotonic logic programs  . . . . . . 203--231
               Marco Cadoli and   
               Thomas Eiter and   
                  Georg Gottlob   Complexity of propositional nested
                                  circumscription and nested abnormality
                                  theories . . . . . . . . . . . . . . . . 232--272
             Orna Kupferman and   
                 Moshe Y. Vardi   From linear time to branching time . . . 273--294
                 Kewen Wang and   
                     Lizhu Zhou   Comparisons and computation of
                                  well-founded semantics for disjunctive
                                  logic programs . . . . . . . . . . . . . 295--327
                 Sara Cohen and   
             Yehoshua Sagiv and   
                    Werner Nutt   Equivalences among aggregate queries
                                  with negation  . . . . . . . . . . . . . 328--360
         Konstantin Korovin and   
                Andrei Voronkov   Knuth--Bendix constraint solving is
                                  NP-complete  . . . . . . . . . . . . . . 361--388
               Thomas Eiter and   
               Michael Fink and   
         Giuliana Sabbatini and   
                   Hans Tompits   Reasoning about evolving nonmonotonic
                                  knowledge bases  . . . . . . . . . . . . 389--440
         Panos Rondogiannis and   
               William W. Wadge   Minimum model semantics for logic
                                  programs with negation-as-failure  . . . 441--467
               Klaus Aehlig and   
                  Jan Johannsen   An elementary fragment of second-order
                                  lambda calculus  . . . . . . . . . . . . 468--480

ACM Transactions on Computational Logic
Volume 6, Number 3, July, 2005

                Foto Afrati and   
         Stavros Cosmadakis and   
      Eugénie Foustoucos   Datalog programs and their persistency
                                  numbers  . . . . . . . . . . . . . . . . 481--518
              Mauro Ferrari and   
         Camillo Fiorentini and   
                  Guido Fiorino   On the complexity of the disjunction
                                  property in intuitionistic and modal
                                  logics . . . . . . . . . . . . . . . . . 519--538
                  Matthew Stone   Disjunction and modular goal-directed
                                  proof search . . . . . . . . . . . . . . 539--577
            George Metcalfe and   
            Nicola Olivetti and   
                     Dov Gabbay   Sequent and hypersequent calculi for
                                  abelian and \Lukasiewicz logics  . . . . 578--613
           Bernard Boigelot and   
   Sébastien Jodogne and   
                  Pierre Wolper   An effective decision procedure for
                                  linear arithmetic over the integers and
                                  reals  . . . . . . . . . . . . . . . . . 614--633
             Nicole Schweikardt   Arithmetic, first-order logic, and
                                  counting quantifiers . . . . . . . . . . 634--671

ACM Transactions on Computational Logic
Volume 6, Number 4, October, 2005

               Krzysztof R. Apt   Editorial  . . . . . . . . . . . . . . . 673--673
            Phokion G. Kolaitis   LICS 2003 special issue  . . . . . . . . 674--674
       Bakhadyr Khoussainov and   
                Sasha Rubin and   
                  Frank Stephan   Automatic linear orders and trees  . . . 675--700
            Andrzej S. Murawski   About the undecidability of program
                                  equivalence in finitary languages with
                                  state  . . . . . . . . . . . . . . . . . 701--726
                 James F. Lynch   Convergence law for random graphs with
                                  specified degree sequence  . . . . . . . 727--748
                Dale Miller and   
                      Alwen Tiu   A proof theory for generic judgments . . 749--783
       Dominic J. D. Hughes and   
            Rob J. Van Glabbeek   Proof nets for unit-free
                                  multiplicative-additive linear logic . . 784--842


ACM Transactions on Computational Logic
Volume 7, Number 1, January, 2006

              Tomi Janhunen and   
         Ilkka Niemelä and   
             Dietmar Seipel and   
              Patrik Simons and   
                   Jia-Huai You   Unfolding partiality and disjunctions in
                                  stable model semantics . . . . . . . . . 1--37
               Deborah East and   
        Miroslaw Truszczy\'nski   Predicate-calculus-based logics for
                                  modeling and solving search problems . . 38--83
               Paolo Liberatore   Complexity results on DPLL and
                                  resolution . . . . . . . . . . . . . . . 84--107
          Anatoli Degtyarev and   
             Michael Fisher and   
                    Boris Konev   Monodic temporal resolution  . . . . . . 108--150
            Jürgen Dix and   
                Sarit Kraus and   
             V. S. Subrahmanian   Heterogeneous temporal probabilistic
                                  agents . . . . . . . . . . . . . . . . . 151--198

ACM Transactions on Computational Logic
Volume 7, Number 2, April, 2006

        Russell Impagliazzo and   
               Nathan Segerlind   Constant-depth Frege systems with
                                  counting axioms polynomially simulate
                                  Nullstellensatz refutations  . . . . . . 199--218
              Paolo Coppola and   
                 Simone Martini   Optimizing optimal reduction: a type
                                  inference algorithm for elementary
                                  affine logic . . . . . . . . . . . . . . 219--260
         Vladimir Lifschitz and   
             Alexander Razborov   Why are there so many loop formulas? . . 261--268
            Agostino Dovier and   
           Andrea Formisano and   
              Eugenio G. Omodeo   Decidability results for sets with atoms 269--301
               Giorgi Japaridze   Propositional computability logic I  . . 302--330
               Giorgi Japaridze   Propositional computability logic II . . 331--362
              Andreas Blass and   
                  Yuri Gurevich   Ordinary interactive small-step
                                  algorithms, I  . . . . . . . . . . . . . 363--419

ACM Transactions on Computational Logic
Volume 7, Number 3, July, 2006

                      Yan Zhang   Logic program-based updates  . . . . . . 421--472
        Andrzej S. Murawski and   
                 C.-H. Luke Ong   Fast verification of MLL proof nets via
                                  IMLL . . . . . . . . . . . . . . . . . . 473--498
               Nicola Leone and   
             Gerald Pfeifer and   
             Wolfgang Faber and   
               Thomas Eiter and   
              Georg Gottlob and   
               Simona Perri and   
            Francesco Scarcello   The DLV system for knowledge
                                  representation and reasoning . . . . . . 499--562
         Stefano Bistarelli and   
              Ugo Montanari and   
                Francesca Rossi   Soft concurrent constraint programming   563--589
            Arthur Charlesworth   Comprehending software correctness
                                  implies comprehending an
                                  intelligence-related limitation  . . . . 590--612

ACM Transactions on Computational Logic
Volume 7, Number 4, October, 2006

               Tran Cao Son and   
               Chitta Baral and   
                   Nam Tran and   
               Sheila Mcilraith   Domain-dependent knowledge in answer set
                                  planning . . . . . . . . . . . . . . . . 613--657
            Lawrence C. Paulson   Defining functions on equivalence
                                  classes  . . . . . . . . . . . . . . . . 658--675
       Christopher A. Stone and   
                  Robert Harper   Extensional equivalence and singleton
                                  types  . . . . . . . . . . . . . . . . . 676--722
                Stefan Ratschan   Efficient solving of quantified
                                  inequality constraints over the real
                                  numbers  . . . . . . . . . . . . . . . . 723--748
               Stephen Cook and   
                    Neil Thapen   The strength of replacement in weak
                                  arithmetic . . . . . . . . . . . . . . . 749--764
            Joost Vennekens and   
                David Gilis and   
                  Marc Denecker   Splitting an operator: Algebraic
                                  modularity results for logics with
                                  fixpoint semantics . . . . . . . . . . . 765--797
           Jules Desharnais and   
       Bernhard Möller and   
                   Georg Struth   Kleene algebra with domain . . . . . . . 798--833


ACM Transactions on Computational Logic
Volume 8, Number 1, January, 2007

       Maria Paola Bonacina and   
              Nachum Dershowitz   Abstract canonical inference . . . . . . ??
              Alessio Guglielmi   A system of interaction and structure    ??
           Paolo Liberatore and   
                  Marco Schaerf   Compilability of propositional abduction ??
           Annabelle McIver and   
                 Carroll Morgan   Results on the quantitative
                                  $\mu$-calculus $q{M}\mu$ . . . . . . . . ??
           Alexander Rabinovich   On compositionality and its limitations  ??
            Joost Vennekens and   
                David Gilis and   
                  Marc Denecker   Erratum to splitting an operator:
                                  Algebraic modularity results for logics
                                  with fixpoint semantics  . . . . . . . . ??
                Greta Yorsh and   
                Thomas Reps and   
                Mooly Sagiv and   
               Reinhard Wilhelm   Logical characterizations of heap
                                  abstractions . . . . . . . . . . . . . . ??

ACM Transactions on Computational Logic
Volume 8, Number 2, April, 2007

           Michael Benedikt and   
              Leonid Libkin and   
                    Frank Neven   Logical definability and query languages
                                  over ranked and unranked trees . . . . . ??
                     Karl Crary   Sound and complete elimination of
                                  singleton kinds  . . . . . . . . . . . . ??
          John M. Hitchcock and   
               Jack H. Lutz and   
          Sebastiaan A. Terwijn   The arithmetical complexity of dimension
                                  and randomness . . . . . . . . . . . . . ??
               Paolo Liberatore   Where fail-safe default logics fail  . . ??
               Fangzhen Lin and   
                   Jia-Huai You   Recycling computed answers in rewrite
                                  systems for abduction  . . . . . . . . . ??
   Viorica Sofronie-Stokkermans   On unification for bounded distributive
                                  lattices . . . . . . . . . . . . . . . . ??

ACM Transactions on Computational Logic
Volume 8, Number 3, July, 2007

             Marco Pedicini and   
              Francesco Quaglia   PELCR: Parallel environment for optimal
                                  lambda-calculus reduction  . . . . . . . 14:1--14:??
              Andreas Blass and   
                  Yuri Gurevich   Ordinary interactive small-step
                                  algorithms, II . . . . . . . . . . . . . 15:1--15:??
              Andreas Blass and   
                  Yuri Gurevich   Ordinary interactive small-step
                                  algorithms, III  . . . . . . . . . . . . 16:1--16:??
               Thomas Eiter and   
               Michael Fink and   
                 Stefan Woltran   Semantical characterizations and
                                  complexity of equivalences in answer set
                                  programming  . . . . . . . . . . . . . . 17:1--17:??
                    Ofer Arieli   Paraconsistent reasoning and
                                  preferential entailments by signed
                                  quantified Boolean formulae  . . . . . . 18:1--18:??

ACM Transactions on Computational Logic
Volume 8, Number 4, August, 2007

          Renate A. Schmidt and   
                Ullrich Hustadt   The axiomatic translation principle for
                                  modal logic  . . . . . . . . . . . . . . 19:1--19:??
            Sophie Laplante and   
          Richard Lassaigne and   
Frédéric Magniez and   
          Sylvain Peyronnet and   
            Michel de Rougemont   Probabilistic abstraction for model
                                  checking: an approach based on property
                                  testing  . . . . . . . . . . . . . . . . 20:1--20:??
              Arnaud Durand and   
              Etienne Grandjean   First-order queries on structures of
                                  bounded degree are computable with
                                  constant delay . . . . . . . . . . . . . 21:1--21:??
            Nicola Olivetti and   
          Gian Luca Pozzato and   
             Camilla B. Schwind   A sequent calculus and a theorem prover
                                  for standard conditional logics  . . . . 22:1--22:??
                 C. W. Choi and   
               J. H. M. Lee and   
                  P. J. Stuckey   Removing propagation redundant
                                  constraints in redundant modeling  . . . 23:1--23:??
                Edward Hung and   
                Lise Getoor and   
             V. S. Subrahmanian   Probabilistic interval XML . . . . . . . 24:1--24:??


ACM Transactions on Computational Logic
Volume 9, Number 1, December, 2007

              Sharon Shoham and   
                  Orna Grumberg   A game-based framework for CTL
                                  counterexamples and 3-valued
                                  abstraction-refinement . . . . . . . . . 1:1--1:??
              Jeremy Avigad and   
             Kevin Donnelly and   
                 David Gray and   
                      Paul Raff   A formally verified proof of the prime
                                  number theorem . . . . . . . . . . . . . 2:1--2:23
        Jan Van den Bussche and   
              Stijn Vansummeren   Polymorphic type inference for the named
                                  nested relational calculus . . . . . . . 3:1--3:??
         Shuvendu K. Lahiri and   
               Randal E. Bryant   Predicate abstraction with indexed
                                  predicates . . . . . . . . . . . . . . . 4:1--4:??
             Christel Baier and   
          Nathalie Bertrand and   
           Philippe Schnoebelen   Verifying nondeterministic probabilistic
                                  channel systems against $\omega$-regular
                                  linear-time properties . . . . . . . . . 5:1--5:??
      Ma\lgorzata Biernacka and   
                  Olivier Danvy   A concrete framework for environment
                                  machines . . . . . . . . . . . . . . . . 6:1--6:??
          Fabrizio Angiulli and   
            Gianluigi Greco and   
                 Luigi Palopoli   Outlier detection by logic programming   7:1--7:??

ACM Transactions on Computational Logic
Volume 9, Number 2, March, 2008

            Silvio Ghilardi and   
            Enrica Nicolini and   
              Daniele Zucchelli   A comprehensive combination framework    8:1--8:??
              Chiaki Sakama and   
                  Katsumi Inoue   Coordination in answer set programming   9:1--9:??
            Slawomir Lasota and   
               Igor Walukiewicz   Alternating timed automata . . . . . . . 10:1--10:??
                 Felix Klaedtke   Bounds on the automata size for
                                  Presburger arithmetic  . . . . . . . . . 11:1--11:??
 Véronique Bruy\`ere and   
         Emmanuel Dall'olio and   
    Jean-François Raskin   Durations and parametric model-checking
                                  in timed automata  . . . . . . . . . . . 12:1--12:??
              Floris Geerts and   
           Sofie Haesevoets and   
                  Bart Kuijpers   First-order complete and computationally
                                  complete query languages for
                                  spatio-temporal databases  . . . . . . . 13:1--13:??
              Marc Denecker and   
              Eugenia Ternovska   A logic of nonmonotone inductive
                                  definitions  . . . . . . . . . . . . . . 14:1--14:??

ACM Transactions on Computational Logic
Volume 9, Number 3, June, 2008

            Agostino Dovier and   
               Carla Piazza and   
               Gianfranco Rossi   A uniform approach to constraint-solving
                                  for lists, multisets, compact lists, and
                                  sets . . . . . . . . . . . . . . . . . . 15:1--15:??
                 Karl Crary and   
                  Susmit Sarkar   Foundational certified code in the Twelf
                                  metalogical framework  . . . . . . . . . 16:1--16:??
               Samir Genaim and   
                      Andy King   Inferring non-suspension conditions for
                                  logic programs with dynamic scheduling   17:1--17:??
              Andreas Blass and   
                  Yuri Gurevich   Program termination and well partial
                                  orderings  . . . . . . . . . . . . . . . 18:1--18:??
              Andreas Blass and   
                  Yuri Gurevich   Abstract state machines capture parallel
                                  algorithms: Correction and extension . . 19:1--19:??
              Hana Chockler and   
          Joseph Y. Halpern and   
                 Orna Kupferman   What causes a system to satisfy a
                                  specification? . . . . . . . . . . . . . 20:1--20:??
                Simone Bova and   
                Franco Montagna   Proof search in Hájek's basic logic . . . 21:1--21:??
            Diego Calvanese and   
        Giuseppe De Giacomo and   
             Maurizio Lenzerini   Conjunctive query containment and
                                  answering under description logic
                                  constraints  . . . . . . . . . . . . . . 22:1--22:??
        Aleksandar Nanevski and   
             Frank Pfenning and   
               Brigitte Pientka   Contextual modal type theory . . . . . . 23:1--23:??

ACM Transactions on Computational Logic
Volume 9, Number 4, August, 2008

          Yannick Chevalier and   
          Ralf Küsters and   
   Michaël Rusinowitch and   
                Mathieu Turuani   Complexity results for security
                                  protocols with Diffie--Hellman
                                  exponentiation and commuting public key
                                  encryption . . . . . . . . . . . . . . . 24:1--24:??
               Frank Wolter and   
          Michael Zakharyaschev   Undecidability of the unification and
                                  admissibility problems for modal and
                                  description logics . . . . . . . . . . . 25:1--25:??
              Stijn Heymans and   
      Davy Van Nieuwenborgh and   
                   Dirk Vermeir   Open answer set programming with guarded
                                  programs . . . . . . . . . . . . . . . . 26:1--26:??
                   Yi-Dong Shen   Reasoning with recursive loops under the
                                  PLP framework  . . . . . . . . . . . . . 27:1--27:??
               Helmut Seidl and   
             Kumar Neeraj Verma   Flat and one-variable clauses:
                                  Complexity of verifying cryptographic
                                  protocols with single blind copying  . . 28:1--28:??
              Marco Alberti and   
           Federico Chesani and   
            Marco Gavanelli and   
              Evelina Lamma and   
                Paola Mello and   
                  Paolo Torroni   Verifiable agent interaction in
                                  abductive logic programming: The SCIFF
                                  framework  . . . . . . . . . . . . . . . 29:1--29:??


ACM Transactions on Computational Logic
Volume 10, Number 1, January, 2009

          Alexander Artikis and   
               Marek Sergot and   
                    Jeremy Pitt   Specifying norm-governed computational
                                  societies  . . . . . . . . . . . . . . . 1:1--1:??
          Lou Van Den Dries and   
         Yiannis N. Moschovakis   Arithmetic complexity  . . . . . . . . . 2:1--2:??
           Neil Yorke-Smith and   
                  Carmen Gervet   Certainty closure: Reliable constraint
                                  reasoning with incomplete or erroneous
                                  data . . . . . . . . . . . . . . . . . . 3:1--3:??
         Alessandro Armando and   
       Maria Paola Bonacina and   
              Silvio Ranise and   
                 Stephan Schulz   New results on rewrite-based
                                  satisfiability procedures  . . . . . . . 4:1--4:??
                Luca Iocchi and   
         Thomas Lukasiewicz and   
              Daniele Nardi and   
                Riccardo Rosati   Reasoning about actions with sensing
                                  under qualitative and probabilistic
                                  uncertainty  . . . . . . . . . . . . . . 5:1--5:??
                 Luca Aceto and   
                Wan Fokkink and   
         Anna Ingolfsdottir and   
                     Bas Luttik   A finite equational base for CCS with
                                  left merge and communication merge . . . 6:1--6:??
                  Juha Kontinen   A logical characterization of the
                                  counting hierarchy . . . . . . . . . . . 7:1--7:??

ACM Transactions on Computational Logic
Volume 10, Number 2, February, 2009

                   Ugo Dal Lago   The geometry of linear higher-order
                                  recursion  . . . . . . . . . . . . . . . 8:1--8:??
            Ruggero Lanotte and   
                    Simone Tini   Probabilistic bisimulation as a
                                  congruence . . . . . . . . . . . . . . . 9:1--9:??
           Isabelle Gnaedig and   
       Hél\`ene Kirchner   Termination of rewriting under
                                  strategies . . . . . . . . . . . . . . . 10:1--10:??
        Maurizio Gabbrielli and   
               Maria Chiara Meo   A compositional semantics for CHR  . . . 11:1--11:??
           Stefano Guerrini and   
                  Andrea Masini   Proofs, tests and continuation passing
                                  style  . . . . . . . . . . . . . . . . . 12:1--12:??
         Lutz Schröder and   
                 Dirk Pattinson   PSPACE bounds for rank-1 modal logics    13:1--13:??
             Paola Bruscoli and   
              Alessio Guglielmi   On the proof complexity of deep
                                  inference  . . . . . . . . . . . . . . . 14:1--14:??

ACM Transactions on Computational Logic
Volume 10, Number 3, April, 2009

               Stavros Tripakis   Checking timed Büchi automata emptiness
                                  on simulation graphs . . . . . . . . . . 15:1--15:??
      Stéphane Demri and   
                  Ranko Lazi\'c   LTL with the freeze quantifier and
                                  register automata  . . . . . . . . . . . 16:1--16:??
             Lucas Bordeaux and   
               Marco Cadoli and   
                   Toni Mancini   Generalizing consistency and other
                                  constraint properties to quantified
                                  constraints  . . . . . . . . . . . . . . 17:1--17:??
             Laura Giordano and   
          Valentina Gliozzi and   
            Nicola Olivetti and   
              Gian Luca Pozzato   Analytic tableaux calculi for KLM logics
                                  of nonmonotonic reasoning  . . . . . . . 18:1--18:??
             Mingsheng Ying and   
                  Yuan Feng and   
                Runyao Duan and   
                   Zhengfeng Ji   An algebra of quantum processes  . . . . 19:1--19:??
                  Adel Bouhoula   Simultaneous checking of completeness
                                  and ground confluence for algebraic
                                  specifications . . . . . . . . . . . . . 20:1--20:??
             Laura Giordano and   
          Valentina Gliozzi and   
            Nicola Olivetti and   
                Camilla Schwind   Tableau calculus for preference-based
                                  conditional logics: PCL and its
                                  extensions . . . . . . . . . . . . . . . 21:1--21:??
              Akitoshi Kawamura   Differential recursion . . . . . . . . . 22:1--22:??

ACM Transactions on Computational Logic
Volume 10, Number 4, August, 2009

            Patrick Baillot and   
           Jean-Yves Marion and   
      Simona Ronchi Della Rocca   Guest editorial: Special issue on
                                  implicit computational complexity  . . . 23:1--23:??
             Toshiyasu Arai and   
                   Naohi Eguchi   A new function algebra of EXPTIME
                                  functions by safe nested recursion . . . 24:1--24:??
                   Ugo Dal Lago   Context semantics, linear logic, and
                                  computational complexity . . . . . . . . 25:1--25:??
            Tristan Crolard and   
        Emmanuel Polonowski and   
               Pierre Valarcher   Extending the loop language with
                                  higher-order procedural variables  . . . 26:1--26:??
           Jean-Yves Marion and   
          Romain Péchoux   Sup-interpretations, a semantic method
                                  for static analysis of program resources 27:1--27:??
              Neil D. Jones and   
               Lars Kristiansen   A flow calculus of mwp-bounds for
                                  complexity analysis  . . . . . . . . . . 28:1--28:??
                Jean-Yves Moyen   Resource control graphs  . . . . . . . . 29:1--29:??


ACM Transactions on Computational Logic
Volume 11, Number 1, October, 2009

      Krishnendu Chatterjee and   
        Thomas A. Henzinger and   
                   Florian Horn   Finitary winning in $\omega$-regular
                                  games  . . . . . . . . . . . . . . . . . 1:1--1:??
       Peter Schneider-Kamp and   
          Jürgen Giesl and   
       Alexander Serebrenik and   
           René Thiemann   Automated termination proofs for logic
                                  programs by term rewriting . . . . . . . 2:1--2:??
           Valentin Goranko and   
                 Dmitry Shkatov   Tableau-based decision procedures for
                                  logics of strategic ability in
                                  multiagent systems . . . . . . . . . . . 3:1--3:??
           Michael Benedikt and   
                   Luc Segoufin   Regular tree languages definable in FO
                                  and in FO$_{mod}$  . . . . . . . . . . . 4:1--4:??
                Ferruccio Guidi   The formal system $\lambda \delta$ . . . 5:1--5:??
               Brigitte Pientka   Higher-order term indexing using
                                  substitution trees . . . . . . . . . . . 6:1--6:??
                 Rob Arthan and   
              Ursula Martin and   
          Erik A. Mathiesen and   
                    Paulo Oliva   A general framework for sound and
                                  complete Floyd-Hoare logics  . . . . . . 7:1--7:??

ACM Transactions on Computational Logic
Volume 11, Number 2, January, 2010

               James Bailey and   
                Guozhu Dong and   
             Anthony Widjaja To   Logical queries over views: Decidability
                                  and expressiveness . . . . . . . . . . . 8:1--8:??
         Hubert Comon-Lundh and   
   Véronique Cortier and   
         Eugen Zãlinescu   Deciding security properties for
                                  cryptographic protocols. Application to
                                  key cycles . . . . . . . . . . . . . . . 9:1--9:??
             Octavian Udrea and   
  Diego Reforgiato Recupero and   
             V. S. Subrahmanian   Annotated RDF  . . . . . . . . . . . . . 10:1--10:??
                Robin Adams and   
                    Zhaohui Luo   Weyl's predicative classical mathematics
                                  as a logic-enriched type theory  . . . . 11:1--11:??
         Stavros Cosmadakis and   
         Eugenie Foustoucos and   
        Anastasios Sidiropoulos   Undecidability and intractability
                                  results concerning datalog programs and
                                  their persistency numbers  . . . . . . . 12:1--12:??
                  Alwen Tiu and   
                    Dale Miller   Proof search specifications of
                                  bisimulation and modal logics for the
                                  $\pi$-calculus . . . . . . . . . . . . . 13:1--13:??
               Thomas Eiter and   
                Mantas \vSimkus   FDNC: Decidable nonmonotonic disjunctive
                                  logic programs with function symbols . . 14:1--14:??

ACM Transactions on Computational Logic
Volume 11, Number 3, May, 2010

            Manuel Bodirsky and   
                Jan Kára   A fast algorithm and datalog
                                  inexpressibility for temporal reasoning  15:1--15:??
          Kedar S. Namjoshi and   
             Richard J. Trefler   On the completeness of compositional
                                  reasoning methods  . . . . . . . . . . . 16:1--16:??
         Detlef Kähler and   
          Ralf Küsters and   
                   Thomas Wilke   Deciding strategy properties of
                                  contract-signing protocols . . . . . . . 17:1--17:??
          Nachum Dershowitz and   
                  Iddo Tzameret   Complexity of propositional proofs under
                                  a promise  . . . . . . . . . . . . . . . 18:1--18:??
             Eli Ben-Sasson and   
                Prahladh Harsha   Lower bounds for bounded depth Frege
                                  proofs via Pudlák--Buss games . . . . . . 19:1--19:??
                Marko Samer and   
                   Helmut Veith   On the distributivity of LTL
                                  specifications . . . . . . . . . . . . . 20:1--20:??

ACM Transactions on Computational Logic
Volume 11, Number 4, July, 2010

           Michael Kaminski and   
                 Simone Martini   CSL 2008 special issue . . . . . . . . . 21:1--21:??
           Olaf Beyersdorff and   
          Sebastian Müller   A tight Karp--Lipton collapse result in
                                  bounded arithmetic . . . . . . . . . . . 22:1--22:??
      Krishnendu Chatterjee and   
              Laurent Doyen and   
            Thomas A. Henzinger   Quantitative languages . . . . . . . . . 23:1--23:??
             Nadia Creignou and   
            Henning Schnoor and   
                   Ilka Schnoor   Nonuniform Boolean constraint
                                  satisfaction problems with cardinality
                                  constraint . . . . . . . . . . . . . . . 24:1--24:??
Mariangiola Dezani-Ciancaglini and   
           Roberto Di Cosmo and   
           Elio Giovannetti and   
                 Makoto Tatsuta   On isomorphisms of intersection types    25:1--25:??
             Martin Hofmann and   
             Ulrich Schöpp   Pure pointer programs with iteration . . 26:1--26:??
           Matthias Horbach and   
           Christoph Weidenbach   Superposition for fixed domains  . . . . 27:1--27:??
                  Alexis Saurin   Typing streams in the $\Lambda
                                  \mu$-calculus  . . . . . . . . . . . . . 28:1--28:??
              Hana Chockler and   
          Joseph Y. Halpern and   
                 Orna Kupferman   Erratum for ``What causes a system to
                                  satisfy a specification?'' . . . . . . . 29:1--29:??


ACM Transactions on Computational Logic
Volume 12, Number 1, October, 2010

               Rohit Chadha and   
             Mahesh Viswanathan   A counterexample-guided
                                  abstraction-refinement framework for
                                  Markov decision processes  . . . . . . . 1:1--1:??
                 Axel Legay and   
                  Pierre Wolper   On (Omega-)regular model checking  . . . 2:1--2:??
              Georg Gottlob and   
           Reinhard Pichler and   
                       Fang Wei   Monadic datalog over finite structures
                                  of bounded treewidth . . . . . . . . . . 3:1--3:??
              Nicola Galesi and   
                 Massimo Lauria   Optimality of size-degree tradeoffs for
                                  polynomial calculus  . . . . . . . . . . 4:1--4:??
         Stefano Bistarelli and   
              Ugo Montanari and   
            Francesca Rossi and   
              Francesco Santini   Unicast and multicast QoS routing with
                                  soft-constraint logic programming  . . . 5:1--5:??
           David Billington and   
          Grigoris Antoniou and   
          Guido Governatori and   
                  Michael Maher   An inclusion theorem for defeasible
                                  logics . . . . . . . . . . . . . . . . . 6:1--6:??
         Alessandro Cimatti and   
            Alberto Griggio and   
             Roberto Sebastiani   Efficient generation of Craig
                                  interpolants in satisfiability modulo
                                  theories . . . . . . . . . . . . . . . . 7:1--7:??
             Carlo A. Furia and   
                   Matteo Rossi   A theory of sampling for continuous-time
                                  metric temporal logic  . . . . . . . . . 8:1--8:??

ACM Transactions on Computational Logic
Volume 12, Number 2, January, 2011

              Yuri Gurevich and   
                    Itay Neeman   Logic of infons: The propositional case  9:1--9:??
                  Ranko Lazi\'c   Safety alternating automata on data
                                  words  . . . . . . . . . . . . . . . . . 10:1--10:??
               Thomas Eiter and   
       Giovambattista Ianni and   
         Thomas Lukasiewicz and   
              Roman Schindlauer   Well-founded semantics for description
                                  logic programs in the Semantic Web . . . 11:1--11:??
                 Stefan Szeider   Monadic second order logic on graphs
                                  with local cardinality constraints . . . 12:1--12:??
            Michael Bauland and   
            Martin Mundhenk and   
           Thomas Schneider and   
            Henning Schnoor and   
               Ilka Schnoor and   
               Heribert Vollmer   The tractability of model checking for
                                  LTL: The good, the bad, and the ugly
                                  fragments  . . . . . . . . . . . . . . . 13:1--13:??
            Paulo Shakarian and   
              Austin Parker and   
             Gerardo Simari and   
Venkatramana V. S. Subrahmanian   Annotated probabilistic temporal logic   14:1--14:??
            Christian Urban and   
               James Cheney and   
               Stefan Berghofer   Mechanizing the metatheory of LF . . . . 15:1--15:??
              Andreas Blass and   
                  Yuri Gurevich   Persistent queries in the behavioral
                                  theory of algorithms . . . . . . . . . . 16:1--16:??
          Anastasia Analyti and   
          Grigoris Antoniou and   
          Carlos Viegas Damasio   MWeb: a principled framework for modular
                                  Web rule bases and its semantics . . . . 17:1--17:??

ACM Transactions on Computational Logic
Volume 12, Number 3, May, 2011

           Flemming Nielson and   
             Sebastian Nanz and   
             Hanne Riis Nielson   Modal abstractions of concurrent
                                  behavior . . . . . . . . . . . . . . . . 18:1--18:??
        Marcin Jurdzi\'nski and   
                  Ranko Lazi\'c   Alternating automata on data trees and
                                  XPath satisfiability . . . . . . . . . . 19:1--19:??
              Jos De Bruijn and   
               Thomas Eiter and   
              Axel Polleres and   
                   Hans Tompits   Embedding nonground logic programs into
                                  autoepistemic logic for knowledge-base
                                  combination  . . . . . . . . . . . . . . 20:1--20:??
            Jan A. Bergstra and   
                    Alban Ponse   Proposition algebra  . . . . . . . . . . 21:1--21:??
José Espírito Santo and   
              Luís Pinto   A calculus of multiary sequent terms . . 22:1--22:??

ACM Transactions on Computational Logic
Volume 12, Number 4, July, 2011

    Lutz Straß Burger and   
              Alessio Guglielmi   A system of interaction and structure
                                  IV: The exponentials and decomposition   23:1--23:??
              Andrei A. Bulatov   Complexity of conservative constraint
                                  satisfaction problems  . . . . . . . . . 24:1--24:??
                 Paolo Ferraris   Logic programs with propositional
                                  connectives and aggregates . . . . . . . 25:1--25:??
      Adri\`a Gascón and   
              Guillem Godoy and   
        Manfred Schmidt-Schauss   Unification and matching on compressed
                                  terms  . . . . . . . . . . . . . . . . . 26:1--26:??
       Miko\laj Boja\'nczyk and   
               Claire David and   
              Anca Muscholl and   
          Thomas Schwentick and   
                   Luc Segoufin   Two-variable logic on data words . . . . 27:1--27:??
      Krishnendu Chatterjee and   
             Luca De Alfaro and   
            Thomas A. Henzinger   Qualitative concurrent parity games  . . 28:1--28:??
             Md. Aquil Khan and   
                 Mohua Banerjee   Logics for information systems and their
                                  dynamic extensions . . . . . . . . . . . 29:1--29:??


ACM Transactions on Computational Logic
Volume 13, Number 1, January, 2012

             Arie Gurfinkel and   
                 Marsha Chechik   Robust Vacuity for Branching Temporal
                                  Logic  . . . . . . . . . . . . . . . . . 1:1--1:??
                   David Baelde   Least and Greatest Fixed Points in
                                  Linear Logic . . . . . . . . . . . . . . 2:1--2:??
         Benno van den Berg and   
                 Richard Garner   Topological and Simplicial Models of
                                  Identity Types . . . . . . . . . . . . . 3:1--3:??
              Wouter Gelade and   
                    Frank Neven   Succinctness of the Complement and
                                  Intersection of Regular Expressions  . . 4:1--4:??
          Florent Madelaine and   
                 Barnaby Martin   The Complexity of Positive First-Order
                                  Logic without Equality . . . . . . . . . 5:1--5:??
           Cinzia Di Giusto and   
        Maurizio Gabbrielli and   
               Maria Chiara Meo   On the Expressive Power of Multiple
                                  Heads in CHR . . . . . . . . . . . . . . 6:1--6:??
            Naghmeh Ghafari and   
             Arie Gurfinkel and   
              Nils Klarlund and   
                Richard Trefler   Reachability Problems in Piecewise FIFO
                                  Systems  . . . . . . . . . . . . . . . . 7:1--7:??
        Jeroen J. A. Keiren and   
          Michel A. Reniers and   
             Tim A. C. Willemse   Structural Analysis of Boolean Equation
                                  Systems  . . . . . . . . . . . . . . . . 8:1--8:??
              Phuong Nguyen and   
                   Stephen Cook   The Complexity of Proving the Discrete
                                  Jordan Curve Theorem . . . . . . . . . . 9:1--9:??

ACM Transactions on Computational Logic
Volume 13, Number 2, April, 2012

                 Jordi Levy and   
                 Mateu Villaret   Nominal Unification from a Higher-Order
                                  Perspective  . . . . . . . . . . . . . . 10:1--10:??
            Stefano Berardi and   
                 Ugo de'Liguoro   Interactive Realizers: a New Approach to
                                  Program Extraction from Nonconstructive
                                  Proofs . . . . . . . . . . . . . . . . . 11:1--11:??
            Kousha Etessami and   
             Mihalis Yannakakis   Model Checking of Recursive
                                  Probabilistic Systems  . . . . . . . . . 12:1--12:??
            Paulo Shakarian and   
          Gerardo I. Simari and   
             V. S. Subrahmanian   Annotated Probabilistic Temporal Logic:
                                  Approximate Fixpoint Implementation  . . 13:1--13:??
              Mauro Ferrari and   
         Camillo Fiorentini and   
                  Guido Fiorino   Simplification Rules for Intuitionistic
                                  Propositional Tableaux . . . . . . . . . 14:1--14:??
          Sebastian Danicic and   
          Robert M. Hierons and   
            Michael R. Laurence   Complexity of Data Dependence Problems
                                  for Program Schemas with Concurrency . . 15:1--15:??
           Jakob Nordström   On the Relative Strength of Pebbling and
                                  Resolution . . . . . . . . . . . . . . . 16:1--16:??
             Nadia Creignou and   
                 Arne Meier and   
           Heribert Vollmer and   
                 Michael Thomas   The Complexity of Reasoning for
                                  Fragments of Autoepistemic Logic . . . . 17:1--17:??
             Marco Gaboardi and   
           Jean-Yves Marion and   
      Simona Ronchi Della Rocca   An Implicit Characterization of PSPACE   18:1--18:??

ACM Transactions on Computational Logic
Volume 13, Number 3, August, 2012

              Wouter Gelade and   
           Marcel Marquardt and   
              Thomas Schwentick   The dynamic complexity of formal
                                  languages  . . . . . . . . . . . . . . . 19:1--19:??
               Gilles Dowek and   
              Murdoch J. Gabbay   Permissive-nominal logic: First-order
                                  logic over nominal terms and sets  . . . 20:1--20:??
               Franz Baader and   
            Silvio Ghilardi and   
                   Carsten Lutz   LTL over description logic axioms  . . . 21:1--21:??
            Sara Miner More and   
                   Pavel Naumov   Calculus of cooperation and game-based
                                  reasoning about protocol privacy . . . . 22:1--22:??
            Kazuhisa Makino and   
                   Hirotaka Ono   Deductive inference for the interiors
                                  and exteriors of Horn theories . . . . . 23:1--23:??
  Bjòrn Kjos-Hanssen and   
              Frank Stephan and   
                  Jason Teutsch   Arithmetic complexity via effective
                                  names for random sequences . . . . . . . 24:1--24:??
          Alessandro Bianco and   
             Fabio Mogavero and   
                 Aniello Murano   Graded computation tree logic  . . . . . 25:1--25:??
           Robert Goldblatt and   
                 Marcel Jackson   Well-structured program equivalence is
                                  highly undecidable . . . . . . . . . . . 26:1--26:??
                Rajeev Alur and   
         Pavol Cerný and   
                Scott Weinstein   Algorithmic analysis of array-accessing
                                  programs . . . . . . . . . . . . . . . . 27:1--27:??

ACM Transactions on Computational Logic
Volume 13, Number 4, October, 2012

Konstantinos Chatzikokolakis and   
              Sophia Knight and   
       Catuscia Palamidessi and   
             Prakash Panangaden   Epistemic Strategies and Games on
                                  Concurrent Processes . . . . . . . . . . 28:1--28:??
                  Udi Boker and   
                 Orna Kupferman   Translating to Co--Büchi Made Tight,
                                  Unified, and Useful  . . . . . . . . . . 29:1--29:??
              Pavlos Peppas and   
          Costas D. Koutras and   
             Mary-Anne Williams   Maps in Multiple Belief Change . . . . . 30:1--30:??
              Arnaud Durand and   
                  Juha Kontinen   Hierarchies in Dependence Logic  . . . . 31:1--31:??
     Ewa Madali\'nska-Bugaj and   
                Linh Anh Nguyen   A Generalized QSQR Evaluation Method for
                                  Horn Knowledge Bases . . . . . . . . . . 32:1--32:??
          Steven Schockaert and   
             Jeroen Janssen and   
                   Dirk Vermeir   Fuzzy Equilibrium Logic: Declarative
                                  Problem Solving in Continuous Domains    33:1--33:??
                 Diego Figueira   Decidability of Downward XPath . . . . . 34:1--34:??


ACM Transactions on Computational Logic
Volume 14, Number 1, February, 2013

               Hariolf Betz and   
            Thom Frühwirth   Linear-Logic Based Analysis of
                                  Constraint Handling Rules with
                                  Disjunction  . . . . . . . . . . . . . . 1:1--1:??
       Markus Krötzsch and   
          Sebastian Rudolph and   
                 Pascal Hitzler   Complexities of Horn Description Logics  2:1--2:??
              Xiaoping Chen and   
                 Jianmin Ji and   
                   Fangzhen Lin   Computing Loops with at Most One
                                  External Support Rule  . . . . . . . . . 3:1--3:??
             Mathieu Baudet and   
   Véronique Cortier and   
       Stéphanie Delaune   YAPA: a Generic Tool for Computing
                                  Intruder Knowledge . . . . . . . . . . . 4:1--4:??
               Richard McKinley   Proof Nets for Herbrand's Theorem  . . . 5:1--5:??
 Dominique Larchey-Wendling and   
                Didier Galmiche   Nondeterministic Phase Semantics and the
                                  Undecidability of Boolean BI . . . . . . 6:1--6:??
      Marcello M. Bonsangue and   
              Stefan Milius and   
                Alexandra Silva   Sound and Complete Axiomatizations of
                                  Coalgebraic Language Equivalence . . . . 7:1--7:??

ACM Transactions on Computational Logic
Volume 14, Number 2, June, 2013

              Alexander Kartzow   First-Order Logic on Higher-Order Nested
                                  Pushdown Trees . . . . . . . . . . . . . 8:1--8:??
                Paul Gastin and   
              Nathalie Sznajder   Fair Synthesis for Asynchronous
                                  Distributed Systems  . . . . . . . . . . 9:1--9:??
            Paulo Shakarian and   
        Matthias Broecheler and   
         V. S. Subrahmanian and   
              Cristian Molinaro   Using Generalized Annotated Programs to
                                  Solve Social Network Diffusion
                                  Optimization Problems  . . . . . . . . . 10:1--10:??
             Mnacho Echenim and   
                Nicolas Peltier   Instantiation Schemes for Nested
                                  Theories . . . . . . . . . . . . . . . . 11:1--11:??
          Gerardo I. Simari and   
          John P. Dickerson and   
                  Amy Sliva and   
             V. S. Subrahmanian   Parallel Abductive Query Answering in
                                  Probabilistic Logic Programs . . . . . . 12:1--12:??
           Roman Kontchakov and   
                Yavor Nenov and   
         Ian Pratt-Hartmann and   
          Michael Zakharyaschev   Topological Logics with Connectedness
                                  over Euclidean Spaces  . . . . . . . . . 13:1--13:??
            James Delgrande and   
             Torsten Schaub and   
               Hans Tompits and   
                 Stefan Woltran   A Model-Theoretic Approach to Belief
                                  Change in Answer Set Programming . . . . 14:1--14:??
              Martin Gebser and   
                 Torsten Schaub   Tableau Calculi for Logic Programs under
                                  Answer Set Semantics . . . . . . . . . . 15:1--15:??
José Júlio Alferes and   
             Matthias Knorr and   
                 Terrance Swift   Query-Driven Procedures for Hybrid MKNF
                                  Knowledge Bases  . . . . . . . . . . . . 16:1--16:??

ACM Transactions on Computational Logic
Volume 14, Number 3, August, 2013

              Johan Wittocx and   
              Marc Denecker and   
             Maurice Bruynooghe   Constraint Propagation for First-Order
                                  Logic and Inductive Definitions  . . . . 17:1--17:??
                     M. Praveen   Does Treewidth Help in Modal
                                  Satisfiability?  . . . . . . . . . . . . 18:1--18:??
                       Tony Tan   Graph Reachability and Pebble Automata
                                  over Infinite Alphabets  . . . . . . . . 19:1--19:??
           Olaf Beyersdorff and   
              Nicola Galesi and   
                 Massimo Lauria   Parameterized Complexity of DPLL Search
                                  Procedures . . . . . . . . . . . . . . . 20:1--20:??
      Angelos Charalambidis and   
  Konstantinos Handjopoulos and   
    Panagiotis Rondogiannis and   
               William W. Wadge   Extensional Higher-Order Logic
                                  Programming  . . . . . . . . . . . . . . 21:1--21:??
              Elvira Albert and   
               Samir Genaim and   
                Abu Naser Masud   On the Inference of Resource Usage Upper
                                  and Lower Bounds . . . . . . . . . . . . 22:1--22:??
              Floor Sietsma and   
               Krzysztof R. Apt   Common Knowledge in Email Exchanges  . . 23:1--23:??
             Andreas Herzig and   
                Jerome Lang and   
                 Pierre Marquis   Propositional Update Operators Based on
                                  Formula/Literal Dependence . . . . . . . 24:1--24:??

ACM Transactions on Computational Logic
Volume 14, Number 4, November, 2013

            Wojciech Kazana and   
                   Luc Segoufin   Enumeration of monadic second-order
                                  queries on trees . . . . . . . . . . . . 25:1--25:??
      Jónathan Heras and   
            Thierry Coquand and   
       Anders Mörtberg and   
                  Vincent Siles   Computing persistent homology within
                                  Coq/SSReflect  . . . . . . . . . . . . . 26:1--26:??
                  Ori Lahav and   
                    Arnon Avron   A unified semantic framework for fully
                                  structural propositional sequent systems 27:1--27:??
           Jose Gaintzarain and   
                    Paqui Lucio   Logical foundations for more expressive
                                  declarative temporal logic programming
                                  languages  . . . . . . . . . . . . . . . 28:1--28:??
              Olivier Danvy and   
                      Ian Zerny   Three syntactic theories for combinatory
                                  graph reduction  . . . . . . . . . . . . 29:1--29:??
            Manuel Bodirsky and   
       H. Dugald Macpherson and   
                  Johan Thapper   Constraint satisfaction tractability
                                  from semi-lattice operations on infinite
                                  sets . . . . . . . . . . . . . . . . . . 30:1--30:??
              Jeroen Ketema and   
            Jakob Grue Simonsen   Least upper bounds on the size of
                                  confluence and Church--Rosser diagrams
                                  in term rewriting and $ \lambda
                                  $-calculus . . . . . . . . . . . . . . . 31:1--31:??
               Florian Rabe and   
              Kristina Sojakova   Logical relations for a logical
                                  framework  . . . . . . . . . . . . . . . 32:1--32:??
                Taolue Chen and   
             Marco Diciolla and   
          Marta Kwiatkowska and   
             Alexandru Mereacre   Verification of linear duration
                                  properties over continuous-time Markov
                                  chains . . . . . . . . . . . . . . . . . 33:1--33:??
               Roy Dyckhoff and   
        Mehrnoosh Sadrzadeh and   
                Julien Truffaut   Algebra, proof theory and applications
                                  for an intuitionistic logic of
                                  propositions, actions and adjoint modal
                                  operators  . . . . . . . . . . . . . . . 34:1--34:??


ACM Transactions on Computational Logic
Volume 15, Number 1, February, 2014

               Matthew S. Bauer   A PSPACE-complete first-order fragment
                                  of computability logic . . . . . . . . . 1:1--1:??
            Arnold Beckmann and   
                 Samuel R. Buss   Improved witnessing and local
                                  improvement principles for second-order
                                  bounded arithmetic . . . . . . . . . . . 2:1--2:??
             Filippo Bonchi and   
      Marcello M. Bonsangue and   
            Helle H. Hansen and   
         Prakash Panangaden and   
        Jan J. M. M. Rutten and   
                Alexandra Silva   Algebra-coalgebra duality in
                                  Brzozowski's minimization algorithm  . . 3:1--3:??
   David Fernández-Duque   Non-finite axiomatizability of dynamic
                                  topological logic  . . . . . . . . . . . 4:1--4:??
        Roberto Bruttomesso and   
            Silvio Ghilardi and   
                  Silvio Ranise   Quantifier-free interpolation in
                                  combinations of equality interpolating
                                  theories . . . . . . . . . . . . . . . . 5:1--5:??
            Albert Atserias and   
                     Anuj Dawar   Degree lower bounds of tower-type for
                                  approximating formulas with parity
                                  quantifiers  . . . . . . . . . . . . . . 6:1--6:??
          Renate A. Schmidt and   
              Dmitry Tishkovsky   Using tableau to decide description
                                  logics with full role negation and
                                  identity . . . . . . . . . . . . . . . . 7:1--7:??
                       Tony Tan   Extending two-variable logic on data
                                  trees with order on data values and its
                                  automata . . . . . . . . . . . . . . . . 8:1--8:??
                     Hubie Chen   On the complexity of existential
                                  positive queries . . . . . . . . . . . . 9:1--9:??
                  Lan Zhang and   
            Ullrich Hustadt and   
                    Clare Dixon   A resolution calculus for the
                                  branching-time temporal logic CTL  . . . 10:1--10:??

ACM Transactions on Computational Logic
Volume 15, Number 2, April, 2014

            Vernon Asuncion and   
                  Yan Zhang and   
                        Yi Zhou   Preferred First-Order Answer Set
                                  Programs . . . . . . . . . . . . . . . . 11:1--11:??
               Tran Cao Son and   
            Enrico Pontelli and   
           Ngoc-Hieu Nguyen and   
                  Chiaki Sakama   Formalizing Negotiations Using Logic
                                  Programming  . . . . . . . . . . . . . . 12:1--12:??
               Cindy Eisner and   
                Dana Fisman and   
                  John Havlicek   Safety and Liveness, Weakness and
                                  Strength, and the Underlying Topological
                                  Relations  . . . . . . . . . . . . . . . 13:1--13:??
                  Yuan Feng and   
                 Yuxin Deng and   
                 Mingsheng Ying   Symbolic Bisimulation for Quantum
                                  Processes  . . . . . . . . . . . . . . . 14:1--14:??
            Benedikt Bollig and   
                Paul Gastin and   
           Benjamin Monmege and   
                   Marc Zeitoun   Pebble Weighted Automata and Weighted
                                  Logics . . . . . . . . . . . . . . . . . 15:1--15:??
      Krishnendu Chatterjee and   
                  Laurent Doyen   Partial-Observation Stochastic Games:
                                  How to Win when Belief Fails . . . . . . 16:1--16:??
            Arnold Beckmann and   
        Pavel Pudlák and   
                    Neil Thapen   Parity Games and Propositional Proofs    17:1--17:??

ACM Transactions on Computational Logic
Volume 15, Number 3, September, 2014

          Cristian Molinaro and   
                  Amy Sliva and   
             V. S. Subrahmanian   Super-Solutions: Succinctly Representing
                                  Solutions in Abductive Annotated
                                  Probabilistic Temporal Logic . . . . . . 18:1--18:??
             Nadia Creignou and   
                   Uwe Egly and   
               Johannes Schmidt   Complexity Classifications for
                                  Logic-Based Argumentation  . . . . . . . 19:1--19:??
           Markus Aschinger and   
            Conrad Drescher and   
              Georg Gottlob and   
               Heribert Vollmer   LoCo --- a Logic for Configuration
                                  Problems . . . . . . . . . . . . . . . . 20:1--20:??
              Robert J. Simmons   Structural Focalization  . . . . . . . . 21:1--21:??
             Mingsheng Ying and   
                 Yangjia Li and   
                 Nengkun Yu and   
                      Yuan Feng   Model-Checking Linear-Time Properties of
                                  Quantum Systems  . . . . . . . . . . . . 22:1--22:??
          María Poza and   
César Domínguez and   
      Jónathan Heras and   
                    Julio Rubio   A Certified Reduction Strategy for
                                  Homological Image Processing . . . . . . 23:1--23:??
             Arnaud Carayol and   
                Axel Haddad and   
                  Olivier Serre   Randomization in Automata on Infinite
                                  Trees  . . . . . . . . . . . . . . . . . 24:1--24:??
          Alessandro Artale and   
           Roman Kontchakov and   
         Vladislav Ryzhikov and   
          Michael Zakharyaschev   A Cookbook for Temporal Conceptual Data
                                  Modelling with Description Logics  . . . 25:1--25:??

ACM Transactions on Computational Logic
Volume 15, Number 4, September, 2014

         Stefan Göller and   
            Anthony Widjaja Lin   Refining the Process Rewrite Systems
                                  Hierarchy via Ground Tree Rewrite
                                  Systems  . . . . . . . . . . . . . . . . 26:1--26:??
                  Udi Boker and   
      Krishnendu Chatterjee and   
        Thomas A. Henzinger and   
                 Orna Kupferman   Temporal Specifications with
                                  Accumulative Values  . . . . . . . . . . 27:1--27:??
          Maciej Komosinski and   
                  Adam Kups and   
Dorota Leszczy\'nska-Jasion and   
             Mariusz Urba\'nski   Identifying Efficient Abductive
                                  Hypotheses Using Multicriteria Dominance
                                  Relation . . . . . . . . . . . . . . . . 28:1--28:??
            Achille Frigeri and   
           Liliana Pasquale and   
                Paola Spoletini   Fuzzy Time in Linear Temporal Logic  . . 30:1--30:??
         Gerhard Schellhorn and   
               John Derrick and   
                 Heike Wehrheim   A Sound and Complete Proof Technique for
                                  Linearizability of Concurrent Data
                                  Structures . . . . . . . . . . . . . . . 31:1--31:??
           Fabrizio Riguzzi and   
                 Terrance Swift   Terminating Evaluation of Logic Programs
                                  with Finite Three-Valued Models  . . . . 32:1--32:??
          Damiano Zanardini and   
                   Samir Genaim   Inference of Field-Sensitive
                                  Reachability and Cyclicity . . . . . . . 33:1--33:??
             Fabio Mogavero and   
             Aniello Murano and   
           Giuseppe Perelli and   
                 Moshe Y. Vardi   Reasoning About Strategies: On the
                                  Model-Checking Problem . . . . . . . . . 34:1--34:??
             Filippo Bonchi and   
             Fabio Gadducci and   
     Giacoma Valentina Monreale   A General Theory of Barbs, Contexts, and
                                  Labels . . . . . . . . . . . . . . . . . 35:1--35:??


ACM Transactions on Computational Logic
Volume 16, Number 1, March, 2015

          Shulamit Halamish and   
                 Orna Kupferman   Minimizing Deterministic Lattice
                                  Automata . . . . . . . . . . . . . . . . 1:1--1:??
               Silvia Crafa and   
              Francesco Ranzato   Logical Characterizations of Behavioral
                                  Relations on Transition Systems of
                                  Probability Distributions  . . . . . . . 2:1--2:??
                    Jia Tao and   
              Giora Slutzki and   
                 Vasant Honavar   A Conceptual Framework for
                                  Secrecy-preserving Reasoning in
                                  Knowledge Bases  . . . . . . . . . . . . 3:1--3:??
                 M. Biscaia and   
               D. Henriques and   
                      P. Mateus   Decidability of Approximate Skolem
                                  Problem and Applications to Logical
                                  Verification of Dynamical Properties of
                                  Markov Chains  . . . . . . . . . . . . . 4:1--4:??
           Agata Ciabattoni and   
                  Ori Lahav and   
              Lara Spendier and   
                  Anna Zamansky   Taming Paraconsistent (and Other)
                                  Logics: an Algorithmic Approach  . . . . 5:1--5:??
                   Guy Avni and   
                 Orna Kupferman   Parameterized Weighted Containment . . . 6:1--6:??
           Gaëlle Fontaine   Why Is It Hard to Obtain a Dichotomy for
                                  Consistent Query Answering?  . . . . . . 7:1--7:??
              Mauro Ferrari and   
         Camillo Fiorentini and   
                  Guido Fiorino   An Evaluation-Driven Decision Procedure
                                  for G3i  . . . . . . . . . . . . . . . . 8:1--8:??
         Stefan Göller and   
        Jean-Christoph Jung and   
                  Markus Lohrey   The Complexity of Decomposing Modal and
                                  First-Order Theories . . . . . . . . . . 9:1--9:??

ACM Transactions on Computational Logic
Volume 16, Number 2, February, 2015

            Jakob Grue Simonsen   A Confluent Rewriting System Having No
                                  Computable, One-Step, Normalizing
                                  Strategy . . . . . . . . . . . . . . . . 10:1--10:??
     Anastasios Skarlatidis and   
         Georgios Paliouras and   
          Alexander Artikis and   
               George A. Vouros   Probabilistic Event Calculus for Event
                                  Recognition  . . . . . . . . . . . . . . 11:1--11:??
         Roberto Sebastiani and   
                  Silvia Tomasi   Optimization Modulo Theories with Linear
                                  Rational Costs . . . . . . . . . . . . . 12:1--12:??
      Jean-Pierre Jouannaud and   
                   Albert Rubio   Normal Higher-Order Termination  . . . . 13:1--13:??
        Bertram Felgenhauer and   
            Aart Middeldorp and   
               Harald Zankl and   
            Vincent Van Oostrom   Layer Systems for Proving Confluence . . 14:1--14:??
      Stéphane Demri and   
                  Morgan Deters   Two-Variable Separation Logic and Its
                                  Inner Circle . . . . . . . . . . . . . . 15:1--15:??
           Pierre Genev\`es and   
           Nabil Laya\"\ida and   
               Alan Schmitt and   
                   Nils Gesbert   Efficiently Deciding $ \mu $-Calculus
                                  with Converse over Finite Trees  . . . . 16:1--16:??
          Eryk Kopczy\'nski and   
                       Tony Tan   On the Variable Hierarchy of First-Order
                                  Spectra  . . . . . . . . . . . . . . . . 17:1--17:??
              Nicolai Kraus and   
              Christian Sattler   Higher Homotopies in a Hierarchy of
                                  Univalent Universes  . . . . . . . . . . 18:1--18:??

ACM Transactions on Computational Logic
Volume 16, Number 3, July, 2015

          Novak Novakovi\'c and   
         Lutz Straßburger   On the Power of Substitution in the
                                  Calculus of Structures . . . . . . . . . 19:1--19:??
              Ranko Lazi\'c and   
                Sylvain Schmitz   Nonelementary Complexities for Branching
                                  VASS, MELL, and Extensions . . . . . . . 20:1--20:??
         Christoph Berkholz and   
              Andreas Krebs and   
                 Oleg Verbitsky   Bounds for the Quantifier Depth in
                                  Finite-Variable Logics: Alternation
                                  Hierarchy  . . . . . . . . . . . . . . . 21:1--21:??
           Bettina Fazzinga and   
              Sergio Flesca and   
               Francesco Parisi   On the Complexity of Probabilistic
                                  Abstract Argumentation Frameworks  . . . 22:1--22:??
     Peter Lefanu Lumsdaine and   
              Michael A. Warren   The Local Universes Model: an Overlooked
                                  Coherence Construction for Dependent
                                  Type Theories  . . . . . . . . . . . . . 23:1--23:??
         Marijn J. H. Heule and   
                 Stefan Szeider   A SAT Approach to Clique-Width . . . . . 24:1--24:??
        Massimo Benerecetti and   
             Fabio Mogavero and   
                 Aniello Murano   Reasoning About Substructures and Games  25:1--25:??
                 Andrea Asperti   Computational Complexity Via Finite
                                  Types  . . . . . . . . . . . . . . . . . 26:1--26:??
        Christopher Hampson and   
                     Agi Kurucz   Undecidable Propositional Bimodal Logics
                                  and One-Variable First-Order Linear
                                  Temporal Logics with Counting  . . . . . 27:1--27:??

ACM Transactions on Computational Logic
Volume 16, Number 4, November, 2015

               Yuval Filmus and   
             Massimo Lauria and   
               Mladen Miksa and   
       Jakob Nordström and   
                   Marc Vinyals   From Small Space to Small Width in
                                  Resolution . . . . . . . . . . . . . . . 28:1--28:??
              Sjoerd Cranen and   
               Maciej Gazda and   
           Wieger Wesselink and   
             Tim A. C. Willemse   Abstraction in Fixpoint Logic  . . . . . 29:1--29:??
           Hitoshi Furusawa and   
                   Georg Struth   Concurrent Dynamic Algebra . . . . . . . 30:1--30:??
                   Zhe Wang and   
                 Kewen Wang and   
                   Rodney Topor   DL-Lite Ontology Revision Based on An
                                  Alternative Semantic Characterization    31:1--31:??
             Daniel G. Schwartz   Dynamic Reasoning Systems  . . . . . . . 32:1--32:??
           Enrico Marchioni and   
             Michael Wooldridge   Lukasiewicz Games: a Logic-Based
                                  Approach to Quantitative Strategic
                                  Interactions . . . . . . . . . . . . . . 33:1--33:??
           Oliver Friedmann and   
             Felix Klaedtke and   
                   Martin Lange   Ramsey-Based Inclusion Checking for
                                  Visibly Pushdown Automata  . . . . . . . 34:1--34:??
                   Simon Kramer   Logic of Intuitionistic Interactive
                                  Proofs (Formal Theory of Perfect
                                  Knowledge Transfer)  . . . . . . . . . . 35:1--35:??
             Arnaud Carayol and   
                Axel Haddad and   
                  Olivier Serre   Erratum for ``Randomization in Automata
                                  on Infinite Trees''  . . . . . . . . . . 36:1--36:??


ACM Transactions on Computational Logic
Volume 17, Number 1, December, 2015

           André Platzer   Differential Game Logic  . . . . . . . . 1:1--1:??
          Jakub Michaliszyn and   
                   Jan Otop and   
            Emanuel Kiero\'nski   On the Decidability of Elementary Modal
                                  Logics . . . . . . . . . . . . . . . . . 2:1--2:??
Rémy Chrétien and   
   Véronique Cortier and   
       Stéphanie Delaune   From Security Protocols to Pushdown
                                  Automata . . . . . . . . . . . . . . . . 3:1--3:??
          Serenella Cerrito and   
        Amélie David and   
               Valentin Goranko   Optimal Tableau Method for Constructive
                                  Satisfiability Testing and Model
                                  Synthesis in the Alternating-Time
                                  Temporal Logic ATL+  . . . . . . . . . . 4:1--4:??
                   Florian Rabe   Lax Theory Morphisms . . . . . . . . . . 5:1--5:??
         K. Rustan M. Leino and   
                    Paqui Lucio   An Assertional Proof of the Stability
                                  and Correctness of Natural Mergesort . . 6:1--6:22
         Johannes K. Fichte and   
                 Stefan Szeider   Backdoors to Normality for Disjunctive
                                  Logic Programs . . . . . . . . . . . . . 7:1--7:??

ACM Transactions on Computational Logic
Volume 17, Number 2, March, 2016

           Michael Benedikt and   
            Balder Ten Cate and   
            Michael Vanden Boom   Effective Interpolation and Preservation
                                  in Guarded Logics  . . . . . . . . . . . 8:1--8:??
               Paolo Liberatore   Belief Merging by Examples . . . . . . . 9:1--9:??
                Simone Bova and   
              Robert Ganian and   
                 Stefan Szeider   Model Checking Existential Logic on
                                  Partially Ordered Sets . . . . . . . . . 10:1--10:??
              Elvira Albert and   
     Antonio Flores-Montoya and   
               Samir Genaim and   
          Enrique Martin-Martin   May-Happen-in-Parallel Analysis for
                                  Actor-Based Concurrency  . . . . . . . . 11:1--11:??
             Stephane Demri and   
                  Morgan Deters   Expressive Completeness of Separation
                                  Logic with Two Variables and No
                                  Separating Conjunction . . . . . . . . . 12:1--12:??
          Konstantinos Mamouras   The Hoare Logic of Deterministic and
                                  Nondeterministic Monadic Recursion
                                  Schemes  . . . . . . . . . . . . . . . . 13:1--13:??
           Michael Benedikt and   
                    Clemens Ley   Limiting Until in Ordered Tree Query
                                  Languages  . . . . . . . . . . . . . . . 14:1--14:??

ACM Transactions on Computational Logic
Volume 17, Number 3, July, 2016

             Brijesh Dongol and   
               Ian J. Hayes and   
                   Georg Struth   Convolution as a Unifying Concept:
                                  Applications in Separation Logic,
                                  Interval Calculi, and Concurrency  . . . 15:1--15:??
              Ranko Lazi\'c and   
         Joël Ouaknine and   
                  James Worrell   Zeno, Hercules, and the Hydra: Safety
                                  Metric Temporal Logic is
                                  Ackermann-Complete . . . . . . . . . . . 16:1--16:??
           Agata Ciabattoni and   
            Revantha Ramanayake   Power and Limits of Structural Display
                                  Rules  . . . . . . . . . . . . . . . . . 17:1--17:??
            Wlodzimierz Drabent   Correctness and Completeness of Logic
                                  Programs . . . . . . . . . . . . . . . . 18:1--18:??
            Albert Atserias and   
             Massimo Lauria and   
           Jakob Nordström   Narrow Proofs May Be Maximally Long  . . 19:1--19:??
             Nadia Creignou and   
               Odile Papini and   
        Stefan Rümmele and   
                 Stefan Woltran   Belief Merging within Fragments of
                                  Propositional Logic  . . . . . . . . . . 20:1--20:??
                    Adam Trybus   Rational Region-Based Affine Logic of
                                  the Real Plane . . . . . . . . . . . . . 21:1--21:??
                   Lian Wen and   
                 Kewen Wang and   
               Yi-Dong Shen and   
                   Fangzhen Lin   A Model for Phase Transition of Random
                                  Answer-Set Programs  . . . . . . . . . . 22:1--22:??

ACM Transactions on Computational Logic
Volume 17, Number 4, November, 2016

               Rohit Chadha and   
             Vincent Cheval and   
       Stefan Ciobâca and   
                   Steve Kremer   Automated Verification of Equivalence
                                  Properties of Cryptographic Protocols    23:1--23:??
        Alessandro Facchini and   
               Filip Murlak and   
              Michal Skrzypczak   Index Problems for Game Automata . . . . 24:1--24:??
          Michael Elberfeld and   
               Martin Grohe and   
                    Till Tantau   Where First-Order and Monadic
                                  Second-Order Logic Coincide  . . . . . . 25:1--25:??
           Lorenzo Carlucci and   
              Nicola Galesi and   
                 Massimo Lauria   On the Proof Complexity of
                                  Paris--Harrington and Off-Diagonal
                                  Ramsey Tautologies . . . . . . . . . . . 26:1--26:??
              Bart Bogaerts and   
            Joost Vennekens and   
                  Marc Denecker   On Well-Founded Set-Inductions and
                                  Locally Monotone Operators . . . . . . . 27:1--27:??
           Hitoshi Furusawa and   
                   Georg Struth   Taming Multirelations  . . . . . . . . . 28:1--28:??
              Kristina Sojakova   The Equivalence of the Torus and the
                                  Product of Two Circles in Homotopy Type
                                  Theory . . . . . . . . . . . . . . . . . 29:1--29:??
            Aleksy Schubert and   
             Pawel Urzyczyn and   
    Daria Walukiewicz-Chrzaszcz   How Hard Is Positive Quantification? . . 30:1--30:??
          Witold Charatonik and   
                Piotr Witkowski   Two-Variable Logic with Counting and
                                  Trees  . . . . . . . . . . . . . . . . . 31:1--31:??
               Saguy Benaim and   
           Michael Benedikt and   
          Witold Charatonik and   
        Emanuel Kiero\'nski and   
         Rastislav Lenhardt and   
           Filip Mazowiecki and   
                  James Worrell   Complexity of Two-Variable Logic on
                                  Finite Trees . . . . . . . . . . . . . . 32:1--32:??


ACM Transactions on Computational Logic
Volume 18, Number 1, April, 2017

           Martin Lück and   
                 Arne Meier and   
                Irena Schindler   Parametrised Complexity of
                                  Satisfiability in Temporal Logic . . . . 1:1--1:??
              Petar Dapi\'c and   
           Petar Markovi\'c and   
                 Barnaby Martin   Quantified Constraint Satisfaction
                                  Problem on Semicomplete Digraphs . . . . 2:1--2:??
             Kensuke Kojima and   
               Atsushi Igarashi   A Hoare Logic for GPU Kernels  . . . . . 3:1--3:??
               Davide Sangiorgi   Equations, Contractions, and Unique
                                  Solutions  . . . . . . . . . . . . . . . 4:1--4:??
             Tom J. Ameloot and   
                Bas Ketsman and   
                Frank Neven and   
                    Daniel Zinn   Datalog Queries Distributing over
                                  Components . . . . . . . . . . . . . . . 5:1--5:??
               Adrian Haret and   
        Stefan Rümmele and   
                 Stefan Woltran   Merging in the Horn Fragment . . . . . . 6:1--6:??
         Isabella Mastroeni and   
              Damiano Zanardini   Abstract Program Slicing: an Abstract
                                  Interpretation-Based Approach to Program
                                  Slicing  . . . . . . . . . . . . . . . . 7:1--7:??

ACM Transactions on Computational Logic
Volume 18, Number 2, June, 2017

          Szymon Chlebowski and   
          Maciej Komosinski and   
                      Adam Kups   Automated Generation of Erotetic Search
                                  Scenarios: Classification, Optimization,
                                  and Knowledge Extraction . . . . . . . . 8:1--8:??
                 Heng Zhang and   
                      Yan Zhang   Expressiveness of Logic Programs under
                                  the General Stable Model Semantics . . . 9:1--9:??
       Pablo Barceló and   
             Pablo Muñoz   Graph Logics with Rational Relations:
                                  The Role of Word Combinatorics . . . . . 10:1--10:??
            Arnold Beckmann and   
                       Sam Buss   The NP Search Problems of Frege and
                                  Extended Frege Proofs  . . . . . . . . . 11:1--11:??
            Przemyslaw Daca and   
        Thomas A. Henzinger and   
Jan Kretínský and   
                 Tatjana Petrov   Faster Statistical Model Checking for
                                  Unbounded Temporal Properties  . . . . . 12:1--12:??
           Jan Friso Groote and   
            David N. Jansen and   
        Jeroen J. A. Keiren and   
                  Anton J. Wijs   An $ O(m \log n) $ Algorithm for
                                  Computing Stuttering Equivalence and
                                  Branching Bisimulation . . . . . . . . . 13:1--13:??
               Carsten Fuhs and   
                Cynthia Kop and   
                  Naoki Nishida   Verifying Procedural Programs via
                                  Constrained Rewriting Induction  . . . . 14:1--14:??
                Che-Ping Su and   
              Tuan-Fang Fan and   
                Churn-Jung Liau   Possibilistic Justification Logic:
                                  Reasoning About Justified Uncertain
                                  Beliefs  . . . . . . . . . . . . . . . . 15:1--15:??
           Denis Ponomaryov and   
            Mikhail Soutchanski   Progression of Decomposed Local-Effect
                                  Action Theories  . . . . . . . . . . . . 16:1--16:??
      Nicholas R. Radcliffe and   
          Luis F. T. Moraes and   
                Rakesh M. Verma   Uniqueness of Normal Forms for Shallow
                                  Term Rewrite Systems . . . . . . . . . . 17:1--17:??

ACM Transactions on Computational Logic
Volume 18, Number 3, August, 2017

          George Barmpalias and   
             Douglas Cenzer and   
          Christopher P. Porter   The Probability of a Computable Output
                                  from a Random Oracle . . . . . . . . . . 18:1--18:??
           André Platzer   Differential Hybrid Games  . . . . . . . 19:1--19:??
    Nathanaël Fijalkow and   
               Charles Paperman   Monadic Second-Order Logic with
                                  Arbitrary Monadic Predicates . . . . . . 20:1--20:??
             Ronald De Haan and   
                  Iyad Kanj and   
                 Stefan Szeider   On the Parameterized Complexity of
                                  Finding Small Unsatisfiable Subsets of
                                  CNF Formulas and CSP Instances . . . . . 21:1--21:??
            Davide Bresolin and   
                 Agi Kurucz and   
Emilio Muñoz-Velasco and   
         Vladislav Ryzhikov and   
            Guido Sciavicco and   
          Michael Zakharyaschev   Horn Fragments of the Halpern--Shoham
                                  Interval Temporal Logic  . . . . . . . . 22:1--22:??
            Manuel Bodirsky and   
              Peter Jonsson and   
                 Trung Van Pham   The Complexity of Phylogeny Constraint
                                  Satisfaction Problems  . . . . . . . . . 23:1--23:??
            Michael Blondin and   
               Alain Finkel and   
            Christoph Haase and   
                   Serge Haddad   The Logical View on Continuous Petri
                                  Nets . . . . . . . . . . . . . . . . . . 24:1--24:??
              Matthew Hague and   
        Andrzej S. Murawski and   
             C.-H. Luke Ong and   
                  Olivier Serre   Collapsible Pushdown Automata and
                                  Recursion Schemes  . . . . . . . . . . . 25:1--25:??

ACM Transactions on Computational Logic
Volume 18, Number 4, December, 2017

         Sebastian Eberhard and   
              Gabriel Ebner and   
                   Stefan Hetzl   Algorithmic Compression of Finite Tree
                                  Languages by Rigid Acyclic Grammars  . . 26:1--26:??
          Shqiponja Ahmetaj and   
            Diego Calvanese and   
            Magdalena Ortiz and   
                  Mantas Simkus   Managing Change in Graph-Structured Data
                                  Using Description Logics . . . . . . . . 27:1--27:??
             Marco Calautti and   
               Sergio Greco and   
               Irina Trubitsyna   Detecting Decidable Classes of Finitely
                                  Ground Logic Programs with Function
                                  Symbols  . . . . . . . . . . . . . . . . 28:1--28:??
                 Hubie Chen and   
             Moritz Müller   One Hierarchy Spawns Another: Graph
                                  Deconstructions and the Complexity
                                  Classification of Conjunctive Queries    29:1--29:??
              Andreas Krebs and   
               Howard Straubing   An Effective Characterization of the
                                  Alternation Hierarchy in Two-Variable
                                  Logic  . . . . . . . . . . . . . . . . . 30:1--30:??
      Krishnendu Chatterjee and   
        Thomas A. Henzinger and   
                       Jan Otop   Nested Weighted Automata . . . . . . . . 31:1--31:??
               Pavel Naumov and   
                        Jia Tao   Information Flow under Budget
                                  Constraints  . . . . . . . . . . . . . . 32:1--32:??
             Kord Eickmeyer and   
          Michael Elberfeld and   
               Frederik Harwath   Succinctness of Order-Invariant Logics
                                  on Depth-Bounded Structures  . . . . . . 33:1--33:??


ACM Transactions on Computational Logic
Volume 19, Number 1, February, 2018

           Olaf Beyersdorff and   
                 Leroy Chew and   
              Meena Mahajan and   
                    Anil Shukla   Are Short Proofs Narrow? QBF Resolution
                                  Is Not So Simple . . . . . . . . . . . . 1:1--1:??
              Miika Hannula and   
              Juha Kontinen and   
              Jonni Virtema and   
               Heribert Vollmer   Complexity of Propositional Logics in
                                  Team Semantic  . . . . . . . . . . . . . 2:1--2:??
              Steffen Van Bakel   Characterisation of Normalisation
                                  Properties for $ \lambda \mu $ using
                                  Strict Negated Intersection Types  . . . 3:1--3:??
         Lutz Schröder and   
                     Yde Venema   Completeness of Flat Coalgebraic
                                  Fixpoint Logics  . . . . . . . . . . . . 4:1--4:??
        Andrea Aler Tubella and   
              Alessio Guglielmi   Subatomic Proof Systems: Splittable
                                  Systems  . . . . . . . . . . . . . . . . 5:1--5:??
         Elliot Fairweather and   
       Maribel Fernández   Typed Nominal Rewriting  . . . . . . . . 6:1--6:??