Journal of Automated Reasoning, Volume 49

Volume 49, Number 1, June 2012

• 
  Liang Chang, Zhongzhi Shi, Tianlong Gu, Lingzhong Zhao:
  A Family of Dynamic Description Logics for Representing and Reasoning About Actions. 1-52
• 
  Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann:
  SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. 53-93
• 
  Alexander Krauss, Tobias Nipkow:
  Proof Pearl: Regular Expression Equivalence and Relation Algebra. 95-106
• 
  Freek Wiedijk:
  "Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009. 107-109

Volume 49, Number 2, August 2012

Special Issue: Theory and Applications of Abstraction, Substitution and Naming

• 
  Maribel Fernández, Christian Urban:
  Preface: Theory and Applications of Abstraction, Substitution and Naming. 111-114
• 
  Matthew R. Lakin, Andrew M. Pitts:
  Encoding Abstract Syntax Without Fresh Names. 115-140
• 
  Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride:
  Strongly Typed Term Representations in Coq. 141-159
• 
  Filippo Bonchi, Maria Grazia Buscemi, Vincenzo Ciancia, Fabio Gadducci:
  A Presheaf Environment for the Explicit Fusion Calculus. 161-183
• 
  Randy Pollack, Masahiko Sato, Wilmer Ricciotti:
  A Canonical Locally Named Representation of Binding. 185-207
• 
  James Cheney, Michael Norrish, René Vestergaard:
  Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. 209-239
• 
  Andrew Gacek, Dale Miller, Gopalan Nadathur:
  A Two-Level Logic Approach to Reasoning About Computations. 241-273
• 
  Kristoffer Høgsbro Rose, Roel Bloo, Frédéric Lang:
  On Explicit Substitution with Names. 275-300

Volume 49, Number 3, October 2012

Special Issue: The POPLmark Challenge

• 
  Benjamin C. Pierce, Stephanie Weirich:
  Preface. 301-302
• 
  Stefan Berghofer:
  A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL. 303-326
• 
  Jérôme Vouillon:
  A Solution to the PoplMark Challenge Based on de Bruijn Indices. 327-362
• 
  Arthur Charguéraud:
  The Locally Nameless Representation. 363-408
• 
  André Hirschowitz, Marco Maggesi:
  Nested Abstract Syntax in Coq. 409-426
• 
  Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi:
  Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. 427-451
• 
  Andrew W. Appel, Robert Dockins, Xavier Leroy:
  A List-Machine Benchmark for Mechanized Metatheory. 453-491

Volume 49, Number 4, December 2012

• 
  Steven Schockaert, Jeroen Janssen, Dirk Vermeir:
  Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction. 493-550
• 
  Jia Tao, Giora Slutzki, Vasant G. Honavar:
  PSPACE Tableau Algorithms for Acyclic Modalized $\boldsymbol{\mathcal{ALC}}$. 551-582
• 
  Matti Järvisalo, Armin Biere, Marijn Heule:
  Simulating Circuit-Level Simplifications on CNF. 583-619