


default search action
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
- 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
- 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.