Table of contents for issues of Journal of Automated Reasoning

Last update: Mon Nov 27 10:42:08 MST 2023                Valid HTML 3.2!

Volume 1, Number 1, March, 1985
Volume 1, Number 2, June, 1985
Volume 1, Number 3, September, 1985
Volume 1, Number 4, December, 1985
Volume 2, Number 1, March, 1986
Volume 2, Number 2, June, 1986
Volume 2, Number 3, September, 1986
Volume 2, Number 4, December, 1986
Volume 3, Number 1, March, 1987
Volume 3, Number 2, June, 1987
Volume 3, Number 3, September, 1987
Volume 3, Number 4, December, 1987
Volume 4, Number 1, March, 1988
Volume 4, Number 2, June, 1988
Volume 4, Number 3, September, 1988
Volume 4, Number 4, December, 1988
Volume 5, Number 1, March, 1989
Volume 5, Number 2, June, 1989
Volume 5, Number 3, September, 1989
Volume 5, Number 4, December, 1989
Volume 6, Number 1, March, 1990
Volume 6, Number 2, June, 1990
Volume 6, Number 3, September, 1990
Volume 6, Number 4, December, 1990
Volume 7, Number 1, March, 1991
Volume 7, Number 2, June, 1991
Volume 7, Number 3, September, 1991
Volume 7, Number 4, December, 1991
Volume 8, Number 1, February, 1992
Volume 8, Number 2, April, 1992
Volume 8, Number 3, June, 1992
Volume 9, Number 1, August, 1992
Volume 9, Number 2, October, 1992
Volume 9, Number 3, December, 1992
Volume 10, Number 1, February, 1993
Volume 10, Number 2, June, 1993
Volume 10, Number 3, October, 1993
Volume 11, Number 1, February, 1993
Volume 11, Number 2, June, 1993
Volume 11, Number 3, October, 1993
Volume 12, Number 1, February, 1994
Volume 12, Number 2, June, 1994
Volume 12, Number 3, October, 1994
Volume 13, Number 1, February, 1994
Volume 13, Number 2, June, 1994
Volume 13, Number 3, October, 1994
Volume 14, Number 1, February, 1995
Volume 14, Number 2, June, 1995
Volume 14, Number 3, October, 1995
Volume 15, Number 1, February, 1995
Volume 15, Number 2, June, 1995
Volume 15, Number 3, October, 1995
Volume 16, Number 1--2, March, 1996
Volume 16, Number 3, June, 1996
Volume 17, Number 1, August, 1996
Volume 17, Number 2, October, 1996
Volume 17, Number 3, December, 1996
Volume 18, Number 1, February, 1997
Volume 18, Number 2, April, 1997
Volume 18, Number 3, June, 1997
Volume 19, Number 1, August, 1997
Volume 19, Number 2, October, 1997
Volume 19, Number 3, December, 1997
Volume 20, Number 1--2, April, 1998
Volume 20, Number 3, June, 1998
Volume 21, Number 1, August, 1998
Volume 21, Number 2, October, 1998
Volume 21, Number 3, December, 1998
Volume 22, Number 1, January, 1999
Volume 22, Number 2, February, 1999
Volume 22, Number 3, March, 1999
Volume 22, Number 4, May, 1999
Volume 23, Number 1, July, 1999
Volume 23, Number 2, August, 1999
Volume 23, Number 3, November, 1999
Volume 24, Number 1--2, February, 2000
Volume 24, Number 3, April, 2000
Volume 24, Number 4, May, 2000
Volume 25, Number 1, July, 2000
Volume 25, Number 2, August, 2000
Volume 25, Number 3, October, 2000
Volume 25, Number 4, November, 2000
Volume 26, Number 1, January, 2001
Volume 26, Number 2, February, 2001
Volume 26, Number 3, April, 2001
Volume 26, Number 4, May, 2001
Volume 27, Number 1, July, 2001
Volume 27, Number 2, August, 2001
Volume 27, Number 3, October, 2001
Volume 27, Number 4, November, 2001
Volume 28, Number 1, January, 2002
Volume 28, Number 2, February, 2002
Volume 28, Number 3, April, 2002
Volume 28, Number 4, May, 2002
Volume 29, Number 1, January, 2002
Volume 29, Number 2, February, 2002
Volume 29, Number 3--4, September, 2002
Volume 30, Number 1, January, 2003
Volume 30, Number 2, February, 2003
Volume 30, Number 3--4, May, 2003
Volume 31, Number 1, September, 2003
Volume 31, Number 2, October, 2003
Volume 31, Number 3--4, November, 2003
Volume 32, Number 1, January, 2004
Volume 32, Number 2, February, 2004
Volume 32, Number 3, February, 2004
Volume 32, Number 4, December, 2004
Volume 33, Number 1, July, 2004
Volume 33, Number 2, September, 2004
Volume 33, Number 3--4, October / December, 2004
Volume 34, Number 1, January, 2005
Volume 34, Number 2, December, 2005
Volume 34, Number 3, April, 2005
Volume 34, Number 4, May, 2005
Volume 35, Number 1--3, October, 2005
Volume 35, Number 4, November, 2005
Volume 36, Number 1--2, January, 2006
Volume 36, Number 3, April, 2006
Volume 36, Number 4, April, 2006
Volume 37, Number 1--2, August, 2006
Volume 37, Number 3, October, 2006
Volume 37, Number 4, November, 2006
Volume 38, Number 1--3, April, 2007
Volume 38, Number 4, May, 2007
Volume 39, Number 1, July, 2007
Volume 39, Number 2, August, 2007
Volume 39, Number 3, October, 2007
Volume 39, Number 4, December, 2007
Volume 40, Number 1, January, 2008
Volume 40, Number 2--3, March, 2008
Volume 40, Number 4, May, 2008
Volume 41, Number 1, July, 2008
Volume 41, Number 2, August, 2008
Volume 41, Number 3--4, November, 2008
Volume 42, Number 1, January, 2009
Volume 42, Number 2--4, April, 2009
Volume 43, Number 1, June, 2009
Volume 43, Number 2, August, 2009
Volume 43, Number 3, October, 2009
Volume 43, Number 4, December, 2009
Volume 44, Number 1--2, February, 2010
Volume 44, Number 3, March, 2010
Volume 44, Number 4, April, 2010
Volume 45, Number 1, June, 2010
Volume 45, Number 2, August, 2010
Volume 45, Number 3, October, 2010
Volume 45, Number 4, December, 2010
Volume 46, Number 1, January, 2011
Volume 46, Number 2, February, 2011
Volume 46, Number 3--4, April, 2011
Volume 47, Number 1, June, 2011
Volume 47, Number 2, August, 2011
Volume 47, Number 3, October, 2011
Volume 47, Number 4, December, 2011
Volume 48, Number 1, January, 2012
Volume 48, Number 2, February, 2012
Volume 48, Number 3, March, 2012
Volume 48, Number 4, April, 2012
Volume 49, Number 1, June, 2012
Volume 49, Number 2, August, 2012
Volume 49, Number 3, October, 2012
Volume 49, Number 4, December, 2012
Volume 50, Number 1, January, 2013
Volume 50, Number 2, February, 2013
Volume 50, Number 3, March, 2013
Volume 50, Number 4, April, 2013
Volume 51, Number 1, June, 2013
Volume 51, Number 2, August, 2013
Volume 51, Number 3, October, 2013
Volume 51, Number 4, December, 2013
Volume 52, Number 1, January, 2014
Volume 52, Number 2, February, 2014
Volume 52, Number 3, March, 2014
Volume 52, Number 4, April, 2014
Volume 53, Number 1, June, 2014
Volume 53, Number 2, August, 2014
Volume 53, Number 3, October, 2014
Volume 53, Number 4, December, 2014
Volume 54, Number 1, January, 2015
Volume 54, Number 2, February, 2015
Volume 54, Number 3, March, 2015
Volume 54, Number 4, April, 2015
Volume 55, Number 1, June, 2015
Volume 55, Number 2, August, 2015
Volume 55, Number 3, October, 2015
Volume 55, Number 4, December, 2015
Volume 56, Number 1, January, 2016
Volume 56, Number 2, February, 2016
Volume 56, Number 3, March, 2016
Volume 56, Number 4, April, 2016
Volume 57, Number 1, June, 2016
Volume 57, Number 2, August, 2016
Volume 57, Number 3, October, 2016
Volume 57, Number 4, December, 2016
Volume 58, Number 1, January, 2017
Volume 58, Number 2, February, 2017
Volume 58, Number 3, March, 2017
Volume 58, Number 4, April, 2017
Volume 59, Number 1, June, 2017
Volume 59, Number 2, August, 2017
Volume 59, Number 3, October, 2017
Volume 59, Number 4, December, 2017
Volume 60, Number 1, January, 2018
Volume 60, Number 2, February, 2018
Volume 60, Number 3, March, 2018
Volume 60, Number 4, April, 2018
Volume 61, Number 1--4, June, 2018
Volume 62, Number 1, January, 2019
Volume 62, Number 2, February, 2019
Volume 62, Number 3, March, 2019
Volume 62, Number 4, April, 2019
Volume 63, Number 1, June, 2019
Volume 63, Number 2, August, 2019
Volume 63, Number 3, October, 2019
Volume 63, Number 4, December, 2019
Volume 64, Number 1, January, 2020
Volume 64, Number 2, February, 2020
Volume 64, Number 3, March, 2020
Volume 64, Number 4, April, 2020
Volume 64, Number 5, June, 2020
Volume 64, Number 6, August, 2020
Volume 64, Number 7, October, 2020
Volume 64, Number 8, December, 2020
Volume 65, Number 1, January, 2021
Volume 65, Number 2, February, 2021
Volume 65, Number 3, March, 2021
Volume 65, Number 4, April, 2021
Volume 65, Number 5, June, 2021
Volume 65, Number 6, August, 2021
Volume 65, Number 7, October, 2021
Volume 65, Number 8, December, 2021
Volume 66, Number 1, February, 2022
Volume 66, Number 2, May, 2022
Volume 66, Number 3, August, 2022
Volume 66, Number 4, November, 2022
Volume 67, Number 1, March, 2023
Volume 67, Number 2, June, 2023
Volume 67, Number 3, September, 2023
Volume 67, Number 4, December, 2023


Journal of Automated Reasoning
Volume 1, Number 1, March, 1985

                      Larry Wos   Editorial: A journal is born . . . . . . 1--3
                     L. Wos and   
           Fernando Pereira and   
                Robert Hong and   
            Robert S. Boyer and   
          J. Strother Moore and   
              W. W. Bledsoe and   
             L. J. Henschen and   
          Bruce G. Buchanan and   
           Graham Wrightson and   
                  Cordell Green   An overview of automated reasoning and
                                  related fields . . . . . . . . . . . . . 5--48
               James S. Bennett   ROGET: A knowledge-based system for
                                  acquiring the conceptual structure of a
                                  diagnostic expert system . . . . . . . . 49--74
             Christian Lengauer   On the role of automated theorem proving
                                  in the compile-time derivation of
                                  concurrency  . . . . . . . . . . . . . . 75--101
                 Ewing Lusk and   
                  Ross Overbeek   Non-horn problems  . . . . . . . . . . . 103--114

Journal of Automated Reasoning
Volume 1, Number 2, June, 1985

             David M. Russinoff   An experiment with the Boyer--Moore
                                  theorem prover: A proof of Wilson's
                                  theorem  . . . . . . . . . . . . . . . . 121--139
                Adnan Yahya and   
           Lawrence J. Henschen   Deduction in non-Horn databases  . . . . 141--160
         Peter E. Friedland and   
                   Yumi Iwasaki   The concept and implementation of
                                  skeletal plans . . . . . . . . . . . . . 161--208
                 E. L. Lusk and   
                 R. A. Overbeek   Reasoning about equality . . . . . . . . 209--228
                      Anonymous   Announcements  . . . . . . . . . . . . . 229--229
                      Anonymous   Changes of address . . . . . . . . . . . 230--230

Journal of Automated Reasoning
Volume 1, Number 3, September, 1985

             William McCune and   
              Lawrence Henschen   Experiments with semantic paramodulation 231--261
                     Alan Bundy   Incidence calculus: A mechanism for
                                  probabilistic reasoning  . . . . . . . . 263--283
            R. L. Constable and   
             T. B. Knoblock and   
                    J. L. Bates   Writing programs that construct proofs   285--326
              H. J. Ohlbach and   
             M. Schmidt-Schauss   The lion and the unicorn . . . . . . . . 327--332

Journal of Automated Reasoning
Volume 1, Number 4, December, 1985

                Mark E. Stickel   Automated deduction by theory resolution 333--355
                John G. Mauceri   Robot selection expert `Rose'  . . . . . 357--390
                      Jon Doyle   Circumscription and implicit
                                  definability . . . . . . . . . . . . . . 391--405
                     N. Shankar   Towards mechanical metamathematics . . . 407--434
       Hans Jürgen Ohlbach   Predicate logic hacker tricks  . . . . . 435--440
                      Anonymous   Announcement . . . . . . . . . . . . . . 441--441


Journal of Automated Reasoning
Volume 2, Number 1, March, 1986

          Bruce D. Parrello and   
             Waldo C. Kabat and   
                         L. Wos   Job-shop scheduling using automated
                                  reasoning: A case study of the
                                  car-sequencing problem . . . . . . . . . 1--42
              Werner Dilger and   
                   Agnes Janson   Intelligent backtracking in deduction
                                  systems by means of extended unification
                                  graphs . . . . . . . . . . . . . . . . . 43--62
            Lawrence C. Paulson   Proving termination of normalization
                                  functions for conditional expressions    63--74
           Wolfram Büttner   Unification in datastructure multisets   75--88
                Mark E. Stickel   Schubert's Steamroller problem:
                                  Formulations and solutions . . . . . . . 89--101
                      Anonymous   Announcing a new journal . . . . . . . . 103--103
                      Anonymous   Addresses of Editor-in-Chief and
                                  Editorial Board  . . . . . . . . . . . . 105--107

Journal of Automated Reasoning
Volume 2, Number 2, June, 1986

                     Alan Bundy   Correctness criteria of some algorithms
                                  for uncertain reasoning using Incidence
                                  Calculus . . . . . . . . . . . . . . . . 109--126
                  Thomas Kramer   Automated analysis of operators on state
                                  tables: A technique for intelligent
                                  search . . . . . . . . . . . . . . . . . 127--153
                C. Aquilano and   
                 R. Barbuti and   
               P. Bocchetti and   
                    M. Martelli   Negation as Failure. Completeness of the
                                  Query Evaluation Process for Horn clause
                                  programs with recursive definitions  . . 155--170
              David A. Plaisted   A decision procedure for combinations of
                                  propositional temporal logic and other
                                  specialized theories . . . . . . . . . . 171--190
       Francis Jeffry Pelletier   Seventy-five problems for testing
                                  automatic theorem provers  . . . . . . . 191--216
                      Anonymous   Call for papers  . . . . . . . . . . . . 217--217
                      Anonymous   Announcing a new journal . . . . . . . . 218--218

Journal of Automated Reasoning
Volume 2, Number 3, September, 1986

              J. Strother Moore   Editor's preface to `Basic principles of
                                  mechanical theorem proving in elementary
                                  geometries' by Wu Wen-Tsun . . . . . . . 219--220
                    Wen-Tsun Wu   Basic principles of mechanical theorem
                                  proving in elementary geometries . . . . 221--252
           Shang-Ching Chou and   
            William F. Schelter   Proving geometry theorems with rewrite
                                  rules  . . . . . . . . . . . . . . . . . 253--273
              Joerg H. Siekmann   Editor's note  . . . . . . . . . . . . . 275--275
        Manfred Schmidt-Schauss   Unification under associativity and
                                  idempotence is of type nullary . . . . . 277--281
                   Franz Baader   The theory of idempotent semigroups is
                                  of unification type zero . . . . . . . . 283--286
               Robert Boyer and   
                 Ewing Lusk and   
             William McCune and   
              Ross Overbeek and   
               Mark Stickel and   
                   Lawrence Wos   Set theory in first-order logic: Clauses
                                  for Gödel's axioms  . . . . . . . . . . . 287--327

Journal of Automated Reasoning
Volume 2, Number 4, December, 1986

                      Anonymous   Editorial announcement A new column:
                                  Basic research problems  . . . . . . . . iii--iii
              Helder Coelho and   
             Luis Moniz Pereira   Automated reasoning in geometry theorem
                                  proving with Prolog  . . . . . . . . . . 329--390
               Jia-Huai You and   
             P. A. Subrahmanyam   A class of confluent term rewriting
                                  systems and unification  . . . . . . . . 391--418
           Barney Glickfeld and   
                  Ross Overbeek   A foray into combinatory logic . . . . . 419--431
                      Anonymous   Announcement . . . . . . . . . . . . . . 433--433


Journal of Automated Reasoning
Volume 3, Number 1, March, 1987

       Hans Jürgen Ohlbach   Link inheritance in abstract clause
                                  graphs . . . . . . . . . . . . . . . . . 1--34
             Tie-Cheng Wang and   
                  W. W. Bledsoe   Hierarchical deduction . . . . . . . . . 35--77
                      Larry Wos   Editor's note  . . . . . . . . . . . . . 79--80
                      Larry Wos   Some obstacles to the automation of
                                  reasoning, and the problem of redundant
                                  information  . . . . . . . . . . . . . . 81--90
             William McCune and   
                      Larry Wos   A case study in automated theorem
                                  proving: Finding sages in combinatory
                                  logic  . . . . . . . . . . . . . . . . . 91--107
                      Anonymous   Change of address  . . . . . . . . . . . 109--109
                      Anonymous   Announcements  . . . . . . . . . . . . . 109--111

Journal of Automated Reasoning
Volume 3, Number 2, June, 1987

                Anthony G. Cohn   A more expressive formulation of many
                                  sorted logic . . . . . . . . . . . . . . 113--200
                      Larry Wos   The problem of choosing the inference
                                  rule to employ . . . . . . . . . . . . . 201--209
                Rick L. Stevens   Some experiments in nonassociative ring
                                  theory with an automated theorem prover  211--221
                      Anonymous   Announcement . . . . . . . . . . . . . . 223--223

Journal of Automated Reasoning
Volume 3, Number 3, September, 1987

                   S. V. Reeves   Adding equality to semantic tableaux . . 225--246
           Alexander Herold and   
          Jörg H. Siekmann   Unification in Abelian semigroups  . . . 247--283
                Mark E. Stickel   A comparison of the variable-abstraction
                                  and constant-abstraction methods for
                                  associative-commutative unification  . . 285--289
               Shang-Ching Chou   A method for the mechanical derivation
                                  of formulas in elementary geometry . . . 291--299
               J.-L. Lassez and   
                    K. Marriott   Explicit representation of terms defined
                                  by counter examples  . . . . . . . . . . 301--317
                      Larry Wos   The problem of extending the set of
                                  support strategy . . . . . . . . . . . . 319--328
             Michael Miller and   
                  Donald Perlis   Proving self-utterances  . . . . . . . . 329--338
                      Anonymous   Announcements  . . . . . . . . . . . . . 339--342

Journal of Automated Reasoning
Volume 3, Number 4, December, 1987

                Zohar Manna and   
              Richard Waldinger   How to clear a block: A theory of plans  343--377
             Alexander Bockmayr   A note on a canonical theory with
                                  undecidable unification and matching
                                  problem  . . . . . . . . . . . . . . . . 379--381
                 Piotr Rudnicki   Obvious inferences . . . . . . . . . . . 383--393
            Richard Treitel and   
          Michael R. Genesereth   Choosing directions for rules  . . . . . 395--431
                      Larry Wos   The problem of definition expansion and
                                  contraction  . . . . . . . . . . . . . . 433--435
                 Tie-Cheng Wang   Case studies of $Z$-module reasoning:
                                  Proving benchmark theorems from ring
                                  theory . . . . . . . . . . . . . . . . . 437--451


Journal of Automated Reasoning
Volume 4, Number 1, March, 1988

                      Anonymous   Publisher's announcement . . . . . . . . v--v
                Jaakko Hintikka   Model minimization--- An alternative to
                                  circumscription  . . . . . . . . . . . . 1--13
                 Alan Bundy and   
                  Leon Sterling   Meta-level inference: Two applications   15--27
                Paul Helman and   
                  Robert Veroff   Designing deductive databases  . . . . . 29--68
                F. Oppacher and   
                        E. Suen   HARP: A tableau-based theorem prover . . 69--100
                      Larry Wos   The problem of finding a strategy to
                                  control binary paramodulation  . . . . . 101--107
                      Anonymous   Errata . . . . . . . . . . . . . . . . . 109--111
                      Anonymous   Book received  . . . . . . . . . . . . . 113--113
                      Anonymous   Announcements  . . . . . . . . . . . . . 115--116

Journal of Automated Reasoning
Volume 4, Number 2, June, 1988

            Robert S. Boyer and   
              J. Strother Moore   The addition of bounded quantification
                                  and partial functions to a computational
                                  logic and its theorem prover . . . . . . 117--172
                   Marek Zaionc   Mechanical procedure for proof
                                  construction via closed terms in typed $
                                  \lambda $ calculus . . . . . . . . . . . 173--190
                 Melvin Fitting   First-order modal tableaux . . . . . . . 191--213
                      Larry Wos   The problem of explaining the disparate
                                  performance of hyperresolution and
                                  paramodulation . . . . . . . . . . . . . 215--217
                     Art Quaife   Automated proofs of Löb's theorem and
                                  Gödel's two incompletensess theorems  . . 219--231
                  Ross Overbeek   Book review  . . . . . . . . . . . . . . 233--234
                      Anonymous   Errata . . . . . . . . . . . . . . . . . 235--236

Journal of Automated Reasoning
Volume 4, Number 3, September, 1988

                      Anonymous   Publisher's announcement . . . . . . . . iii--iii
               Shang-Ching Chou   An introduction to Wu's method for
                                  mechanical theorem proving in geometry   237--267
               Sidney C. Bailin   A $ \lambda $-unifiability test for set
                                  theory . . . . . . . . . . . . . . . . . 269--286
              David A. Plaisted   Non-Horn clause logic programming
                                  without contrapositives  . . . . . . . . 287--325
                      Larry Wos   The problem of self-analytically
                                  choosing the set of support  . . . . . . 327--329
               Deepak Kapur and   
                   Hantao Zhang   Proving equivalence of different
                                  axiomatizations of free groups . . . . . 331--352

Journal of Automated Reasoning
Volume 4, Number 4, December, 1988

                Mark E. Stickel   A prolog technology theorem prover:
                                  Implementation by an extended prolog
                                  compiler . . . . . . . . . . . . . . . . 353--380
              Ursula Martin and   
                  Tobias Nipkow   Unification in Boolean rings . . . . . . 381--396
            Kenneth A. Ross and   
                Rodney W. Topor   Inferring negative information from
                                  disjunctive databases  . . . . . . . . . 397--424
               Klaus Heje Munch   A new reduction rule for the connection
                                  graph proof procedure  . . . . . . . . . 425--444
                Leonard G. Monk   Inference rules using local contexts . . 445--462
                      Larry Wos   The problem of self-analytically
                                  choosing the weights . . . . . . . . . . 463--464
Hans-Jürgen Bürckert and   
           Alexander Herold and   
                   Deepak Kapur   Opening the AC-unification race  . . . . 465--474


Journal of Automated Reasoning
Volume 5, Number 1, March, 1989

                      Anonymous   Publisher's announcement . . . . . . . . v--v
             Vladimir Lifschitz   What is the inverse method?  . . . . . . 1--23
                Dallas Lankford   Non-negative integer basis algorithms
                                  for linear equations with integer
                                  coefficients . . . . . . . . . . . . . . 25--35
                  D. A. Wolfram   Intractable unifiability problems and
                                  backtracking . . . . . . . . . . . . . . 37--47
                  Tong Gao Tang   Temporal logic CTL + PROLOG  . . . . . . 49--65
           S. Purushothaman and   
             P. A. Subrahmanyam   Mechanical certification of systolic
                                  algorithms . . . . . . . . . . . . . . . 67--91
                      Larry Wos   The problem of finding an inference rule
                                  for set theory . . . . . . . . . . . . . 93--95
                     Art Quaife   Automated development of Tarski's
                                  geometry . . . . . . . . . . . . . . . . 97--118
                      Anonymous   Addresses of Editorial Board . . . . . . 119--121
                      Anonymous   Announcements  . . . . . . . . . . . . . 123--124

Journal of Automated Reasoning
Volume 5, Number 2, June, 1989

                   Robert Boyer   Note on verification . . . . . . . . . . 125--125
                      Avra Cohn   The notion of proof in hardware
                                  verification . . . . . . . . . . . . . . 127--139
             Tie-Cheng Wang and   
                   Rick Stevens   Solving open problems in right
                                  alternative rings with $Z$-module
                                  reasoning  . . . . . . . . . . . . . . . 141--165
         Teodor C. Przymusinski   On the declarative and procedural
                                  semantics of logic programs  . . . . . . 167--205
                K. S. Leung and   
                         W. Lam   A fuzzy expert system shell using both
                                  exact and inexact reasoning  . . . . . . 207--233
                      Larry Wos   The problem of determining the size of a
                                  complete set of reductions . . . . . . . 235--237
            Cynthia A. Wick and   
              William W. McCune   Automated reasoning about elementary
                                  point-set topology . . . . . . . . . . . 239--255

Journal of Automated Reasoning
Volume 5, Number 3, September, 1989

               Peter B. Andrews   On connections and higher-order logic    257--291
            Arcot Rajasekar and   
                 Jorge Lobo and   
                    Jack Minker   Weak Generalized Closed World Assumption 293--307
             Ulrich Furbach and   
    Steffen Hölldobler and   
              Joachim Schreiber   Horn equational theories and
                                  paramodulation . . . . . . . . . . . . . 309--337
              Bruce W. Char and   
        Alan R. Macnaughton and   
               Paul A. Strooper   Discovering inequality conditions in the
                                  analytic solution of optimization
                                  problems . . . . . . . . . . . . . . . . 339--362
            Lawrence C. Paulson   The foundation of a generic theorem
                                  prover . . . . . . . . . . . . . . . . . 363--397
                      Larry Wos   The problem of guaranteeing the
                                  existence of a complete set of
                                  reductions . . . . . . . . . . . . . . . 399--401
             Richard Schmid and   
      Hans-Albert Schneider and   
                 Thomas Filkorn   Using an extended PROLOG to solve the
                                  lion and unicorn puzzle  . . . . . . . . 403--408

Journal of Automated Reasoning
Volume 5, Number 4, December, 1989

              J. Strother Moore   System verification  . . . . . . . . . . 409--410
          William R. Bevier and   
        Warren A. Hunt, Jr. and   
          J. Strother Moore and   
               William D. Young   An approach to systems verification  . . 411--428
            Warren A. Hunt, Jr.   Microprocessor design verification . . . 429--460
              J. Strother Moore   A mechanically verified language
                                  implementation . . . . . . . . . . . . . 461--492
               William D. Young   A mechanically verified code generator   493--518
              William R. Bevier   Kit and the short stack  . . . . . . . . 519--530
                      Larry Wos   The problem of guaranteeing the absence
                                  of a complete set of reductions  . . . . 531--532
             G. H. Chisholm and   
                B. T. Smith and   
                   A. S. Wojcik   An automated reasoning problem
                                  associated with proving claims about
                                  programs using Floyd--Hoare inductive
                                  assertion methods  . . . . . . . . . . . 533--540


Journal of Automated Reasoning
Volume 6, Number 1, March, 1990

               Yves Auffray and   
           Jean-Jacques Hebrard   Strategies for modal resolution: Results
                                  and problems . . . . . . . . . . . . . . 1--38
                Pierre Lescanne   On the recursive decomposition ordering
                                  with lexicographical status and other
                                  related orderings  . . . . . . . . . . . 39--49
                J. W. Roach and   
            R. Sundararajan and   
                   L. T. Watson   Replacing unification by constraint
                                  satisfaction to improve logic program
                                  expressiveness . . . . . . . . . . . . . 51--75
                      Larry Wos   The problem of choosing between logic
                                  programming and general-purpose
                                  automated reasoning  . . . . . . . . . . 77--78
          Siva Anantharaman and   
                    Jieh Hsiang   Automated proofs of the Moufang
                                  identities in alternative rings  . . . . 79--109

Journal of Automated Reasoning
Volume 6, Number 2, June, 1990

                      Anonymous   Editorial announcement . . . . . . . . . iii--iii
               John Staples and   
              Peter J. Robinson   Structure sharing for quantified terms:
                                  Fundamentals . . . . . . . . . . . . . . 115--145
                James J. Lu and   
             V. S. Subrahmanian   Protected completions of first-order
                                  general logic programs . . . . . . . . . 147--172
                 D. Cantone and   
               E. G. Omodeo and   
                   A. Policriti   The automation of syllogistic  . . . . . 173--187
                 D. Cantone and   
                     V. Cutello   Decision procedures for elementary
                                  sublanguages of set theory . . . . . . . 189--201
     Giuseppa Carr\`a Ferro and   
                 Giovanni Gallo   A procedure to prove statements in
                                  differential geometry  . . . . . . . . . 203--209
                      Larry Wos   The problem of finding a mapping between
                                  clause representation and
                                  natural-deduction representation . . . . 211--212
                      Larry Wos   Meeting the challenge of fifty years of
                                  logic  . . . . . . . . . . . . . . . . . 213--232

Journal of Automated Reasoning
Volume 6, Number 3, September, 1990

                 Timothy Stokes   Gröbner bases in exterior algebra . . . . 233--250
                        Yuan Yu   Computer proofs in Group Theory  . . . . 251--286
                       W. Bibel   Short proofs of the pigeonhole formulas
                                  based on the connection method . . . . . 287--297
            Joseph S. Di Piazza   Interweaving knowledge extracting,
                                  organizing and evaluating: A concrete
                                  design for preventing logic and
                                  structure bugs while interviewing
                                  experts  . . . . . . . . . . . . . . . . 299--317
    Hans Kleine Büning and   
          Ulrich Löwen and   
               Stefan Schmitgen   Equivalence of propositional Prolog
                                  programs . . . . . . . . . . . . . . . . 319--335
                      Larry Wos   The problem of finding a semantic
                                  strategy for focusing inference rules    337--339
                  W. W. Bledsoe   Challenge problems in elementary
                                  calculus . . . . . . . . . . . . . . . . 341--359

Journal of Automated Reasoning
Volume 6, Number 4, December, 1990

                      Anonymous   Publisher's announcement . . . . . . . . iii--iii
       Peter F. Patel-Schneider   A decidable first-order logic for
                                  knowledge representation . . . . . . . . 361--388
              David A. Plaisted   A sequent-style model elimination
                                  strategy and a positive refinement . . . 389--402
                   Xiaoshan Gao   Transcendental functions and mechanical
                                  theorem proving in elementary geometries 403--417
                John L. Pollock   Interest driven suppositional reasoning  419--461
                      Larry Wos   The problem of choosing between
                                  predicate and function notation for
                                  problem representation . . . . . . . . . 463--464
                      S. Winker   Robbins algebra: Conditions that make a
                                  near-boolean algebra boolean . . . . . . 465--489
                      Anonymous   Call for papers  . . . . . . . . . . . . 491--492


Journal of Automated Reasoning
Volume 7, Number 1, March, 1991

                      Anonymous   Publisher's announcement . . . . . . . . v--v
             Donald W. Loveland   Near-Horn Prolog and beyond  . . . . . . 1--26
                 Peter Padawitz   Inductive expansion: A calculus for
                                  verifying and synthesizing functional
                                  and logic programs . . . . . . . . . . . 27--103
                      Larry Wos   The problem of finding a restriction
                                  strategy more effective than the set of
                                  support strategy . . . . . . . . . . . . 105--107
                  Matt Kaufmann   Generalization in the presence of free
                                  variables: A mechanically-checked
                                  correctness proof for one algorithm  . . 109--158
                   Rick Stevens   Book reviews . . . . . . . . . . . . . . 159--161
                      Anonymous   Errata . . . . . . . . . . . . . . . . . 163--163
                      Anonymous   Addresses of Editorial Board . . . . . . 165--167

Journal of Automated Reasoning
Volume 7, Number 2, June, 1991

                  Alfredo Ferro   Introduction . . . . . . . . . . . . . . 169--170
                    Wu Wen-Tsun   Mechanical theorem proving of
                                  differential geometries and some of its
                                  applications in mechanics  . . . . . . . 171--191
                     D. Cantone   Decision procedures for elementary
                                  sublanguages of set theory: X.
                                  Multilevel syllogistic extended by the
                                  singleton and powerset operators . . . . 193--230
                 D. Cantone and   
                 J. T. Schwartz   Decision procedures for elementary
                                  sublanguages of set theory: XI.
                                  Multilevel syllogistic extended by some
                                  elementary map constructs  . . . . . . . 231--256
                       A. Ferro   Decision procedures for elementary
                                  sublanguages of set theory: XII.
                                  Multilevel syllogistic extended with
                                  singleton and choice operators . . . . . 257--270
          Franco Parlamento and   
              Alberto Policriti   Decision procedures for elementary
                                  sublanguages of set theory: XIII. Model
                                  graphs, reflection and decidability  . . 271--284
               Peter B. Andrews   More on the problem of finding a mapping
                                  between clause representation and
                                  natural-deduction representation . . . . 285--286
                     Art Quaife   Unsolved problems in elementary number
                                  theory . . . . . . . . . . . . . . . . . 287--300

Journal of Automated Reasoning
Volume 7, Number 3, September, 1991

                      Anonymous   A well-kept secret of history  . . . . . 301--302
                 Alan Bundy and   
         Frank van Harmelen and   
               Jane Hesketh and   
                    Alan Smaill   Experiments with proof plans for
                                  induction  . . . . . . . . . . . . . . . 303--324
                    Rolf Socher   Optimizing the clausal normal form
                                  transformation . . . . . . . . . . . . . 325--336
           Danny De Schreye and   
               Bern Martens and   
             Gunther Sablon and   
             Maurice Bruynooghe   Compiling bottom-up and mixed
                                  derivations into top-down executable
                                  logic programs . . . . . . . . . . . . . 337--358
                   Allan Ramsay   Generating relevant models . . . . . . . 359--368
                    Werner Nutt   The unification hierarchy is undecidable 369--381
                  Tong Gao Tang   Programming in temporal-nonmonotonic
                                  reasoning  . . . . . . . . . . . . . . . 383--401
          Yishai A. Feldman and   
                   Charles Rich   Pattern-directed invocation with
                                  changing equations . . . . . . . . . . . 403--433
                      Larry Wos   The problem of choosing the type of
                                  subsumption to use . . . . . . . . . . . 435--438
                Matthew Wilding   Proving Matijasevich's lemma with a
                                  default arithmetic strategy  . . . . . . 439--446

Journal of Automated Reasoning
Volume 7, Number 4, December, 1991

            Michael A. McRobbie   Automated reasoning and nonclassical
                                  logics: Introduction . . . . . . . . . . 447--451
                 John K. Slaney   The Ackermann constant theorem: A
                                  computer-assisted investigation  . . . . 453--474
                 Paul Pritchard   Algorithms for finding matrix models of
                                  propositional calculi  . . . . . . . . . 475--487
                 Laurent Catach   TABLEAUX: A general theorem prover for
                                  modal logics . . . . . . . . . . . . . . 489--510
              Dov M. Gabbay and   
                Frank Kriwaczek   A family of goal directed theorem
                                  provers based on conjunction and
                                  implication: Part 1  . . . . . . . . . . 511--536
              Dick De Jongh and   
               Lex Hendriks and   
Gerard R. Renardel De Lavalette   Computations in fragments of
                                  intuitionistic propositional logic . . . 537--561
                   A. W. Bollen   Relevant logic programming . . . . . . . 563--585
              Grigori Mints and   
                   Tanel Tammet   Condensed detachment is complete for
                                  relevance logic: A computer-aided proof  587--596
            Robert K. Meyer and   
           Martin W. Bunder and   
                Lawrence Powers   Implementing the `Fool's model' of
                                  combinatory logic  . . . . . . . . . . . 597--630
                      Larry Wos   The problem of choosing the
                                  representation, inference rule, and
                                  strategy . . . . . . . . . . . . . . . . 631--634
       Paul B. Thistlewaite and   
            Michael A. McRobbie   Approaching hard non-classical problems  635--637


Journal of Automated Reasoning
Volume 8, Number 1, February, 1992

                      Anonymous   Publisher's announcement . . . . . . . . v--v
                      Anonymous   A section is born: Studies in Automated
                                  Reasoning  . . . . . . . . . . . . . . . 1--2
             David M. Russinoff   A mechanical proof of Quadratic
                                  Reciprocity  . . . . . . . . . . . . . . 3--21
               Anita Jindal and   
              Ross Overbeek and   
                 Waldo C. Kabat   Exploitation of parallel processing for
                                  implementing high-performance deduction
                                  systems  . . . . . . . . . . . . . . . . 23--38
                 Eric Domenjoud   A technical note on AC-unification. The
                                  number of minimal unifiers of the
                                  equation $ \alpha x_1 + \cdots + \alpha
                                  x_p \doteq_{AC} \beta y_1 + \cdots +
                                  \beta y_q $  . . . . . . . . . . . . . . 39--44
                 Larry M. Hines   Completeness of a prover for dense
                                  linear orders  . . . . . . . . . . . . . 45--75
             Shyi-Ming Chen and   
               Jyh-Sheng Ke and   
                   Jin-Fu Chang   An inexact reasoning algorithm based on
                                  fuzzy rule matrix transformations  . . . 77--90
                     Art Quaife   Automated deduction in von
                                  Neumann--Bernays--Gödel set theory  . . . 91--147

Journal of Automated Reasoning
Volume 8, Number 2, April, 1992

              Soumitra Bose and   
           Edmund M. Clarke and   
              David E. Long and   
                Spiro Michaylov   Parthenon: A parallel theorem prover for
                                  non-Horn clauses . . . . . . . . . . . . 153--181
                    R. Letz and   
                J. Schumann and   
                  S. Bayerl and   
                       W. Bibel   SETHEO: A high-performance theorem
                                  prover . . . . . . . . . . . . . . . . . 183--212
              Robert Veroff and   
                      Larry Wos   The linked inference principle, I: The
                                  formal treatment . . . . . . . . . . . . 213--274
             James D. Baker and   
          Shahriar Zand-Biglari   An integral theorem prover and the role
                                  of proof planning  . . . . . . . . . . . 275--295
              J. C. Shepherdson   SLDNF-resolution with equality . . . . . 297--306
                      Larry Wos   The problem of choosing between using
                                  and avoiding equality predicates . . . . 307--309

Journal of Automated Reasoning
Volume 8, Number 3, June, 1992

            Dave Barker-Plummer   Gazing: An approach to the problem of
                                  definition and lemma use . . . . . . . . 311--344
            Chitta R. Baral and   
             V. S. Subrahmanian   Stable and extension class theory for
                                  logic programs and default logics  . . . 345--366
                 Robert J. Hall   Comparing parameter schemes for
                                  propositional reasoning: An empirical
                                  study  . . . . . . . . . . . . . . . . . 367--394
              Mark F. Russo and   
              Richard L. Peskin   Automatically identifying the asymptotic
                                  behavior of nonlinear singularly
                                  perturbed boundary value problems  . . . 395--419
                      Larry Wos   The problem of reasoning from
                                  inequalities . . . . . . . . . . . . . . 421--426


Journal of Automated Reasoning
Volume 9, Number 1, August, 1992

              William W. Mccune   Automated discovery of new
                                  axiomatizations of the left group and
                                  right group calculi  . . . . . . . . . . 1--24
               Shie-Jue Lee and   
              David A. Plaisted   Eliminating duplication with the
                                  hyper-linking strategy . . . . . . . . . 25--42
                    Dan Benanav   Recognizing unnecessary clauses in
                                  resolution based systems . . . . . . . . 43--76
          Rolf Socher-Ambrosius   How to avoid the derivation of redundant
                                  clauses in reasoning systems . . . . . . 77--97
                Nicola Olivetti   Tableaux and sequent calculus for
                                  minimal entailment . . . . . . . . . . . 99--139
                      Larry Wos   The problem of demodulation during
                                  inference rule application . . . . . . . 141--143

Journal of Automated Reasoning
Volume 9, Number 2, October, 1992

                      Larry Wos   Note on McCune's article on
                                  discrimination trees . . . . . . . . . . 145--146
                 William McCune   Experiments with discrimination-tree
                                  indexing and path indexing for term
                                  retrieval  . . . . . . . . . . . . . . . 147--167
                   Mark Franzen   Hilbert's tenth problem is of
                                  unification type zero  . . . . . . . . . 169--178
              Michael Kifer and   
           Eliezer L. Lozinskii   A logic for reasoning with inconsistency 179--215
            Donald E. Brown and   
               Wendy J. Markert   Uncertainty management with imprecise
                                  knowledge with application to design . . 217--230
              Nevin Heintze and   
            Spiro Michaylov and   
                  Peter Stuckey   CLP(\mathfrakR) and some electrical
                                  engineering problems . . . . . . . . . . 231--260
               Deepak Kapur and   
              Paliath Narendran   Complexity of unification problems with
                                  associative-commutative operators  . . . 261--288
                      Larry Wos   The problem of demodulator adjunction    289--290

Journal of Automated Reasoning
Volume 9, Number 3, December, 1992

                      Larry Wos   Transition to the future . . . . . . . . iii--iii
                  Kenneth Kunen   Single axioms for groups . . . . . . . . 291--308
                Arnon Avron and   
              Furio Honsell and   
               Ian A. Mason and   
                 Robert Pollack   Using typed lambda calculus to implement
                                  formal systems on a machine  . . . . . . 309--354
                  Matt Kaufmann   An extension of the Boyer--Moore Theorem
                                  Prover to support first-order
                                  quantification . . . . . . . . . . . . . 355--372
          Jean-Louis Lassez and   
               Michael J. Maher   On Fourier's algorithm for linear
                                  arithmetic constraints . . . . . . . . . 373--379
                G. M. Kuper and   
              K. W. McAloon and   
                K. V. Palem and   
                    K. J. Perry   A note on the parallel complexity of
                                  anti-unification . . . . . . . . . . . . 381--389
          Arthur L. Delcher and   
                    Simon Kasif   Efficient parallel term matching and
                                  anti-unification . . . . . . . . . . . . 391--406
                      Larry Wos   The problem of demodulating across
                                  argument and literal boundaries  . . . . 407--408
                  Simon Parsons   Book review  . . . . . . . . . . . . . . 409--411


Journal of Automated Reasoning
Volume 10, Number 1, February, 1993

              William W. McCune   Single axioms for groups and Abelian
                                  groups with various operations . . . . . 1--13
                  P. A. J. Noel   Experimenting with Isabelle in ZF set
                                  theory . . . . . . . . . . . . . . . . . 15--58
          Thomas J. Weigert and   
              Jing-Pha Tsai and   
                      Xuhua Liu   Fuzzy operator logic and fuzzy
                                  resolution . . . . . . . . . . . . . . . 59--78
                     F. Corella   What holds in a context? . . . . . . . . 79--93
                  Jim Christian   Flatterms, discrimination nets, and fast
                                  term rewriting . . . . . . . . . . . . . 95--113
                    Frank Vlach   Simplification in a satisfiability
                                  checker for VLSI applications  . . . . . 115--136
                      Larry Wos   The problem of automated theorem finding 137--138

Journal of Automated Reasoning
Volume 10, Number 2, June, 1993

                Li Yan Yuan and   
                   Jia-Huai You   Autoepistemic circumscription and logic
                                  programming  . . . . . . . . . . . . . . 143--160
           Shang-Ching Chou and   
                  Xiao-Shan Gao   Automated reasoning in differential
                                  geometry and mechanics using the
                                  characteristic set method  . . . . . . . 161--172
           Shang-Ching Chou and   
                  Xiao-Shan Gao   Automated reasoning in differential
                                  geometry and mechanics using the
                                  characteristic set method  . . . . . . . 173--189
                 Raymond Ng and   
             V. S. Subrahmanian   A semantical framework for supporting
                                  subjective and conditional probabilities
                                  in deductive databases . . . . . . . . . 191--235
              Marek A. Suchenek   First-order syntactic characterizations
                                  of minimal entailment, domain-minimal
                                  entailment, and Herbrand entailment  . . 237--263
                    Arnon Avron   Gentzen-type systems, resolution and
                                  tableaux . . . . . . . . . . . . . . . . 265--281
                      Larry Wos   The problem of selecting an approach
                                  based on prior success . . . . . . . . . 283--284
              Charles Ashbacher   Book review  . . . . . . . . . . . . . . 285--286

Journal of Automated Reasoning
Volume 10, Number 3, October, 1993

                      Larry Wos   The kernel strategy and its use for the
                                  study of combinatory logic . . . . . . . 287--343
                James J. Lu and   
          Monica D. Barback and   
           Lawrence J. Henschen   Interpreting disjunctive logic programs
                                  based on a strong sense of disjunction   345--370
                James J. Lu and   
             V. S. Subrahmanian   Completeness issues in RUE--NRF
                                  deduction: The undecidability of
                                  viability  . . . . . . . . . . . . . . . 371--388
              Joachim Steinbach   Simplification orderings: Putting them
                                  to the test  . . . . . . . . . . . . . . 389--397
            Chitta R. Baral and   
             V. S. Subrahmanian   Dualities between alternative semantics
                                  for logic programming and nonmonotonic
                                  reasoning  . . . . . . . . . . . . . . . 399--420
                      Larry Wos   The problem of reasoning by analogy  . . 421--422
                      Anonymous   Announcement . . . . . . . . . . . . . . 423--423


Journal of Automated Reasoning
Volume 11, Number 1, February, 1993

                  Adrian Walker   Backchain iteration: Towards a practical
                                  inference method that is simple enough
                                  to be proved terminating, sound, and
                                  complete . . . . . . . . . . . . . . . . 1--22
         Fausto Giunchiglia and   
                     Toby Walsh   The inevitability of inconsistent
                                  abstract spaces  . . . . . . . . . . . . 23--41
                      Amy Felty   Implementing tactics and tacticals in a
                                  higher-order logic programming language  43--81
              Alberto Segre and   
              Daniel Scharstein   Bounded-overhead caching for
                                  definite-clause theorem proving  . . . . 83--113
               Gopalan Nadathur   A proof procedure for the logic of
                                  hereditary Harrop formulas . . . . . . . 115--145
                      Larry Wos   The problem of naming and function
                                  replacement  . . . . . . . . . . . . . . 147--148

Journal of Automated Reasoning
Volume 11, Number 2, June, 1993

                Klaus U. Schulz   Word unification and transformation of
                                  generalized equations  . . . . . . . . . 149--184
               Alexandre Boudet   Competing for the AC--Unification Race   185--212
          William M. Farmer and   
          Joshua D. Guttman and   
               F. Javier Thayer   IMPS: An interactive mathematical proof
                                  system . . . . . . . . . . . . . . . . . 213--248
                 John Grant and   
                 John Horty and   
                 Jorge Lobo and   
                    Jack Minker   View updates in stratified disjunctive
                                  databases  . . . . . . . . . . . . . . . 249--267
                  Jinchang Wang   Inference flexibility in Horn clause
                                  knowledge bases and the simplex method   269--288
                      Larry Wos   The problem of reasoning by case
                                  analysis . . . . . . . . . . . . . . . . 289--291

Journal of Automated Reasoning
Volume 11, Number 3, October, 1993

              W. W. Bledsoe and   
                    Guohui Feng   SET-VAR  . . . . . . . . . . . . . . . . 293--314
                  Ross Overbeek   The CADE-11 competitions: A personal
                                  view . . . . . . . . . . . . . . . . . . 315--316
              Ewing L. Lusk and   
              William W. McCune   Uniform strategies: The CADE-11 theorem
                                  proving contest  . . . . . . . . . . . . 317--331
                   Hantao Zhang   Automated proofs of equality problems in
                                  Overbeek's competition . . . . . . . . . 333--351
            Lawrence C. Paulson   Set theory for verification: I. From
                                  foundations to functions . . . . . . . . 353--389
           Sidney C. Bailin and   
            Dave Barker-Plummer   $-$-match: An inference rule for
                                  incrementally elaborating set
                                  instantiations . . . . . . . . . . . . . 391--428
                  Simon Parsons   Book review  . . . . . . . . . . . . . . 429--431
                      Larry Wos   The problem of induction . . . . . . . . 433--434


Journal of Automated Reasoning
Volume 12, Number 1, February, 1994

           Eliezer L. Lozinskii   Resolving contradictions: A plausible
                                  semantics for inconsistent systems . . . 1--31
              J. Strother Moore   Introduction to the OBDD algorithm for
                                  the ATP community  . . . . . . . . . . . 33--45
           Taäieb Mellouli   TMPR: A tree-structured modified problem
                                  reduction proof procedure and its
                                  extension to three-valued logic  . . . . 47--87
            Belaid Benhamou and   
                   Lakhdar Sais   Tractability through symmetries in
                                  propositional calculus . . . . . . . . . 89--102
           J. Stuart Aitken and   
              Han Reichgelt and   
                 Nigel Shadbolt   Resolution theorem proving in reified
                                  modal logics . . . . . . . . . . . . . . 103--129
                  Simon Parsons   Book review  . . . . . . . . . . . . . . 131--132
                      Larry Wos   The problem of strategy and
                                  hyperresolution  . . . . . . . . . . . . 133--134

Journal of Automated Reasoning
Volume 12, Number 2, June, 1994

            Ralph M. Butler and   
               Ross A. Overbeek   Formula databases for high-performance
                                  resolution/paramodulation systems  . . . 139--156
         Timothy S. C. Chou and   
              Marianne Winslett   A model-based belief revision system . . 157--208
                    E. K. Burke   Unification in partially commutative
                                  semigroups . . . . . . . . . . . . . . . 209--223
       Maria Paola Bonacina and   
                    Jieh Hsiang   On subsumption in distributed
                                  derivations  . . . . . . . . . . . . . . 225--240
           Vincent J. Digricoli   The rue theorem-proving system: The
                                  complete set of LIM+ challenge problems  241--264
                      Larry Wos   The problem of hyperparamodulation . . . 265--271

Journal of Automated Reasoning
Volume 12, Number 3, October, 1994

                   Tanel Tammet   Proof strategies in linear logic . . . . 273--304
             Louiqa Raschid and   
                     Jorge Lobo   A semantics for a class of
                                  non-deterministic and causal production
                                  system programs  . . . . . . . . . . . . 305--349
          Giuseppa Carra' Ferro   An extension of a procedure to prove
                                  statements in differential geometry  . . 351--358
               Shie-Jue Lee and   
                   Chih-Hung Wu   Improving the efficiency of a
                                  hyperlinking-based theorem prover by
                                  incremental evaluation with network
                                  structures . . . . . . . . . . . . . . . 359--388
                Zhenyu Qian and   
                  Tobias Nipkow   Reduction and unification in lambda
                                  calculi with a general notion of subtype 389--406
                      Larry Wos   The problem of hyperparamodulation and
                                  nuclei . . . . . . . . . . . . . . . . . 407--409
                      Anonymous   Errata . . . . . . . . . . . . . . . . . 411--412


Journal of Automated Reasoning
Volume 13, Number 1, February, 1994

       Maria Paola Bonacina and   
                    Jieh Hsiang   Parallelization of deduction strategies:
                                  An analytical study  . . . . . . . . . . 1--33
               Piero A. Bonatti   Autoepistemic logic programming  . . . . 35--67
                    Li-Yan Yuan   Autoepistemic logic of first order and
                                  its expressive power . . . . . . . . . . 69--82
                  C. A. Johnson   On the termination of clause graph
                                  resolution . . . . . . . . . . . . . . . 83--115
                Adnan Yahya and   
José Alberto Fernández and   
                    Jack Minker   Ordered model trees: A normal form for
                                  disjunctive deductive databases  . . . . 117--143
              Chiaki Sakama and   
                  Katsumi Inoue   An alternative approach to the semantics
                                  of disjunctive logic programs and
                                  deductive databases  . . . . . . . . . . 145--172

Journal of Automated Reasoning
Volume 13, Number 2, June, 1994

               Graham Wrightson   Preface to the special issue on tableaux 173--173
                 Melvin Fitting   Tableaux for logic programming . . . . . 175--188
                Mark E. Stickel   Upside-down meta-interpretation of the
                                  model elimination theorem-proving
                                  procedure for deduction and abduction    189--210
         Reiner Hähnle and   
               Peter H. Schmitt   The liberalized $ \delta $-rule in free
                                  variable semantic tableaux . . . . . . . 211--221
              Vincent Risch and   
             Camilla B. Schwind   Tableau-based characterization and
                                  theorem proving for default logic  . . . 223--242
        Marcello D'Agostino and   
                  Dov M. Gabbay   A generalization of analytic deduction
                                  via labelled deductive systems. Part I:
                                  Basic substructural logics . . . . . . . 243--281

Journal of Automated Reasoning
Volume 13, Number 3, October, 1994

                 Owen Astrachan   METEOR: Exploring model elimination
                                  theorem proving  . . . . . . . . . . . . 283--296
                    R. Letz and   
                    K. Mayr and   
                      C. Goller   Controlled integration of the cut rule
                                  into connection tableau calculi  . . . . 297--337
          Peter Baumgartner and   
                 Ulrich Furbach   Model elimination without
                                  contrapositives and its application to
                                  PTTP . . . . . . . . . . . . . . . . . . 339--359
        Pierangelo Miglioli and   
                Ugo Moscato and   
                  Mario Ornaghi   An improved refutation system for
                                  intuitionistic predicate logic . . . . . 361--373
                    Sven Lorenz   A tableau prover for domain minimization 375--390
   Regimantas Pliu\vskevi\vcius   The saturated tableaux for linear
                                  miniscoped Horn-like temporal logic  . . 391--407
                    J. Schumann   Tableau-based theorem provers: Systems
                                  and implementations  . . . . . . . . . . 409--421


Journal of Automated Reasoning
Volume 14, Number 1, February, 1995

             Vladimir Lifschitz   Preface to the special issue on
                                  commonsense and nonmonotonic reasoning   1--1
             Ilkka Niemelä   A decision method for nonmonotonic
                                  reasoning based on autoepistemic
                                  reasoning  . . . . . . . . . . . . . . . 3--42
            Matthew L. Ginsberg   Modality and interrupts  . . . . . . . . 43--91
José Júlio Alferes and   
Carlos Viegas Damásio and   
      Luís Moniz Pereira   A logic programming system for
                                  nonmonotonic reasoning . . . . . . . . . 93--147
               Franz Baader and   
             Bernhard Hollunder   Embedding defaults into terminological
                                  knowledge representation formalisms  . . 149--180

Journal of Automated Reasoning
Volume 14, Number 2, June, 1995

              Adel Bouhoula and   
       Michaël Rusinowitch   Implicit induction in conditional
                                  theories . . . . . . . . . . . . . . . . 189--235
                   Allan Ramsay   Theorem proving for intensional logic    237--255
           Shang-Ching Chou and   
              Xiao-Shan Gao and   
               Jing-Zhong Zhang   Automated production of traditional
                                  proofs in solid geometry . . . . . . . . 257--291
               Deepak Kapur and   
               G. Sivakumar and   
                   Hantao Zhang   A path ordering for proving termination
                                  of AC rewrite systems  . . . . . . . . . 293--316
             Kumar V. Vadaparty   On the complexity of nested-object
                                  matching . . . . . . . . . . . . . . . . 317--323
         Donald W. Loveland and   
              David W. Reed and   
                Debra S. Wilson   SATCHMORE: SATCHMO with RElevancy  . . . 325--351

Journal of Automated Reasoning
Volume 14, Number 3, October, 1995

                 Karl Schlechta   Logic, topology, and integration . . . . 353--381
                  Joan Hart and   
                  Kenneth Kunen   Single axioms for odd exponent groups    383--412
                    Thomas Jech   OTTER experiments in a system of
                                  combinatory logic  . . . . . . . . . . . 413--426
             I. Chakrabarti and   
                  D. Sarkar and   
                 A. K. Majumdar   Identification of inductive properties
                                  during verification of synchronous
                                  sequential circuits  . . . . . . . . . . 427--462


Journal of Automated Reasoning
Volume 15, Number 1, February, 1995

             Vladimir Lifschitz   Preface to the special issue on
                                  commonsense and nonmonotonic reasoning   v--v
         Michael Thielscher and   
                 Torsten Schaub   Default reasoning by deductive planning  1--40
               Franz Baader and   
             Bernhard Hollunder   Priorities on defaults with
                                  prerequisites, and their application in
                                  treating specificity in terminological
                                  default logic  . . . . . . . . . . . . . 41--68
             Sakthi Subramanian   Mechanical verification of strategies    69--93
                      T. Schaub   A new methodology for query answering in
                                  default logics via structure-oriented
                                  theorem proving  . . . . . . . . . . . . 95--165

Journal of Automated Reasoning
Volume 15, Number 2, June, 1995

            Lawrence C. Paulson   Set theory for verification. II:
                                  Induction and recursion  . . . . . . . . 167--215
                  Kenneth Kunen   A Ramsey theorem in Boyer--Moore logic   217--235
                Andrei Voronkov   The anatomy of vampire . . . . . . . . . 237--265
   Hans Jürgen Ohlbach and   
           Christoph Weidenbach   A note on assumptions about Skolem
                                  functions  . . . . . . . . . . . . . . . 267--275
                      Anonymous   The Kluwer \LaTeX style file . . . . . . 277--278

Journal of Automated Reasoning
Volume 15, Number 3, October, 1995

                      Larry Wos   Searching for circles of pure proofs . . 279--315
              G. D'Agostino and   
               A. Montanari and   
                   A. Policriti   A set-theoretic translation method for
                                  polymodal logics . . . . . . . . . . . . 317--337
           Bernhard Beckert and   
                Joachim Posegga   lean TAP: Lean tableau-based deduction   339--358
               J. N. Hooker and   
                       V. Vinay   Branching rules for satisfiability . . . 359--383


Journal of Automated Reasoning
Volume 16, Number 1--2, March, 1996

                   Hantao Zhang   Preface to the special issue on
                                  Automated Mathematical induction . . . . 1--1
   François Bronsard and   
              Uday S. Reddy and   
               Robert W. Hasker   Induction using term orders  . . . . . . 3--37
               Deepak Kapur and   
                 M. Subramaniam   New uses of linear arithmetic in
                                  automated theorem proving by induction   39--78
             Andrew Ireland and   
                     Alan Bundy   Productive use of failure in inductive
                                  proof  . . . . . . . . . . . . . . . . . 79--111
                  Ina Kraan and   
                David Basin and   
                     Alan Bundy   Middle-out reasoning for synthesis and
                                  induction  . . . . . . . . . . . . . . . 113--145
             David A. Basin and   
                     Toby Walsh   A calculus for and termination of
                                  rippling . . . . . . . . . . . . . . . . 147--180
              Matt Kaufmann and   
                Paolo Pecchiari   Interaction with the Boyer--Moore
                                  theorem prover: A tutorial study using
                                  the arithmetic--geometric mean theorem   181--222

Journal of Automated Reasoning
Volume 16, Number 3, June, 1996

                  Robert Veroff   Using hints to increase the
                                  effectiveness of an automated reasoning
                                  program: Case studies  . . . . . . . . . 223--239
              Peter Baumgartner   Linear and unit-resulting refutations
                                  for Horn theories  . . . . . . . . . . . 241--319
           Peter B. Andrews and   
             Matthew Bishop and   
                Sunil Issar and   
                Dan Nesmith and   
             Frank Pfenning and   
                     Hongwei Xi   TPS: A theorem-proving system for
                                  classical type theory  . . . . . . . . . 321--353
               Lusheng Wang and   
              S. K. M. Wong and   
                      Y. Y. Yao   On the completeness of incidence
                                  calculus . . . . . . . . . . . . . . . . 355--368
                Michael Hedberg   A type-theoretic interpretation of
                                  constructive domain theory . . . . . . . 369--425
              Charles Ashbacher   From logic to logic programming  . . . . 427--427


Journal of Automated Reasoning
Volume 17, Number 1, August, 1996

                     Jian Zhang   Constructing finite algebras with FALCON 1--22
                      Larry Wos   The power of combining resonance with
                                  heat . . . . . . . . . . . . . . . . . . 23--81
                  Kenneth Kunen   The semantics of answer literals . . . . 83--95
          Philippe Codognet and   
                    Daniel Diaz   A simple and efficient boolean solver
                                  for Constraint Logic Programming . . . . 97--128
          Paliath Narendran and   
       Michaël Rusinowitch   Any ground associative-commutative
                                  theory has a finite canonical system . . 131--143

Journal of Automated Reasoning
Volume 17, Number 2, October, 1996

                  S. Linton and   
                       D. Shand   Some group theoretic examples with
                                  completion theorem provers . . . . . . . 145--169
José Alberto Fernández and   
                 John Grant and   
                    Jack Minker   Model theoretic approach to view updates
                                  in deductive databases . . . . . . . . . 171--197
             Michael Thielscher   On the completeness of SLDENF-resolution 199--214
                      Larry Wos   OTTER and the Moufang identity problem   215--257

Journal of Automated Reasoning
Volume 17, Number 3, December, 1996

              Yannis Dimopoulos   On computing logic programs  . . . . . . 259--289
        Lawrence C. Paulson and   
          Krzysztof Grabczewski   Mechanizing set theory . . . . . . . . . 291--323
           Shang-Ching Chou and   
              Xiao-Shan Gao and   
               Jing-Zhong Zhang   Automated generation of readable proofs
                                  with geometric invariants  . . . . . . . 325--347
           Shang-Ching Chou and   
              Xiao-Shan Gao and   
               Jing-Zhong Zhang   Automated generation of readable proofs
                                  with geometric invariants  . . . . . . . 349--370
         Gregory Sidebottom and   
              William S. Havens   Nicolog: A simple yet powerful cc(FD)
                                  language . . . . . . . . . . . . . . . . 371--403


Journal of Automated Reasoning
Volume 18, Number 1, February, 1997

                    Larry Hines   A Tribute to Woody Bledsoe . . . . . . . 1--4
              Rong-Huei Hou and   
             Tzung-Pei Hong and   
         Shian-Shyong Tseng and   
                     Sy-Yen Kuo   A New Probabilistic Induction Method . . 5--24
          Grigoris Antoniou and   
                Elmar Langetepe   A Correct Logic Programming Computation
                                  of Default Logic Extensions  . . . . . . 25--46
              Anavai Ramesh and   
           Bernhard Beckert and   
         Reiner Hähnle and   
                 Neil V. Murray   Fast Subsumption Checks Using Anti-Links 47--83
                 Simon Finn and   
         Michael P. Fourman and   
                   John Longley   Partial Functions in a Total Setting . . 85--104
                        Li Dafa   Unification Algorithms for Eliminating
                                  and Introducing Quantifiers in Natural
                                  Deduction Automated Theorem Proving  . . 105--134
   Francis Jeffry Pelletier and   
                Geoff Sutcliffe   An Erratum for Some Errata to ATP
                                  Problems . . . . . . . . . . . . . . . . 135--135

Journal of Automated Reasoning
Volume 18, Number 2, April, 1997

            Geoff Sutcliffe and   
              Christian Suttner   The CADE-13 ATP System Competition . . . 137--138
          Christian Suttner and   
                Geoff Sutcliffe   The Design of the CADE-13 ATP System
                                  Competition  . . . . . . . . . . . . . . 139--162
            Geoff Sutcliffe and   
              Christian Suttner   The Procedures of the CADE-13 ATP System
                                  Competition  . . . . . . . . . . . . . . 163--169
         Robert Nieuwenhuis and   
  José Miguel Rivero and   
    Miguel Ángel Vallejo   Barcelona  . . . . . . . . . . . . . . . 171--176
          Geoffrey D. Alexander   CLIN-E --- Smallest Instance First
                                  Hyper-Linking  . . . . . . . . . . . . . 177--182
                   Heng Chu and   
              David A. Plaisted   CLIN-S --- A Semantically Guided
                                  First-Order Theorem Prover . . . . . . . 183--188
        Jörg Denzinger and   
          Martin Kronenburg and   
                 Stephan Schulz   DISCOUNT --- A Distributed and Learning
                                  Equational Prover  . . . . . . . . . . . 189--198
                   Tanel Tammet   Gandalf  . . . . . . . . . . . . . . . . 199--204
                  Reinhold Letz   LINUS --- A Link Instantion Prover with
                                  Unit Support . . . . . . . . . . . . . . 205--210
             William McCune and   
                      Larry Wos   Otter- The CADE-13 Competition
                                  Incarnations . . . . . . . . . . . . . . 211--220
             M. Paramasivam and   
              David A. Plaisted   RRTP --- A Replacement Rule Theorem
                                  Prover . . . . . . . . . . . . . . . . . 221--226
                Tim Geisler and   
                 Sven Panne and   
           Heribert Schütz   Satchmo- The Compiling and Functional
                                  Variants . . . . . . . . . . . . . . . . 227--236
                  Max Moser and   
               Ortrun Ibens and   
              Reinhold Letz and   
          Joachim Steinbach and   
           Christoph Goller and   
            Johann Schumann and   
                     Klaus Mayr   SETHEO and E-SETHEO --- The CADE-13
                                  Systems  . . . . . . . . . . . . . . . . 237--246
           Christoph Weidenbach   SPASS --- Version 0.49 . . . . . . . . . 247--252
           Christian B. Suttner   SPTHEO --- A Parallel Theorem Prover . . 253--258
                Steve Greenbaum   Violet . . . . . . . . . . . . . . . . . 259--264
         Thomas Hillenbrand and   
                 Arnim Buch and   
                    Roland Vogt   WALDMEISTER --- High-Performance
                                  Equational Deduction . . . . . . . . . . 265--270
            Geoff Sutcliffe and   
              Christian Suttner   The Results- of the CADE-13 ATP System
                                  Competition  . . . . . . . . . . . . . . 271--286
   Francis Jeffry Pelletier and   
            Geoff Sutcliffe and   
              Christian Suttner   Conclusions about the CADE-13 ATP System
                                  Competition  . . . . . . . . . . . . . . 287--296

Journal of Automated Reasoning
Volume 18, Number 3, June, 1997

            Patrick Doherty and   
        Witold \Lukaszewicz and   
                Andrzej Sza\las   Computing Circumscription Revisited: A
                                  Reduction Algorithm  . . . . . . . . . . 297--336
              Anavai Ramesh and   
              George Becker and   
                 Neil V. Murray   CNF and DNF Considered Harmful for
                                  Computing Prime Implicants\slash
                                  Implicates . . . . . . . . . . . . . . . 337--356
              Marek A. Suchenek   Evaluation of Queries under Closed-World
                                  Assumption . . . . . . . . . . . . . . . 357--398
                  Dieter Hutter   Coloring Terms to Control Equational
                                  Reasoning  . . . . . . . . . . . . . . . 399--442


Journal of Automated Reasoning
Volume 19, Number 1, August, 1997

              Jürgen Giesl   Termination of Nested and Mutually
                                  Recursive Algorithms . . . . . . . . . . 1--29
                  C. A. Johnson   Deduction Trees and the View Update
                                  Problem in Indefinite Deductive
                                  Databases  . . . . . . . . . . . . . . . 31--85
          Paliath Narendran and   
                 Friedrich Otto   Single Versus Simultaneous Equational
                                  Unification and Equational Unification
                                  for Variable-Permuting Theories  . . . . 87--115
            O. L. Astrachan and   
                 D. W. Loveland   The Use of Lemmas in the Model
                                  Elimination Procedure  . . . . . . . . . 117--141

Journal of Automated Reasoning
Volume 19, Number 2, October, 1997

        Marc-Michel Corsini and   
                  Antoine Rauzy   Toupie: The $ \mu $-calculus over Finite
                                  Domains as a Constraint Language . . . . 143--171
                K. Hörwein   Structuring Resolution Proofs by
                                  Introducing New Lemmata  . . . . . . . . 173--203
          Peter Baumgartner and   
            Stefan Brüning   A Disjunctive Positive Refinement of
                                  Model Elimination and its Application to
                                  Subsumption Deletion . . . . . . . . . . 205--262

Journal of Automated Reasoning
Volume 19, Number 3, December, 1997

                 William Mccune   Solution of the Robbins Problem  . . . . 263--276
            Ricardo Caferra and   
                Nicolas Peltier   A New Technique for Verifying and
                                  Correcting Logic Programs  . . . . . . . 277--318
                 Alan Bundy and   
         Fausto Giunchiglia and   
        Adolfo Villafiorita and   
                     Toby Walsh   Abstract Proof Checking: An Example
                                  Motivated by an Incompleteness Theorem   319--346
             David Sturgill and   
            Alberto Maria Segre   Nagging: A Distributed, Adversarial
                                  Search-Pruning Technique Applied to
                                  First-Order Inference  . . . . . . . . . 347--376


Journal of Automated Reasoning
Volume 20, Number 1--2, April, 1998

José Júlio Alferes and   
      Luís Moniz Pereira   Preface  . . . . . . . . . . . . . . . . 1--3
                Hans de Nivelle   An Algorithm for the Retrieval of
                                  Unifiers from Discrimination Trees . . . 5--25
  Gilles Défourneaux and   
         Christophe Bourely and   
                Nicolas Peltier   Semantic Generalizations for Proving and
                                  Disproving Conjectures by Analogy  . . . 27--45
          Anatoli Degtyarev and   
                Andrei Voronkov   What You Always Wanted to Know about
                                  Rigid E-Unification  . . . . . . . . . . 47--80
        Peter Fröhlich and   
             Wolfgang Nejdl and   
              Michael Schroeder   Strategies in Model-based Diagnosis  . . 81--105
José Júlio Alferes and   
  Luís Moniz Pereira and   
         Teodor C. Przymusinski   'Classical' Negation in Nonmonotonic
                                  Reasoning and Logic Programming  . . . . 107--142
               Stefan Brass and   
                Jürgen Dix   Characterizations of the Disjunctive
                                  Well-Founded Semantics: Confluent
                                  Calculi and Iterated GCWA  . . . . . . . 143--165
             Paola Forcheri and   
            Paolo Gentilini and   
           Maria Teresa Molfino   Informational Logic as a Tool for
                                  Automated Reasoning  . . . . . . . . . . 167--190
                Ph. Besnard and   
                      T. Schaub   Signed Systems for Paraconsistent
                                  Reasoning  . . . . . . . . . . . . . . . 191--213

Journal of Automated Reasoning
Volume 20, Number 3, June, 1998

             Guoxiang Huang and   
                     Dale Myers   Subgoal Strategies for Solving Board
                                  Puzzles  . . . . . . . . . . . . . . . . 215--253
                    Erica Melis   The Heine--Borel Challenge Problem. In
                                  Honor of Woody Bledsoe . . . . . . . . . 255--282
                 Kahlil Hodgson   Shortest Single Axioms for the
                                  Equivalential Calculus with CD and RCD   283--316
       Hans Jürgen Ohlbach   Elimination of Self-Resolving Clauses    317--336
             M. Paramasivam and   
              David A. Plaisted   Automated Deduction Techniques for
                                  Classification in Description Logic
                                  Systems  . . . . . . . . . . . . . . . . 337--364
      Abdelilah Kandri Rody and   
        Hamid Maârouf and   
                Mohamed Ssafini   Triviality and Dimension of a System of
                                  Algebraic Differential Equations . . . . 365--385
                      Anonymous   The Eleventh International Conference on
                                  Industrial and Engineering Applications
                                  of Artificial Intelligence and Expert
                                  Systems (IEA/AIE--98)  . . . . . . . . . 387--387


Journal of Automated Reasoning
Volume 21, Number 1, August, 1998

                  Li Hongbo and   
                   Cheng Minteh   Clifford Algebraic Reduction Method for
                                  Automated Theorem Proving in
                                  Differential Geometry  . . . . . . . . . 1--21
                  Hoon Hong and   
                Dalibor Jaku\vs   Testing Positiveness of Polynomials  . . 23--38
                James J. Lu and   
             Neil V. Murray and   
                 Erik Rosenthal   A Framework for Automated Reasoning in
                                  Multiple-Valued Logics . . . . . . . . . 39--67
                  Kenneth Kunen   Nonconstructive Computational
                                  Mathematics  . . . . . . . . . . . . . . 69--97
          Christian Suttner and   
                Geoff Sutcliffe   The CADE-14 ATP System Competition . . . 99--134

Journal of Automated Reasoning
Volume 21, Number 2, October, 1998

                      Larry Wos   Automating the Search for Elegant Proofs 135--175
            Geoff Sutcliffe and   
              Christian Suttner   The TPTP Problem Library . . . . . . . . 177--203
                Andrei Voronkov   Proof Search in Intuitionistic Logic
                                  with Equality, or Back to Simultaneous
                                  Rigid $E$-Unification  . . . . . . . . . 205--231
          Jacques Chazarain and   
                   Serge Muller   Automated Synthesis of Recursive
                                  Programs from a $ \forall \exists $
                                  Logical Specification  . . . . . . . . . 233--275
                      Anonymous   Announcements  . . . . . . . . . . . . . 277--277

Journal of Automated Reasoning
Volume 21, Number 3, December, 1998

               Deepak Kapur and   
                  Dongming Wang   Preface  . . . . . . . . . . . . . . . . 277--278
              John Harrison and   
                L. Théry   A Skeptic's Approach to Combining HOL
                                  and Maple  . . . . . . . . . . . . . . . 279--294
               Andrej Bauer and   
              Edmund Clarke and   
                    Xudong Zhao   Analytica-- An Experiment in Combining
                                  Theorem Proving and Symbolic Computation 295--325
             Manfred Kerber and   
           Michael Kohlhase and   
                   Volker Sorge   Integrating Computer Algebra into Proof
                                  Planning . . . . . . . . . . . . . . . . 327--355
           Andreas Dolzmann and   
               Thomas Sturm and   
            Volker Weispfenning   A New Approach for Automatic Theorem
                                  Proving in Real Geometry . . . . . . . . 357--380
                 Jinzhao Wu and   
                    Zhuojun Liu   Well-Behaved Inference Rules for
                                  First-Order Theorem Proving  . . . . . . 381--400


Journal of Automated Reasoning
Volume 22, Number 1, January, 1999

                  Larry Wos and   
                 Gail W. Pieper   The Hot List Strategy  . . . . . . . . . 1--44
            Frieder Stolzenburg   An Algorithm for General Set Unification
                                  and Its Complexity . . . . . . . . . . . 45--63
               Peter Madden and   
                 Alan Bundy and   
                    Alan Smaill   Recursive Program Optimization through
                                  Inductive Synthesis Proof Transformation 65--115

Journal of Automated Reasoning
Volume 22, Number 2, February, 1999

                Erica Melis and   
                    Jon Whittle   Analogy in Inductive Theorem Proving . . 117--147
                A. K. Shiny and   
                 Arun K. Pujari   An Efficient Algorithm to Generate Prime
                                  Implicants . . . . . . . . . . . . . . . 149--170
          William E. Aitken and   
        Robert L. Constable and   
            Judith L. Underwood   Metalogical Frameworks II: Developing a
                                  Reflected Decision Procedure . . . . . . 171--221

Journal of Automated Reasoning
Volume 22, Number 3, March, 1999

              Leon \Lukaszewicz   Triple Dots in a Formal Language . . . . 223--239
              Gilles Pesant and   
                   Michel Boyer   Reasoning about Solids Using Constraint
                                  Logic Programming  . . . . . . . . . . . 241--262
                Ofer Arieli and   
                    Arnon Avron   A Model-Theoretic Approach for
                                  Recovering Consistent Data from
                                  Inconsistent Knowledge Bases . . . . . . 263--309
         Johan G. F. Belinfante   Computer Proofs in Gödel's Class Theory
                                  with Equational Definitions for
                                  Composite and Cross  . . . . . . . . . . 311--339
         Johan G. F. Belinfante   On Computer-Assisted Proofs in Ordinal
                                  Number Theory  . . . . . . . . . . . . . 341--378

Journal of Automated Reasoning
Volume 22, Number 4, May, 1999

              Renate A. Schmidt   Decidability by Resolution for
                                  Propositional Modal Logics . . . . . . . 379--396
           Christian B. Suttner   SPS-Parallelism + SETHEO = SPTHEO  . . . 397--431
           Andrea Formisano and   
              Alberto Policriti   $T$-Resolution: Refinements and Model
                                  Elimination  . . . . . . . . . . . . . . 433--483
                      Anonymous   Author Index to Volume 22  . . . . . . . 485--486
                      Anonymous   Subject Index to Volume 22 . . . . . . . 487--487
                      Anonymous   Contents to Volume 22  . . . . . . . . . 489--490


Journal of Automated Reasoning
Volume 23, Number 1, July, 1999

               G. Sutcliffe and   
                  C. B. Suttner   The CADE-15 ATP System Competition . . . 1--23
          Masahito Kurihara and   
                  Hisashi Kondo   Completion for Multiple Reduction
                                  Orderings  . . . . . . . . . . . . . . . 25--42
               John D. Ramsdell   The Tail-Recursive SECD Machine  . . . . 43--62
                   T. Recio and   
             M. P. Vélez   Automatic Discovery of Theorems in
                                  Elementary Geometry  . . . . . . . . . . 63--82
          Alexander Brodsky and   
           Catherine Lassez and   
          Jean-Louis Lassez and   
               Michael J. Maher   Separability of Polyhedra for Optimal
                                  Filtering of Spatial and Constraint Data 83--104
                      Anonymous   Announcements  . . . . . . . . . . . . . 105--105

Journal of Automated Reasoning
Volume 23, Number 2, August, 1999

               Miki Hermann and   
            Phokion G. Kolaitis   Computational Complexity of Simultaneous
                                  Elementary Matching Problems . . . . . . 107--136
               Allen Van Gelder   Autarky Pruning in Propositional Model
                                  Elimination Reduces Failure Redundancy   137--193

Journal of Automated Reasoning
Volume 23, Number 3, November, 1999

                      Anonymous   Preface  . . . . . . . . . . . . . . . . 195--196
             Piotr Rudnicki and   
               Andrzej Trybulec   On Equivalents of Well-Foundedness . . . 197--234
     Florian Kammüller and   
            Lawrence C. Paulson   A Formal Proof of Sylow's Theorem  . . . 235--264
            Ching-Tsun Chou and   
                    Doron Peled   Formal Verification of a Partial-Order
                                  Reduction Technique for Model Checking   265--298
      Wolfgang Naraschewski and   
                  Tobias Nipkow   Type Inference Verified: Algorithm W in
                                  Isabelle/HOL . . . . . . . . . . . . . . 299--318
           Catherine Dubois and   
Valérie Ménissier-Morain   Certification of a Type Inference Tool
                                  for ML: Damas--Milner within Coq . . . . 319--346
                       M. Jaume   A Full Formalization of SLD--Resolution
                                  in the Calculus of Inductive
                                  Constructions  . . . . . . . . . . . . . 347--371
              James McKinna and   
                 Robert Pollack   Some Lambda Calculus and Type Theory
                                  Formalized . . . . . . . . . . . . . . . 373--409
                  Bernhard Reus   Formalizing Synthetic Domain Theory  . . 411--444
            David M. Goldschlag   A Mechanization of Unity in PC--NQTHM-92 445--498


Journal of Automated Reasoning
Volume 24, Number 1--2, February, 2000

                Ian P. Gent and   
                     Toby Walsh   Satisfiability in the Year 2000  . . . . 1--3
           Miron Abramovici and   
               Jose T. De Sousa   A SAT Solver Using Reconfigurable
                                  Hardware and Virtual Logic . . . . . . . 5--36
           Etienne de Klerk and   
            Hans van Maaren and   
               Joost P. Warners   Relaxations of the Satisfiability
                                  Problem Using Semidefinite Programming   37--65
             Carla P. Gomes and   
                Bart Selman and   
                 Nuno Crato and   
                    Henry Kautz   Heavy-Tailed Phenomena in Satisfiability
                                  and Constraint Satisfaction Problems . . 67--100
           Jan Friso Groote and   
               Joost P. Warners   The Propositional Formula Checker
                                  HeerHugo . . . . . . . . . . . . . . . . 101--125
               Edward A. Hirsch   SAT Local Search Algorithms: Worst-Case
                                  Study  . . . . . . . . . . . . . . . . . 127--143
      Wolfgang Küchlin and   
                   Carsten Sinz   Proving Consistency Assertions for
                                  Automotive Product Data Management . . . 145--163
             Fabio Massacci and   
                  Laura Marraro   Logical Cryptanalysis as a SAT Problem   165--203
              Patrick Mills and   
                   Edward Tsang   Guided Local Search for Solving SAT and
                                  Weighted MAX--SAT Problems . . . . . . . 205--223
                 Irina Rish and   
                   Rina Dechter   Resolution versus Search: Two Strategies
                                  for SAT  . . . . . . . . . . . . . . . . 225--275
               Hantao Zhang and   
                   Mark Stickel   Implementing the Davis--Putnam Method    277--296

Journal of Automated Reasoning
Volume 24, Number 3, April, 2000

             Peter Balsiger and   
            Alain Heuerding and   
            Stefan Schwendimann   A Benchmark Method for the Propositional
                                  Modal Logics K, KT, S4 . . . . . . . . . 297--317
                 Fabio Massacci   Single Step Tableaux for Modal Logics    319--364
             R. Padmanabhan and   
                      P. Penner   A Hyperbase for Binary Lattice
                                  Hyperidentities  . . . . . . . . . . . . 365--370
                Geoff Sutcliffe   The CADE-16 ATP System Competition . . . 371--396

Journal of Automated Reasoning
Volume 24, Number 4, May, 2000

               Edward A. Hirsch   New Worst-Case Upper Bounds for SAT  . . 397--420
             Holger H. Hoos and   
            Thomas Stützle   Local Search Algorithms for SAT: An
                                  Empirical Evaluation . . . . . . . . . . 421--481
         E. Thomas Richards and   
                 Barry Richards   Nonsystematic Search and No-Good
                                  Learning . . . . . . . . . . . . . . . . 483--533


Journal of Automated Reasoning
Volume 25, Number 1, July, 2000

              Bruce Spencer and   
                   J. D. Horton   Efficient Algorithms to Detect and
                                  Restore Minimality, an Extension of the
                                  Regular Restriction of Resolution  . . . 1--34
        François Bry and   
                    Adnan Yahya   Positive Unit Hyperresolution Tableaux
                                  and Their Application to Minimal Model
                                  Generation . . . . . . . . . . . . . . . 35--82

Journal of Automated Reasoning
Volume 25, Number 2, August, 2000

                      Hongbo Li   Vectorial Equations Solving for
                                  Mechanical Geometry Theorem Proving  . . 83--121
              Dieter Hutter and   
               Michael Kohlhase   Managing Structural Information by
                                  Higher-Order Colored Unification . . . . 123--164
                      Anonymous   Erratum  . . . . . . . . . . . . . . . . 165--165

Journal of Automated Reasoning
Volume 25, Number 3, October, 2000

          David A. Plaisted and   
                    Yunshan Zhu   Ordered Semantic Hyper-Linking . . . . . 167--217
           Shang-Ching Chou and   
              Xiao-Shan Gao and   
               Jing-Zhong Zhang   A Deductive Database Approach to
                                  Automated Geometry Theorem Proving and
                                  Discovering  . . . . . . . . . . . . . . 219--246

Journal of Automated Reasoning
Volume 25, Number 4, November, 2000

              Marek A. Suchenek   Evaluation of Queries under Closed-World
                                  Assumption. Part II: The Hierarchical
                                  Case . . . . . . . . . . . . . . . . . . 247--289
           A. Prasad Sistla and   
                     Clement Yu   Reasoning about Qualitative Spatial
                                  Relationships  . . . . . . . . . . . . . 291--328
                      Anonymous   Author Index to Volume 25  . . . . . . . 329--329
                      Anonymous   Subject Index to Volume 25 . . . . . . . 331--332
                      Anonymous   Contents to Volume 25  . . . . . . . . . 333--334


Journal of Automated Reasoning
Volume 26, Number 1, January, 2001

              Jürgen Giesl   Induction Proofs with Partial Functions  1--49
                  Tobias Nipkow   More Church--Rosser Proofs . . . . . . . 51--66
               Chih-Hung Wu and   
                   Shie-Jue Lee   Parallelization of a Hyper-Linking-Based
                                  Theorem Prover . . . . . . . . . . . . . 67--106

Journal of Automated Reasoning
Volume 26, Number 2, February, 2001

           Laurent Théry   A Machine-Checked Implementation of
                                  Buchberger's Algorithm . . . . . . . . . 107--137
            Wolfgang Gehrke and   
               Jochen Pfalzgraf   Computer-Aided Construction of Finite
                                  Geometric Spaces: Automated Verification
                                  of Geometric Constraints . . . . . . . . 139--160
              Matt Kaufmann and   
              J. Strother Moore   Structured Theory Development for a
                                  Mechanized Logic . . . . . . . . . . . . 161--203
              Ulrich Berger and   
      Helmut Schwichtenberg and   
            Monika Seisenberger   The Warshall Algorithm and Dickson's
                                  Lemma: Two Examples of Realistic Program
                                  Extraction . . . . . . . . . . . . . . . 205--221

Journal of Automated Reasoning
Volume 26, Number 3, April, 2001

       Jürgen Avenhaus and   
              David A. Plaisted   General Algorithms for Permutations in
                                  Equational Inference . . . . . . . . . . 223--268
              William M. Farmer   STMM: A Set Theory for Mechanized
                                  Mathematics  . . . . . . . . . . . . . . 269--289
             F. Giunchiglia and   
               P. Pecchiari and   
                     C. Talcott   Reasoning Theories . . . . . . . . . . . 291--331

Journal of Automated Reasoning
Volume 26, Number 4, May, 2001

                  C. A. Johnson   On the Computation of the Disjunctive
                                  Well-Founded Semantics . . . . . . . . . 333--356
          M. Randall Holmes and   
                 Jim Alves-Foss   The Watson Theorem Prover  . . . . . . . 357--408
              Robert McNaughton   Semi-Thue Systems with an Inhibitor  . . 409--431
                      Anonymous   Author Index to Volume 26  . . . . . . . 433--433
                      Anonymous   Subject Index to Volume 26 . . . . . . . 435--435
                      Anonymous   Contents to Volume 26  . . . . . . . . . 437--438


Journal of Automated Reasoning
Volume 27, Number 1, July, 2001

                David Basin and   
                      Amy Felty   Current Trends in Logical Frameworks and
                                  Metalanguages  . . . . . . . . . . . . . 1--2
             Paul Callaghan and   
                    Zhaohui Luo   An Implementation of LF with Coercive
                                  Subtyping & Universes . . . . . . . . . . 3--27
               Mirna Bognar and   
                 Roel de Vrijer   A Calculus of Lambda Calculus Contexts   29--59
               Paula Severi and   
                     Nora Szasz   Studies of a Theory of Specifications
                                  with Built-in Program Extraction . . . . 61--87

Journal of Automated Reasoning
Volume 27, Number 2, August, 2001

                      Larry Wos   A Milestone Reached and a Secret
                                  Revealed . . . . . . . . . . . . . . . . 89--95
                   Dolph Ulrich   A Legacy Recalled and a Tradition
                                  Continued  . . . . . . . . . . . . . . . 97--122
                  Robert Veroff   Finding Shortest Proofs: An Application
                                  of Linked Inference Rules  . . . . . . . 123--139
             Kenneth Harris and   
               Branden Fitelson   Distributivity in $ {\L } \aleph_0 $ and
                                  Other Sentential Logics  . . . . . . . . 141--156
                  Robert Veroff   Solving Open Questions and Other
                                  Challenge Problems Using Proof Sketches  157--174
                      Larry Wos   Conquering the Meredith Single Axiom . . 175--199
           Branden Fitelson and   
                      Larry Wos   Missing Proofs Found . . . . . . . . . . 201--225

Journal of Automated Reasoning
Volume 27, Number 3, October, 2001

                   G. Sutcliffe   The CADE-17 ATP System Competition . . . 227--250
         Michael L. Littman and   
        Stephen M. Majercik and   
                Toniann Pitassi   Stochastic Boolean Satisfiability  . . . 251--296
                  Guido Fiorino   An $ O(n \log n)$-SPACE Decision
                                  Procedure for the Propositional Dummett
                                  Logic  . . . . . . . . . . . . . . . . . 297--311
                      Lifeng He   I-SATCHMO: An Improvement of SATCHMO . . 313--322

Journal of Automated Reasoning
Volume 27, Number 4, November, 2001

            Ruben A. Gamboa and   
                  Matt Kaufmann   Nonstandard Analysis in ACL2 . . . . . . 323--351
      Guilherme Bittencourt and   
                   Isabel Tonin   An Algorithm for Dual Transformation in
                                  First-Order Logic  . . . . . . . . . . . 353--389
                  P. A. Bonatti   Resolution for Skeptical Stable Model
                                  Semantics  . . . . . . . . . . . . . . . 391--421
                      Anonymous   Author Index to Volume 27  . . . . . . . 423--423
                      Anonymous   Subject Index to Volume 27 . . . . . . . 425--425
                      Anonymous   Contents to Volume 27  . . . . . . . . . 427--428


Journal of Automated Reasoning
Volume 28, Number 1, January, 2002

                 Adnan H. Yahya   Duality for Goal-Driven Query Processing
                                  in Disjunctive Deductive Databases . . . 1--34
                    Steven Eker   Single Elementary
                                  Associative--Commutative Matching  . . . 35--51
               Yi-Dong Shen and   
                Li-Yan Yuan and   
                   Jia-Huai You   SLT-Resolution for the Well-Founded
                                  Semantics  . . . . . . . . . . . . . . . 53--97

Journal of Automated Reasoning
Volume 28, Number 2, February, 2002

                Ian P. Gent and   
                     Toby Walsh   Satisfiability in the Year 2000  . . . . 99--99
               Marco Cadoli and   
              Marco Schaerf and   
          Andrea Giovanardi and   
             Massimo Giovanardi   An Algorithm to Evaluate Quantified
                                  Boolean Formulae and Its Experimental
                                  Evaluation . . . . . . . . . . . . . . . 101--142
         Enrico Giunchiglia and   
          Armando Tacchella and   
             Fausto Giunchiglia   SAT-Based Decision Procedures for
                                  Classical Modal Logics . . . . . . . . . 143--171
               Ian Horrocks and   
       Peter F. Patel-Schneider   Evaluating Optimized Decision Procedures
                                  for Propositional Modal $ K_{(m)} $
                                  Satisfiability . . . . . . . . . . . . . 173--204
            Ullrich Hustadt and   
              Renate A. Schmidt   Using Resolution for Testing Modal
                                  Satisfiability and Building Models . . . 205--232
                      Anonymous   Erratum  . . . . . . . . . . . . . . . . 233--233

Journal of Automated Reasoning
Volume 28, Number 3, April, 2002

            Robert Cremanns and   
                 Friedrich Otto   A Completion Procedure for Finitely
                                  Presented Groups That Is Based on Word
                                  Cycles . . . . . . . . . . . . . . . . . 235--256
        Predrag Jani\vci\'c and   
                     Alan Bundy   A General Setting for Flexibly Combining
                                  and Augmenting Decision Procedures . . . 257--305
               G. Sutcliffe and   
              C. B. Suttner and   
                F. J. Pelletier   The IJCAR ATP System Competition . . . . 307--320
            Henk Barendregt and   
                 Erik Barendsen   Autarkic Computations in Formal Proofs   321--336

Journal of Automated Reasoning
Volume 28, Number 4, May, 2002

                  Teodor Knapik   Checking Simple Properties of Transition
                                  Systems Defined by Thue Specifications   337--369
               J. N. Hooker and   
                    G. Rago and   
                 V. Chandru and   
                 A. Shrivastava   Partial Instantiation Methods for
                                  Inference in First-Order Logic . . . . . 371--396
           Angelo Montanari and   
          Alberto Policriti and   
                 Matteo Slanina   Alternative Translation Techniques for
                                  Propositional and First-Order Modal
                                  Logics . . . . . . . . . . . . . . . . . 397--415
                Eugene Goldberg   Proving Unsatisfiability of CNFs Locally 417--434
                      Anonymous   Author Index to Volume 28  . . . . . . . 435--435
                      Anonymous   Subject Index to Volume 28 . . . . . . . 437--437
                      Anonymous   Contents to Volume 28  . . . . . . . . . 439--440


Journal of Automated Reasoning
Volume 29, Number 1, January, 2002

             William McCune and   
              Robert Veroff and   
           Branden Fitelson and   
             Kenneth Harris and   
               Andrew Feist and   
                      Larry Wos   Short Single Axioms for Boolean Algebra  1--16
                Adnan Yahya and   
              David A. Plaisted   Ordered Semantic Hyper Tableaux  . . . . 17--57
                    John Slaney   More Proofs of an Axiom of \Lukasiewicz  59--66
            Ruediger Thiele and   
                      Larry Wos   Hilbert's Twenty-Fourth Problem  . . . . 67--89
            Vivek S. Borkar and   
              Vijay Chandru and   
               Sanjoy K. Mitter   Mathematical Programming Embeddings of
                                  Logic  . . . . . . . . . . . . . . . . . 91--106

Journal of Automated Reasoning
Volume 29, Number 2, February, 2002

                  Larry Wos and   
               Dolph Ulrich and   
               Branden Fitelson   Vanquishing the XCB Question: The
                                  Methodological Discovery of the Last
                                  Shortest Single Axiom for the
                                  Equivalential Calculus . . . . . . . . . 107--124
               Leila Amgoud and   
               Claudette Cayrol   Inferring from Inconsistency in
                                  Preference-Based Argumentation
                                  Frameworks . . . . . . . . . . . . . . . 125--169
                 G. Mashevitzky   Unification Types of Completely Regular
                                  Semigroups . . . . . . . . . . . . . . . 171--182

Journal of Automated Reasoning
Volume 29, Number 3--4, September, 2002

            Fairouz Kamareddine   Preface: Mechanizing and Automating
                                  Mathematics: In honour of N. G. de
                                  Bruijn . . . . . . . . . . . . . . . . . 183--188
          Grzegorz Bancerek and   
                 Piotr Rudnicki   A Compendium of Continuous Lattices in
                                  MIZAR  . . . . . . . . . . . . . . . . . 189--224
                Yves Bertot and   
             Nicolas Magaud and   
                Paul Zimmermann   A Proof of GMP Square Root . . . . . . . 225--252
                 Marc Bezem and   
           Dimitri Hendriks and   
                Hans de Nivelle   Automated Proof Construction in Type
                                  Theory Using Resolution  . . . . . . . . 253--275
               Dimitri Hendriks   Proof Reflection in Coq  . . . . . . . . 277--307
           Quang Huy Nguyen and   
            Claude Kirchner and   
       Hél\`ene Kirchner   External Rewriting for Skeptical Proof
                                  Assistants . . . . . . . . . . . . . . . 309--336
           Virgile Prevosto and   
                 Damien Doligez   Algorithms and Proofs Inheritance in the
                                  FOC Language . . . . . . . . . . . . . . 337--363
                  Freek Wiedijk   A New Implementation of Automath . . . . 365--387
              Markus Wenzel and   
                  Freek Wiedijk   A Comparison of Mizar and Isar . . . . . 389--411
                      Anonymous   Author Index to Volume 29  . . . . . . . 413--413
                      Anonymous   Subject Index to Volume 29 . . . . . . . 415--415
                      Anonymous   Contents to Volume 29  . . . . . . . . . 417--418


Journal of Automated Reasoning
Volume 30, Number 1, January, 2003

                 Cesare Tinelli   Cooperation of Background Reasoners in
                                  Theory Reasoning by Residue Sharing  . . 1--31
          Antonella Santone and   
               Gigliola Vaglini   Modifying LOTOS Specifications by Means
                                  of Automatable Formula-Based
                                  Integrations . . . . . . . . . . . . . . 33--58
        Fairouz Kamareddine and   
                    Haiyan Qiao   Formalizing Strong Normalization Proofs
                                  of Explicit Substitution Calculi in ALF  59--98
              Miquel Bofill and   
              Guillem Godoy and   
         Robert Nieuwenhuis and   
                   Albert Rubio   Paramodulation and Knuth--Bendix
                                  Completion with Nontotal and
                                  Nonmonotonic Orderings . . . . . . . . . 99--120

Journal of Automated Reasoning
Volume 30, Number 2, February, 2003

                Andrei Voronkov   Proof-Search in Intuitionistic Logic
                                  with Equality, or Back to Simultaneous
                                  Rigid $E$-Unification  . . . . . . . . . 121--151
   Michaël Rusinowitch and   
            Sorin Stratulat and   
                   Francis Klay   Mechanical Verification of an Ideal
                                  Incremental ABR Conformance Algorithm    153--177
                      Larry Wos   The Strategy of Cramming . . . . . . . . 179--204
      Krishnendu Chatterjee and   
            Pallab Dasgupta and   
              P. P. Chakrabarti   A Branching Time Temporal Framework for
                                  Quantitative Reasoning . . . . . . . . . 205--232

Journal of Automated Reasoning
Volume 30, Number 3--4, May, 2003

                  Tobias Nipkow   Java Bytecode Verification . . . . . . . 233--233
                   Xavier Leroy   Java Bytecode Verification: Algorithms
                                  and Formalizations . . . . . . . . . . . 235--269
          Stephen N. Freund and   
               John C. Mitchell   A Type System for the Java Bytecode
                                  Language and Verifier  . . . . . . . . . 271--321
       Robert F. Stärk and   
                 Joachim Schmid   Completeness of a Bytecode Verifier and
                                  a Certifying Java-to-JVM Compiler  . . . 323--361
                   G. Klein and   
                   M. Wildmoser   Verified Bytecode Subroutines  . . . . . 363--398
             David A. Basin and   
           Stefan Friedrich and   
                Marek Gawkowski   Bytecode Verification by Model Checking  399--444
                      Anonymous   Author Index to Volume 30  . . . . . . . 445--445
                      Anonymous   Subject Index to Volume 30 . . . . . . . 447--447
                      Anonymous   Contents to Volume 30  . . . . . . . . . 449--450


Journal of Automated Reasoning
Volume 31, Number 1, September, 2003

                  Robert Veroff   A Shortest $2$-Basis for Boolean Algebra
                                  in Terms of the Sheffer Stroke . . . . . 1--9
                    Lin Hai and   
                  Sun Jigui and   
                    Zhang Yimin   Theorem Proving Based on the Extension
                                  Rule . . . . . . . . . . . . . . . . . . 11--21
               G. Sutcliffe and   
                  C. B. Suttner   The CADE-18 ATP System Competition . . . 23--32
               Gilles Dowek and   
    Thér\`ese Hardin and   
                Claude Kirchner   Theorem Proving Modulo . . . . . . . . . 33--72
               R. Gentilini and   
                  C. Piazza and   
                   A. Policriti   From Bisimulation to Simulation:
                                  Coarsest Partition Problems  . . . . . . 73--103

Journal of Automated Reasoning
Volume 31, Number 2, October, 2003

                   Deepak Kapur   Announcement . . . . . . . . . . . . . . 105--105
        Panagiotis Manolios and   
              J. Strother Moore   Partial Functions in ACL2  . . . . . . . 107--127
               Leo Bachmair and   
              Ashish Tiwari and   
               Laurent Vigneron   Abstract Congruence Closure  . . . . . . 129--168
               Peter B. Andrews   Herbrand Award Acceptance Speech . . . . 169--187

Journal of Automated Reasoning
Volume 31, Number 3--4, November, 2003

                   Amy P. Felty   Preface  . . . . . . . . . . . . . . . . 189--190
            Nadeem A. Hamid and   
                 Zhong Shao and   
            Valery Trifonov and   
             Stefan Monnier and   
                   Zhaozhong Ni   A Syntactic Approach to Foundational
                                  Proof-Carrying Code  . . . . . . . . . . 191--229
            Andrew W. Appel and   
          Neophytos Michael and   
                Aaron Stump and   
                  Roberto Virga   A Trustworthy Proof Checker  . . . . . . 231--260
             David Aspinall and   
             Adriana Compagnoni   Heap-Bounded Assembly Language . . . . . 261--302
                       Eva Rose   Lightweight Bytecode Verification  . . . 303--334
                James Riely and   
               Matthew Hennessy   Trust and Partial Typing in Open Systems
                                  of Mobile Agents . . . . . . . . . . . . 335--370
                      Anonymous   Author Index to Volume 31  . . . . . . . 371--371
                      Anonymous   Subject Index to Volume 31 . . . . . . . 373--373
                      Anonymous   Contents to Volume 31  . . . . . . . . . 375--376


Journal of Automated Reasoning
Volume 32, Number 1, January, 2004

                   Deepak Kapur   Preface  . . . . . . . . . . . . . . . . 1--2
             Noboru Matsuda and   
                   Kurt VanLehn   GRAMY: A Geometry Theorem Prover Capable
                                  of Construction  . . . . . . . . . . . . 3--33
          Christoph Walther and   
             Stephan Schweitzer   Verification in the Classroom  . . . . . 35--73
           Peter B. Andrews and   
              Chad E. Brown and   
             Frank Pfenning and   
             Matthew Bishop and   
                Sunil Issar and   
                     Hongwei Xi   ETPS: A System to Help Students Write
                                  Formal Proofs  . . . . . . . . . . . . . 75--92

Journal of Automated Reasoning
Volume 32, Number 2, February, 2004

                    Lin Hai and   
                      Sun Jigui   Knowledge Compilation Using the
                                  Extension Rule . . . . . . . . . . . . . 93--102
           Harald Ganzinger and   
         Robert Nieuwenhuis and   
                   Pilar Nivela   Fast Term Indexing with Coded Context
                                  Trees  . . . . . . . . . . . . . . . . . 103--120
           Christoph Kreitz and   
                   Heiko Mantel   A Matrix Characterization for
                                  Multiplicative Exponential Linear Logic  121--166
                  C. A. Johnson   Top-Down Query Processing in First-Order
                                  Deductive Databases under the DWFS . . . 167--184

Journal of Automated Reasoning
Volume 32, Number 3, February, 2004

                   Deepak Kapur   Preface  . . . . . . . . . . . . . . . . 185--186
            Maxim Makatchev and   
           Pamela W. Jordan and   
                   Kurt VanLehn   Abductive Theorem Proving for Analyzing
                                  Student Explanations to Guide Feedback
                                  in Intelligent Tutoring Systems  . . . . 187--226
             Richard Sommer and   
                Gregory Nuckols   A Proof Environment for Teaching
                                  Mathematics  . . . . . . . . . . . . . . 227--258
             P. Baumgartner and   
                 U. Furbach and   
             M. Gross-Hardt and   
                      A. Sinner   Living Book-- Deduction, Slicing, and
                                  Interaction  . . . . . . . . . . . . . . 259--286

Journal of Automated Reasoning
Volume 32, Number 4, December, 2004

                   Deepak Kapur   Obituary . . . . . . . . . . . . . . . . ??
Francisco-Jesús Martín-Mateos and   
 José-Antonio Alonso and   
María-José Hidalgo and   
    José-Luis Ruiz-Reina   Formal verification of a generic
                                  framework to synthesize SAT-provers  . . ??
                  Xavier Urbain   Modular and Incremental Automated
                                  Termination Proofs . . . . . . . . . . . ??


Journal of Automated Reasoning
Volume 33, Number 1, July, 2004

          Siva Anantharaman and   
          Paliath Narendran and   
            Michael Rusinowitch   Unification Modulo ACUI Plus
                                  Distributivity Axioms  . . . . . . . . . 1--28
            Lawrence C. Paulson   Organizing Numerical Theories Using
                                  Axiomatic Type Classes . . . . . . . . . 29--49
         Jürgen Zimmer and   
                    Erica Melis   Constraint Solving for Proof Planning    51--88

Journal of Automated Reasoning
Volume 33, Number 2, September, 2004

                Chuck Liang and   
           Gopalan Nadathur and   
                     Xiaochu Qi   Choices in Representation and Reduction
                                  Strategies for Lambda Terms in
                                  Intensional Contexts . . . . . . . . . . 89--132
                     N. Peltier   Representing and Building Models for
                                  Decidable Subclasses of Equational
                                  Clausal Logic  . . . . . . . . . . . . . 133--170
              Monty Newborn and   
                   Zongyan Wang   Octopus: Combining Learning and Parallel
                                  Search . . . . . . . . . . . . . . . . . 171--218

Journal of Automated Reasoning
Volume 33, Number 3--4, October / December, 2004

               Deepak Kapur and   
               Laurent Vigneron   Preface  . . . . . . . . . . . . . . . . 219--220
                Silvio Ghilardi   Model-Theoretic Methods in Combined
                                  Constraint Satisfiability  . . . . . . . 221--249
          Calogero G. Zarba and   
           Domenico Cantone and   
              Jacob T. Schwartz   A Decision Procedure for a Sublanguage
                                  of Set Theory Involving Monotone,
                                  Additive, and Multiplicative Functions,
                                  I: The Two-Level Case  . . . . . . . . . 251--269
     Thierry Boy de la Tour and   
                 Mnacho Echenim   On the Complexity of Deduction Modulo
                                  Leaf Permutative Equations . . . . . . . 271--317
                    Josef Urban   MPTP --- Motivation, Implementation,
                                  First Experiments  . . . . . . . . . . . 319--339
        Guillaume Feuillade and   
               Thomas Genet and   
 Valérie Viet Triem Tong   Reachability Analysis over Term
                                  Rewriting Systems  . . . . . . . . . . . 341--383


Journal of Automated Reasoning
Volume 34, Number 1, January, 2005

              Calogero G. Zarba   Combining Sets with Cardinals  . . . . . 1--29
             Anja Remshagen and   
                 Klaus Truemper   An Effective Algorithm for the Futile
                                  Questioning Problem  . . . . . . . . . . 31--47
           Domenico Cantone and   
          Calogero G. Zarba and   
           Rosa Ruggeri Cannata   A Tableau-Based Decision Procedure for a
                                  Fragment of Set Theory with Iterated
                                  Membership . . . . . . . . . . . . . . . 49--72
          Bernard Jurkowiak and   
                 Chu Min Li and   
                      Gil Utard   A Parallelization Scheme Based on Work
                                  Stealing for a Class of SAT Solvers  . . 73--101

Journal of Automated Reasoning
Volume 34, Number 2, December, 2005

          Jürgen Giesl and   
                   Deepak Kapur   Preface  . . . . . . . . . . . . . . . . 103--104
                     H. Zantema   Termination of String Rewriting Proved
                                  Automatically  . . . . . . . . . . . . . 105--139
       Alexander Serebrenik and   
               Danny De Schreye   Termination of Floating-Point
                                  Computations . . . . . . . . . . . . . . 141--177
               Brigitte Pientka   Verifying Termination and Reduction
                                  Properties about Higher-Order Logic
                                  Programs . . . . . . . . . . . . . . . . 179--207

Journal of Automated Reasoning
Volume 34, Number 3, April, 2005

             Cesare Tinelli and   
              Calogero G. Zarba   Combining Nonstably Infinite Theories    209--238
           Konstantine Arkoudas   Simplifying Proofs in Fitch-Style
                                  Natural Deduction Systems  . . . . . . . 239--294
M. C. Fernández-Gago and   
                 U. Hustadt and   
                   C. Dixon and   
                  M. Fisher and   
                       B. Konev   First-Order Temporal Verification in
                                  Practice . . . . . . . . . . . . . . . . 295--321

Journal of Automated Reasoning
Volume 34, Number 4, May, 2005

           Jügen Giesl and   
                   Deepak Kapur   Preface  . . . . . . . . . . . . . . . . 323--323
               Alfons Geser and   
            Dieter Hofbauer and   
              Johannes Waldmann   Termination Proofs for String Rewriting
                                  Systems via Inverse Match-Bounds . . . . 365--385
        Panagiotis Manolios and   
                    Daron Vroon   Ordinal Arithmetic: Algorithms and
                                  Mechanization  . . . . . . . . . . . . . 387--423
          Evelyne Contejean and   
       Claude Marché and   
     Ana Paula Tomás and   
                  Xavier Urbain   Mechanically Proving Termination Using
                                  Polynomial Interpretations . . . . . . . ??


Journal of Automated Reasoning
Volume 35, Number 1--3, October, 2005

         Enrico Giunchiglia and   
                     Toby Walsh   Satisfiability in the Year 2005  . . . . 1--2
               Ateet Bhalla and   
           Inês Lynce and   
    José T. de Sousa and   
      João Marques-Silva   Heuristic-Based Backtracking Relaxation
                                  for Propositional Satisfiability . . . . 3--24
               Guoqiang Pan and   
                 Moshe Y. Vardi   Symbolic Techniques in Satisfiability
                                  Solving  . . . . . . . . . . . . . . . . 25--50
        Michael Alekhnovich and   
           Edward A. Hirsch and   
                Dmitry Itsykson   Exponential Lower Bounds for the Running
                                  Time of DPLL Algorithms on Satisfiable
                                  Formulas . . . . . . . . . . . . . . . . 51--72
                 Stefan Szeider   Backdoor Sets for DLL Subsolvers . . . . 73--88
                  Jan Johannsen   The Complexity of Pure Literal
                                  Elimination  . . . . . . . . . . . . . . 89--95
                  John Thornton   Clause Weighting Local Search for SAT    97--142
             Alan M. Frisch and   
        Timothy J. Peugniez and   
         Anthony J. Doggett and   
           Peter W. Nightingale   Solving Non--Boolean Satisfiability
                                  Problems with Stochastic Local Search: A
                                  Comparison of Encodings  . . . . . . . . 143--179
            Yacine Boufkhad and   
             Olivier Dubois and   
            Yannet Interian and   
                    Bart Selman   Regular Random $k$-SAT: Properties of
                                  Balanced Formulas  . . . . . . . . . . . 181--200
              Andreas Meier and   
                   Volker Sorge   Applying SAT Solving in Classification
                                  of Finite Algebras . . . . . . . . . . . 201--235
         Alessandro Armando and   
         Claudio Castellini and   
         Enrico Giunchiglia and   
                  Marco Maratea   The SAT-based Approach to Separation
                                  Logic  . . . . . . . . . . . . . . . . . 237--263
              Marco Bozzano and   
        Roberto Bruttomesso and   
         Alessandro Cimatti and   
             Tommi Junttila and   
           Peter van Rossum and   
             Stephan Schulz and   
             Roberto Sebastiani   M ath SAT: Tight Integration of SAT and
                                  Mathematical Decision Procedures . . . . 265--293

Journal of Automated Reasoning
Volume 35, Number 4, November, 2005

              Gilles Barthe and   
            Pierre Courtieu and   
            Guillaume Dufay and   
     Simão Melo de Sousa   Tool-Assisted Specification and
                                  Verification of Typed Low--Level
                                  Languages  . . . . . . . . . . . . . . . 295--354
            Robert S. Boyer and   
          Wilfred J. Legato and   
                Victor W. Marek   Toward Automating the Discovery of
                                  Decreasing Measures  . . . . . . . . . . 355--371
              Clark Barrett and   
          Leonardo de Moura and   
                    Aaron Stump   Design and Results of the First
                                  Satisfiability Modulo Theories
                                  Competition (SMT-COMP 2005)  . . . . . . 373--390
                     N. Peltier   Some Techniques for Proving Termination
                                  of the Hyperresolution Calculus  . . . . 391--427
                    Nimish Shah   Book Review: \booktitleRippling:
                                  Meta-Level Guidance for Mathematical
                                  Reasoning, by Alan Bundy, David Basin,
                                  Dieter Hutter, and Andrew Ireland,
                                  Cambridge University Press, 2005 . . . . 429--431


Journal of Automated Reasoning
Volume 36, Number 1--2, January, 2006

         Alessandro Armando and   
                David Basin and   
                  Jorge Cuellar   Automated Reasoning for Security
                                  Protocol Analysis  . . . . . . . . . . . 1--3
            Giampaolo Bella and   
             Fabio Massacci and   
            Lawrence C. Paulson   Verifying the SET Purchase Protocols . . 5--37
               Rohit Chadha and   
               Steve Kremer and   
                  Andre Scedrov   Formal Analysis of Multiparty Contract
                                  Signing  . . . . . . . . . . . . . . . . 39--83
   Stéphanie Delaune and   
             Florent Jacquemard   Decision Procedures for the Security of
                                  Protocols with Probabilistic Encryption
                                  against Offline Dictionary Attacks . . . 85--124
           Hans Hüttel and   
             Ji\vrí Srba   Decidability Issues for Extended
                                  Ping--Pong Protocols . . . . . . . . . . 125--147
               Graham Steel and   
                     Alan Bundy   Attacking Group Protocols by Refuting
                                  Incorrect Inductive Conjectures  . . . . 149--176

Journal of Automated Reasoning
Volume 36, Number 3, April, 2006

            Gilles Audemard and   
         Bela\"\id Benhamou and   
               Laurent Henocque   Predicting and Detecting Symmetries in
                                  FOL Finite Model Search  . . . . . . . . 177--212
              Viktor Kuncak and   
             Huu Hai Nguyen and   
                  Martin Rinard   Deciding Boolean Algebra with Presburger
                                  Arithmetic . . . . . . . . . . . . . . . 213--239
              Nick C. Fiala and   
                  Keith M. Agre   Searching for Shortest Single Axioms for
                                  Groups of Exponent 6 . . . . . . . . . . 241--257
                 Carlos Simpson   Explaining Gabriel--Zisman Localization
                                  to the Computer  . . . . . . . . . . . . 259--285

Journal of Automated Reasoning
Volume 36, Number 4, April, 2006

              Bernd Fischer and   
            Geoff Sutcliffe and   
                 Stephan Schulz   Empirically Successful Automated
                                  Reasoning: Systems Issue . . . . . . . . 287--287
             Bernd Löchner   Things to Know when Implementing KBO . . 289--310
                 Michael Beeson   Mathematical Induction in Otter--Lambda  311--344
             Andrew Ireland and   
              Bill J. Ellis and   
                Andrew Cook and   
           Roderick Chapman and   
                   Janet Barnes   An Integrated Approach to High Integrity
                                  Software Verification  . . . . . . . . . 379--410
         Enrico Giunchiglia and   
             Yuliya Lierler and   
                  Marco Maratea   Answer Set Programming Based on
                                  Propositional Satisfiability . . . . . . ??


Journal of Automated Reasoning
Volume 37, Number 1--2, August, 2006

              Bernd Fischer and   
            Geoff Sutcliffe and   
                 Stephan Schulz   Empirically Successful Automated
                                  Reasoning: Applications Issue  . . . . . 1--1
                  R. Veroff and   
                      M. Spinks   Axiomatizing the Skew Boolean
                                  Propositional Calculus . . . . . . . . . 3--20
                    Josef Urban   MPTP 0.2: Design, Implementation, and
                                  Initial Experiments  . . . . . . . . . . 21--43
               Carsten Sinz and   
      Wolfgang Küchlin and   
             Dieter Feichtinger   Checking Consistency and Completeness of
                                  On-Line Product Manuals  . . . . . . . . 45--66
José-Luis Ruiz-Reina and   
Francisco-Jesús Martín-Mateos and   
 José-Antonio Alonso and   
María-José Hidalgo   Formal Correctness of a Quadratic
                                  Unification Algorithm  . . . . . . . . . 67--92
        Panagiotis Manolios and   
        Sudarshan K. Srinivasan   A Framework for Verifying Bit-Level
                                  Pipelined Machines Based on Automated
                                  Deduction and Decision Procedures  . . . 93--116
                    Oliver Pell   Verification of FPGA Layout Generators
                                  in Higher-Order Logic  . . . . . . . . . 117--152

Journal of Automated Reasoning
Volume 37, Number 3, October, 2006

          Jürgen Giesl and   
                   Deepak Kapur   Third Special Issue on Techniques for
                                  Automated Termination Proofs . . . . . . 153--154
          Jürgen Giesl and   
       René Thiemann and   
       Peter Schneider-Kamp and   
                  Stephan Falke   Mechanizing and Improving Dependency
                                  Pairs  . . . . . . . . . . . . . . . . . 155--203
        Kusakari Keiichirou and   
            Nakamura Masaki and   
               Toyama Yoshihito   Elimination Transformations for
                                  Associative--Commutative Rewriting
                                  Systems  . . . . . . . . . . . . . . . . 205--229

Journal of Automated Reasoning
Volume 37, Number 4, November, 2006

           Olivier Bailleux and   
                 Pierre Marquis   Some Computational Aspects of
                                  distance-sat . . . . . . . . . . . . . . 231--260
              Gilles Dequen and   
                 Olivier Dubois   An Efficient Approach to Solving Random
                                  $k$-SAT Problems . . . . . . . . . . . . 261--276
                  Steven Givant   The Calculus of Relations as a
                                  Foundation for Mathematics . . . . . . . 277--322
     Sébastien Limet and   
                  Gernot Salzer   Tree Tuple Languages from the Logic
                                  Programming Point of View  . . . . . . . 323--349


Journal of Automated Reasoning
Volume 38, Number 1--3, April, 2007

           Bernhard Beckert and   
            Lawrence C. Paulson   Preface  . . . . . . . . . . . . . . . . 1--2
             Roger Antonsen and   
                   Arild Waaler   Liberalized Variable Splitting . . . . . 3--30
           Domenico Cantone and   
      Marianna Nicolosi-Asmundo   A Sound Framework for $ \delta $-Rule
                                  Variants in Free-Variable Semantic
                                  Tableaux . . . . . . . . . . . . . . . . 31--56
                Swen Jacobs and   
                   Uwe Waldmann   Comparing Instance Generation Methods
                                  for Automated Reasoning  . . . . . . . . 57--78
              Reinhold Letz and   
                   Gernot Stenz   The Disconnection Tableau Calculus . . . 79--126
                   Martin Giese   Superposition-based Equality Handling
                                  for Analytic Tableaux  . . . . . . . . . 127--153
             Neil V. Murray and   
                 Erik Rosenthal   Efficient Query Processing with Reduced
                                  Implicate Tries  . . . . . . . . . . . . 155--172
            Davide Bresolin and   
           Angelo Montanari and   
                Guido Sciavicco   An Optimal Decision Procedure for Right
                                  Propositional Neighborhood Logic . . . . 173--199
     Dominique Larchey-Wendling   Graph-based Decision for Gödel--Dummett
                                  Logics . . . . . . . . . . . . . . . . . 201--225
               Carsten Lutz and   
               Maja Mili\vci\'c   A Tableau Algorithm for Description
                                  Logics with Concrete Domains and General
                                  TBoxes . . . . . . . . . . . . . . . . . 227--259
               Thomas Raths and   
                 Jens Otten and   
               Christoph Kreitz   The ILTP Problem Library for
                                  Intuitionistic Logic . . . . . . . . . . 261--271

Journal of Automated Reasoning
Volume 38, Number 4, May, 2007

                  R. Gamboa and   
                      J. Cowles   Theory Extension in ACL2(r)  . . . . . . 273--301
               Marc Aiguier and   
                  Diane Bahrami   Structures for Abstract Rewriting  . . . 303--351
              Jeremy Avigad and   
                 Kevin Donnelly   A Decision Procedure for Linear ``Big
                                  O'' Equations  . . . . . . . . . . . . . 353--373


Journal of Automated Reasoning
Volume 39, Number 1, July, 2007

       Alberto Ciaffaglione and   
              Luigi Liquori and   
                 Marino Miculan   Reasoning about Object-based Calculi in
                                  (Co)Inductive Type Theory and the Theory
                                  of Contexts  . . . . . . . . . . . . . . 1--47
    Hans Kleine Büning and   
               K. Subramani and   
                    Xishun Zhao   Boolean Functions as Models for
                                  Quantified Boolean Formulas  . . . . . . 49--75
               Barbara Morawska   General $E$-unification with Eager
                                  Variable Elimination and a Nice Cycle
                                  Rule . . . . . . . . . . . . . . . . . . 77--106

Journal of Automated Reasoning
Volume 39, Number 2, August, 2007

             David Aspinall and   
            Christoph Lüth   Special Issue on User Interfaces in
                                  Theorem Proving: Preface . . . . . . . . 107--108
             Andrea Asperti and   
     Claudio Sacerdoti Coen and   
               Enrico Tassi and   
             Stefano Zacchiroli   User Interaction with the Matita Proof
                                  Assistant  . . . . . . . . . . . . . . . 109--139
                Paul Cairns and   
                     Jeremy Gow   Integrating Searching and Authoring in
                                  Mizar  . . . . . . . . . . . . . . . . . 141--160
                 Julien Narboux   A Graphical User Interface for Formal
                                  Proofs in Geometry . . . . . . . . . . . 161--180
        William Billingsley and   
                 Peter Robinson   Student Proof Exercises Using MathsTiles
                                  and Isabelle/HOL in an Intelligent Book  181--218
                   Carsten Sinz   Visualizing SAT Instances and Runs of
                                  the DPLL Algorithm . . . . . . . . . . . 219--243

Journal of Automated Reasoning
Volume 39, Number 3, October, 2007

                   Franz Baader   Preface to Special Issue on Reasoning in
                                  Description Logics . . . . . . . . . . . 245--247
               Ian Horrocks and   
                 Ulrike Sattler   A Tableau Decision Procedure for $
                                  \mathcal {SHOIQ} $ . . . . . . . . . . . 249--276
             Dmitry Tsarkov and   
               Ian Horrocks and   
       Peter F. Patel-Schneider   Optimizing Terminological Reasoning for
                                  Expressive Description Logics  . . . . . 277--316
           Stefan Schlobach and   
             Zhisheng Huang and   
              Ronald Cornet and   
             Frank van Harmelen   Debugging Incoherent Terminologies . . . 317--349
            Ullrich Hustadt and   
                Boris Motik and   
                 Ulrike Sattler   Reasoning in Description Logics by a
                                  Reduction to Disjunctive Datalog . . . . 351--384
            Diego Calvanese and   
        Giuseppe De Giacomo and   
             Domenico Lembo and   
         Maurizio Lenzerini and   
                Riccardo Rosati   Tractable Reasoning and Efficient Query
                                  Answering in Description Logics: The
                                  DL--Lite Family  . . . . . . . . . . . . 385--429

Journal of Automated Reasoning
Volume 39, Number 4, December, 2007

              Gem Stapleton and   
            Judith Masthoff and   
                Jean Flower and   
                Andrew Fish and   
                  Jane Southern   Automated Theorem Proving in Euler
                                  Diagram Systems  . . . . . . . . . . . . 431--470
              Julien Forest and   
                   Delia Kesner   Expression Reduction Systems with
                                  Patterns . . . . . . . . . . . . . . . . 513--541
           Daniel R. Brooks and   
                 Esra Erdem and   
         Selim T. Erdo\ugan and   
            James W. Minett and   
                      Don Ringe   Inferring Phylogenetic Trees Using
                                  Answer Set Programming . . . . . . . . . ??


Journal of Automated Reasoning
Volume 40, Number 1, January, 2008

           Mark H. Liffiton and   
              Karem A. Sakallah   Algorithms for Computing Minimal
                                  Unsatisfiable Subsets of Constraints . . 1--33
                   Jia Meng and   
            Lawrence C. Paulson   Translating Higher-Order Clauses to
                                  First-Order Clauses  . . . . . . . . . . 35--60
                 Marc Bezem and   
               Dimitri Hendriks   On the Mechanization of the Proof of
                                  Hessenberg's Theorem in Coherent Logic   61--85

Journal of Automated Reasoning
Volume 40, Number 2--3, March, 2008

                 Ulrich Furbach   IJCAR Preface  . . . . . . . . . . . . . 87--88
            Yevgeny Kazakov and   
                    Boris Motik   A Resolution-Based Decision Procedure
                                  for $ \boldsymbol \mathcal {SHOIQ} $ . . 89--116
                David Toman and   
                  Grant Weddell   On Keys and Functional Dependencies as
                                  First-Class Citizens in Description
                                  Logics . . . . . . . . . . . . . . . . . 117--132
          Kaustuv Chaudhuri and   
             Frank Pfenning and   
                     Greg Price   A Logical Characterization of Forward
                                  and Backward Chaining in the Inverse
                                  Method . . . . . . . . . . . . . . . . . 133--177
               Andrei Paskevich   Connection Tableaux with Lazy
                                  Paramodulation . . . . . . . . . . . . . 179--194
        Jörg Endrullis and   
          Johannes Waldmann and   
                   Hans Zantema   Matrix Interpretations for Proving
                                  Termination of Term Rewriting  . . . . . 195--220
               Volker Sorge and   
              Andreas Meier and   
              Roy McCasland and   
                   Simon Colton   Automatic Construction and Verification
                                  of Isotopy Invariants  . . . . . . . . . 221--243

Journal of Automated Reasoning
Volume 40, Number 4, May, 2008

                 Sandip Ray and   
       Warren A. Hunt, Jr.. and   
              John Matthews and   
              J. Strother Moore   A Mechanical Analysis of Program
                                  Verification Strategies  . . . . . . . . 245--269
       Jesús Aransay and   
           Clemens Ballarin and   
                    Julio Rubio   A Mechanized Proof of the Basic
                                  Perturbation Lemma . . . . . . . . . . . 271--292
               Bishop Brock and   
              Matt Kaufmann and   
              J. Strother Moore   Rewriting with Equivalence Relations in
                                  ACL2 . . . . . . . . . . . . . . . . . . 293--306
            Laurence Rideau and   
      Bernard Paul Serpette and   
                   Xavier Leroy   Tilting at Windmills with Coq: Formal
                                  Verification of a Compilation Algorithm
                                  for Parallel Moves . . . . . . . . . . . 307--326
                Christian Urban   Nominal Techniques in Isabelle/HOL . . . 327--356
            Yevgeny Kazakov and   
                    Boris Motik   A Resolution-Based Decision Procedure
                                  for $ \boldsymbol \mathcal {SHOIQ} $ . . 357--357


Journal of Automated Reasoning
Volume 41, Number 1, July, 2008

               Xavier Leroy and   
                 Sandrine Blazy   Formal Verification of a C-like Memory
                                  Model and Its Uses for Verifying Program
                                  Transformations  . . . . . . . . . . . . 1--31
            Magdalena Ortiz and   
            Diego Calvanese and   
                   Thomas Eiter   Data Complexity of Query Answering in
                                  Expressive Description Logics via
                                  Tableaux . . . . . . . . . . . . . . . . 61--98
               Amine Chaieb and   
                  Tobias Nipkow   Proof Synthesis and Reflection for
                                  Linear Arithmetic  . . . . . . . . . . . ??

Journal of Automated Reasoning
Volume 41, Number 2, August, 2008

            Volker Haarslev and   
               Ralf Möller   On the Scalability of Description Logic
                                  Instance Retrieval . . . . . . . . . . . 99--142
           André Platzer   Differential Dynamic Logic for Hybrid
                                  Systems  . . . . . . . . . . . . . . . . 143--189

Journal of Automated Reasoning
Volume 41, Number 3--4, November, 2008

             Serge Autexier and   
               Heiko Mantel and   
               Stephan Merz and   
                  Tobias Nipkow   Preface  . . . . . . . . . . . . . . . . 191--192
                    Hasan Amjad   Data Compression for Proof Replay  . . . 193--218
           Achim D. Brucker and   
                 Burkhart Wolff   An Extensible Encoding of
                                  Object-oriented Data Models in HOL . . . 219--249
                Osman Hasan and   
                Sofi\`ene Tahar   Using Theorem Proving to Verify
                                  Expectation and Variance for Discrete
                                  Random Variables . . . . . . . . . . . . 295--323
           Roberto Gorrieri and   
           Fabio Martinelli and   
            Marinella Petrocchi   Formal Models and Analysis of Secure
                                  Multicast in Wired and Wireless Networks 325--364
                Nick Moffat and   
              Michael Goldsmith   Assumption--Commitment Support for CSP
                                  Model Checking . . . . . . . . . . . . . 365--398
      Alastair F. Donaldson and   
                   Alice Miller   Automatic Symmetry Detection for Promela ??


Journal of Automated Reasoning
Volume 42, Number 1, January, 2009

                Osman Hasan and   
                Sofi\`ene Tahar   Performance Analysis and Functional
                                  Verification of the Stop-and-Wait
                                  Protocol in HOL  . . . . . . . . . . . . 1--33
                  C. A. Johnson   Computing Only Minimal Answers in
                                  Disjunctive Deductive Databases  . . . . 35--76
                Marko Samer and   
                 Stefan Szeider   Backdoor Sets of Quantified Boolean
                                  Formulas . . . . . . . . . . . . . . . . 77--97
              Magnus Björk   First Order Stålmarck . . . . . . . . . . 99--122

Journal of Automated Reasoning
Volume 42, Number 2--4, April, 2009

               Gerwin Klein and   
                 Ralf Huuck and   
                Bastian Schlich   Operating System Verification  . . . . . 123--124
                    Harvey Tuch   Formal Verification of C Systems Code    125--187
               Hendrik Tews and   
           Marcus Völp and   
                    Tjark Weber   Formal Memory Models for the
                                  Verification of Low-Level
                                  Operating-System Code  . . . . . . . . . 189--227
María del Mar Gallardo and   
               Pedro Merino and   
             David Sanán   Model Checking Dynamic Memory Allocation
                                  in Operating Systems . . . . . . . . . . 229--264
               Syrine Tlili and   
                 Mourad Debbabi   Interprocedural and Flow-Sensitive Type
                                  Analysis for Memory and Type Safety of C
                                  Code . . . . . . . . . . . . . . . . . . 265--300
                 Xinyu Feng and   
                 Zhong Shao and   
                     Yu Guo and   
                      Yuan Dong   Certifying Low-Level Programs with
                                  Hardware Interrupts and Preemptive
                                  Threads  . . . . . . . . . . . . . . . . 301--347
              Matthias Daum and   
 Jan Dörrenbächer and   
                 Burkhart Wolff   Proving Fairness and Implementation
                                  Correctness of a Microkernel Scheduler   349--388
              Eyad Alkassar and   
         Mark A. Hillebrand and   
         Dirk C. Leinenbach and   
        Norbert W. Schirmer and   
            Artem Starostin and   
               Alexandra Tsyban   Balancing the Load . . . . . . . . . . . 389--454


Journal of Automated Reasoning
Volume 43, Number 1, June, 2009

    Jasmin Christian Blanchette   Proof Pearl: Mechanizing the Textbook
                                  Proof of Huffman's Algorithm . . . . . . 1--18
   Jean-François Dufourd   An Intuitionistic Proof of a Discrete
                                  Form of the Jordan Curve Theorem
                                  Formalized in Coq with Combinatorial
                                  Hypermaps  . . . . . . . . . . . . . . . 19--51
         Raúl Monroy and   
                 Alan Bundy and   
                      Ian Green   On Process Equivalence = Equation
                                  Solving in CCS . . . . . . . . . . . . . 53--80
                  Filip Mari\'c   Formalization and Implementation of
                                  Modern SAT Solvers . . . . . . . . . . . 81--119

Journal of Automated Reasoning
Volume 43, Number 2, August, 2009

                   K. Subramani   Optimal Length Resolution Refutations of
                                  Difference Constraint Systems  . . . . . 121--137
                Ruben A. Gamboa   A Formalization of Powerlist Algebra in
                                  ACL2 . . . . . . . . . . . . . . . . . . 139--172
               Harald Zankl and   
               Nao Hirokawa and   
                Aart Middeldorp   KBO Orientability  . . . . . . . . . . . 173--201
                G. Dalzotto and   
                       T. Recio   On Protocols for the Automated Discovery
                                  of Theorems in Elementary Geometry . . . 203--236

Journal of Automated Reasoning
Volume 43, Number 3, October, 2009

            Richard Boulton and   
                   Joe Hurd and   
                   Konrad Slind   Computer Assisted Reasoning  . . . . . . 237--242
                  John Harrison   Formalizing an Analytic Proof of the
                                  Prime Number Theorem . . . . . . . . . . 243--261
             Sandrine Blazy and   
                   Xavier Leroy   Mechanized Semantics for the Clight
                                  Subset of the C Language . . . . . . . . 263--288
                  Tobias Nipkow   Social Choice Theory in HOL  . . . . . . 289--304
                Michael Norrish   Rewriting Conversions Implemented with
                                  Continuations  . . . . . . . . . . . . . 305--336

Journal of Automated Reasoning
Volume 43, Number 4, December, 2009

                   Xavier Leroy   A Formally Verified Compiler Back-end    ??
                Geoff Sutcliffe   The TPTP Problem Library and Associated
                                  Infrastructure . . . . . . . . . . . . . ??


Journal of Automated Reasoning
Volume 44, Number 1--2, February, 2010

          Sascha Böhme and   
             Micha\l Moskal and   
            Wolfram Schulte and   
                 Burkhart Wolff   HOL-Boogie --- An Interactive
                                  Prover-Backend for the Verifying C
                                  Compiler . . . . . . . . . . . . . . . . ??
            Jacques Carette and   
            Makarius Wenzel and   
                  Freek Wiedijk   Preface  . . . . . . . . . . . . . . . . ??
         Claudio Sacerdoti Coen   Declarative Representation of Proof
                                  Terms  . . . . . . . . . . . . . . . . . ??
           Dominik Dietrich and   
                 Ewaryst Schulz   Crystal: Integrating Structured Queries
                                  into a Tactic Language . . . . . . . . . ??
                Ferruccio Guidi   Procedural Representation of CIC Proof
                                  Terms  . . . . . . . . . . . . . . . . . ??
             Perry R. James and   
                 Patrice Chalin   Faster and More Complete Extended Static
                                  Checking for the Java Modeling Language  ??
            Predrag Jani\vci\'c   Geometry Constructions Language  . . . . ??

Journal of Automated Reasoning
Volume 44, Number 3, March, 2010

           Behzad Akbarpour and   
       Lawrence Charles Paulson   MetiTarski: An Automatic Theorem Prover
                                  for Real-Valued Special Functions  . . . 175--205
            Michael Mendler and   
                Stephan Scheele   Towards Constructive DL for Abstraction
                                  and Refinement . . . . . . . . . . . . . 207--243
                Olivier Hermant   Resolution is Cut-Free . . . . . . . . . 245--276
         Knot Pipatsrisawat and   
                 Adnan Darwiche   On Modern Clause-Learning Satisfiability
                                  Solvers  . . . . . . . . . . . . . . . . 277--301

Journal of Automated Reasoning
Volume 44, Number 4, April, 2010

               Alexander Krauss   Partial and Nested Recursive Function
                                  Definitions in Higher-order Logic  . . . 303--336
       Bernardo Cuenca Grau and   
 Christian Halaschek-Wiener and   
            Yevgeny Kazakov and   
     Boontawee Suntisrivaraporn   Incremental Classification of
                                  Description Logics Ontologies  . . . . . 337--369
              Mauro Ferrari and   
         Camillo Fiorentini and   
                  Guido Fiorino   $ \boldsymbol {\cal BC \! D \! L} $:
                                  Basic Constructive Description Logic . . 371--399
              Ruzica Piskac and   
          Leonardo de Moura and   
         Nikolaj Bjòrner   Deciding Effectively Propositional Logic
                                  Using DPLL and Substitution Sets . . . . 401--424


Journal of Automated Reasoning
Volume 45, Number 1, June, 2010

                 Yang Xiang and   
                    Kevin Grant   Preface: Special Issue on Uncertain
                                  Reasoning  . . . . . . . . . . . . . . . 1--2
     Gabriele Kern-Isberner and   
            Manuela Ritterskamp   Preference Fusion for Default Reasoning
                                  Beyond System Z  . . . . . . . . . . . . 3--19
  Miguel A. Palacios-Alonso and   
         Carlos A. Brizuela and   
               L. Enrique Sucar   Evolutionary Learning of Dynamic Naive
                                  Bayesian Classifiers . . . . . . . . . . 21--37
            Salem Benferhat and   
                  Safa Yahi and   
                   Habiba Drias   A New Default Theories Compilation for
                                  MSP--Entailment  . . . . . . . . . . . . 39--59
Frédéric Pichon and   
               Thierry Den\oeux   The Unnormalized Dempster's Rule of
                                  Combination: A New Justification from
                                  the Least Commitment Principle and Some
                                  Extensions . . . . . . . . . . . . . . . 61--87

Journal of Automated Reasoning
Volume 45, Number 2, August, 2010

         Alessandro Armando and   
          Peter Baumgartner and   
                   Gilles Dowek   Preface  . . . . . . . . . . . . . . . . 89--89
               Franz Baader and   
         Rafael Peñaloza   Automata-Based Axiom Pinpointing . . . . 91--129
               Marius Bozga and   
                 Radu Iosif and   
                 Swann Perarnau   Quantitative Separation Logic and
                                  Programs with Lists  . . . . . . . . . . 131--156
                Vivek Nigam and   
                    Dale Miller   A Framework for Proof Systems  . . . . . 157--188
                  Tobias Nipkow   Linear Quantifier Elimination  . . . . . 189--212

Journal of Automated Reasoning
Volume 45, Number 3, October, 2010

                   Zheng Ye and   
           Shang-Ching Chou and   
                  Xiao-Shan Gao   Visually Dynamic Presentation of Proofs
                                  in Plane Geometry  . . . . . . . . . . . 213--241
                   Zheng Ye and   
           Shang-Ching Chou and   
                  Xiao-Shan Gao   Visually Dynamic Presentation of Proofs
                                  in Plane Geometry  . . . . . . . . . . . 243--266
                   James Cheney   Equivariant Unification  . . . . . . . . 267--300
    André L. Galdino and   
   Mauricio Ayala-Rincón   A Formalization of the
                                  Knuth--Bendix(--Huet) Critical Pair
                                  Theorem  . . . . . . . . . . . . . . . . 301--325

Journal of Automated Reasoning
Volume 45, Number 4, December, 2010

           Bernhard Beckert and   
             Reiner Hähnle   Tests and Proofs . . . . . . . . . . . . 327--329
            Andrea Calvagna and   
              Angelo Gargantini   A Formal Logic Approach to Constrained
                                  Combinatorial Testing  . . . . . . . . . 331--358
              Andriy Dunets and   
         Gerhard Schellhorn and   
                  Wolfgang Reif   Automated Flaw Detection in Algebraic
                                  Specifications . . . . . . . . . . . . . 359--395
          Damiano Angeletti and   
         Enrico Giunchiglia and   
          Massimo Narizzano and   
           Alessandra Puddu and   
               Salvatore Sabina   Using Bounded Model Checking for
                                  Coverage Analysis of Safety-Critical
                                  Software in an Industrial Setting  . . . 397--414
          Lydie du Bousquet and   
                 Yves Ledru and   
              Olivier Maury and   
            Catherine Oriat and   
               Jean-Louis Lanet   Reusing a JML Specification Dedicated to
                                  Verification for Testing, and
                                  Vice-Versa: Case Studies . . . . . . . . 415--435
           Delphine Longuet and   
               Marc Aiguier and   
                Pascale Le Gall   Proof-Guided Test Selection from
                                  First-Order Specifications with Equality 437--473


Journal of Automated Reasoning
Volume 46, Number 1, January, 2011

              Carlos Areces and   
            Daniel Gorín   Resolution with Order and Selection for
                                  Hybrid Logics  . . . . . . . . . . . . . 1--42
             Szymon Klarman and   
               Ulle Endriss and   
               Stefan Schlobach   ABox Abduction in the Description Logic
                                  $ \boldsymbol \mathcal {ALC} $ . . . . . 43--80
             Javier Larrosa and   
         Robert Nieuwenhuis and   
            Albert Oliveras and   
Enric Rodríguez-Carbonell   A Framework for Certified Boolean
                                  Branch-and-Bound Optimization  . . . . . 81--102

Journal of Automated Reasoning
Volume 46, Number 2, February, 2011

           Ole J. Mengshoel and   
                   Dan Roth and   
               David C. Wilkins   Portfolios in Stochastic Local Search:
                                  Efficiently Computing Most Probable
                                  Explanations in Bayesian Networks  . . . 103--160
              Elvira Albert and   
                Puri Arenas and   
               Samir Genaim and   
           Germán Puebla   Closed-Form Upper Bounds in Static Cost
                                  Analysis . . . . . . . . . . . . . . . . 161--203
           Antonio Hernando and   
      Eugenio Roanes-Lozano and   
                  Luis M. Laita   A Polynomial Model for Logics with a
                                  Prime Power Number of Truth Values . . . 205--221

Journal of Automated Reasoning
Volume 46, Number 3--4, April, 2011

                 Lujo Bauer and   
              Sandro Etalle and   
           Jerry den Hartog and   
                  Luca Vigan\`o   Preface of Special Issue on ``Computer
                                  Security: Foundations and Automated
                                  Reasoning''  . . . . . . . . . . . . . . 223--224
   Véronique Cortier and   
               Steve Kremer and   
               Bogdan Warinschi   A Survey of Symbolic Methods in
                                  Computational Analysis of Cryptographic
                                  Systems  . . . . . . . . . . . . . . . . 225--259
                 J. Courant and   
              M. Daubignard and   
                     C. Ene and   
              P. Lafourcade and   
                    Y. Lakhnech   Automated Proofs for Asymmetric
                                  Encryption . . . . . . . . . . . . . . . 261--291
             Joana Martinho and   
          António Ravara   Encoding Cryptographic Primitives in a
                                  Calculus with Polyadic Synchronisation   293--323
          Ralf Küsters and   
               Tomasz Truderung   Reducing Protocol Analysis with XOR to
                                  the XOR--Free Case in the Horn Theory
                                  Based Approach . . . . . . . . . . . . . 325--352
                Wihem Arsac and   
            Giampaolo Bella and   
             Xavier Chantry and   
                  Luca Compagna   Multi-Attacker Protocol Validation . . . 353--388
               Max Kanovich and   
                  Paul Rowe and   
                  Andre Scedrov   Collaborative Planning with
                                  Confidentiality  . . . . . . . . . . . . 389--421


Journal of Automated Reasoning
Volume 47, Number 1, June, 2011

       Michael J. C. Gordon and   
              Matt Kaufmann and   
                     Sandip Ray   The Right Tools for the Job: Correctness
                                  of Cone of Influence Reduction Proved
                                  Using ACL2 and HOL4  . . . . . . . . . . 1--16
           John Thangarajah and   
                    Lin Padgham   Computationally Effective Reasoning
                                  About Goal Interactions  . . . . . . . . 17--56
      Louise Abigail Dennis and   
                  Ian Green and   
                    Alan Smaill   The Use of Embeddings to Provide a Clean
                                  Separation of Term and Annotation for
                                  Higher Order Rippling  . . . . . . . . . 57--105

Journal of Automated Reasoning
Volume 47, Number 2, August, 2011

          Renate A. Schmidt and   
               Brigitte Pientka   Preface: Special Issue of Selected
                                  Extended Papers of CADE-22 . . . . . . . 107--109
              Koen Claessen and   
           Ann Lillieström   Automated Inference of Finite
                                  Unsatisfiability . . . . . . . . . . . . 111--132
               Carsten Fuhs and   
          Jürgen Giesl and   
            Michael Parting and   
       Peter Schneider-Kamp and   
              Stephan Swiderski   Proving Termination by Dependency Pairs
                                  and Inductive Theorem Proving  . . . . . 133--160
       Maria Paola Bonacina and   
       Christopher A. Lynch and   
              Leonardo de Moura   On Deciding Satisfiability by Theorem
                                  Proving with Speculative Inferences  . . 161--189
          Peter Baumgartner and   
                   Uwe Waldmann   A Combined Superposition and Model
                                  Evolution Calculus . . . . . . . . . . . 191--227

Journal of Automated Reasoning
Volume 47, Number 3, October, 2011

Francisco Jesús Martín-Mateos and   
José Luis Ruiz-Reina and   
 José Antonio Alonso and   
María José Hidalgo   Proof Pearl: a Formal Proof of Higman's
                                  Lemma in ACL2  . . . . . . . . . . . . . 229--250
              Moa Johansson and   
                Lucas Dixon and   
                     Alan Bundy   Conjecture Synthesis for Inductive
                                  Theories . . . . . . . . . . . . . . . . 251--289
                   Amine Chaieb   Formal Power Series  . . . . . . . . . . 291--318
              Gianni Ciolli and   
           Graziano Gentili and   
                  Marco Maggesi   A Certified Proof of the Cartan Fixed
                                  Point Theorems . . . . . . . . . . . . . 319--336

Journal of Automated Reasoning
Volume 47, Number 4, December, 2011

          Jürgen Giesl and   
             Reiner Hähnle   Preface: Special Issue of Selected
                                  Extended Papers of IJCAR 2010  . . . . . 337--339
            Angelo Brillout and   
            Daniel Kroening and   
        Philipp Rümmer and   
                    Thomas Wahl   An Interpolating Sequent Calculus for
                                  Quantifier-Free Presburger Arithmetic    341--367
Jasmin Christian Blanchette and   
               Alexander Krauss   Monotonicity Inference for Higher-Order
                                  Formulas . . . . . . . . . . . . . . . . 369--398
                Hans de Nivelle   Classical Logic with Partial Functions   399--425
             Despoina Magka and   
            Yevgeny Kazakov and   
                   Ian Horrocks   Tractable Extensions of the Description
                                  Logic $ {\mathcal {EL}} $ with Numerical
                                  Datatypes  . . . . . . . . . . . . . . . 427--450
              Julian Backes and   
              Chad Edward Brown   Analytic Tableaux for Higher-Order Logic
                                  with Choice  . . . . . . . . . . . . . . 451--479
               Nao Hirokawa and   
                Aart Middeldorp   Decreasing Diagrams and Relative
                                  Termination  . . . . . . . . . . . . . . 481--501


Journal of Automated Reasoning
Volume 48, Number 1, January, 2012

          Daniele Zucchelli and   
                Enrica Nicolini   A Decidability Result for the Model
                                  Checking of Infinite-State Systems . . . 1--42
                  Amy Felty and   
             Alberto Momigliano   Hybrid . . . . . . . . . . . . . . . . . 43--105
       Cristina Borralleras and   
             Salvador Lucas and   
            Albert Oliveras and   
Enric Rodríguez-Carbonell and   
                   Albert Rubio   SAT Modulo Linear Arithmetic for Solving
                                  Polynomial Constraints . . . . . . . . . 107--131

Journal of Automated Reasoning
Volume 48, Number 2, February, 2012

         Hubert Comon-Lundh and   
              Catherine Meadows   Special Issue on Security and Rewriting
                                  Foreword . . . . . . . . . . . . . . . . 133--134
          Siva Anantharaman and   
                    Hai Lin and   
          Christopher Lynch and   
          Paliath Narendran and   
            Michael Rusinowitch   Unification Modulo Homomorphic
                                  Encryption . . . . . . . . . . . . . . . 135--158
              Joshua D. Guttman   State and Progress in Strand Spaces:
                                  Proving Fair Exchange  . . . . . . . . . 159--195
               Steve Kremer and   
            Antoine Mercier and   
                   Ralf Treinen   Reducing Equational Theories for the
                                  Decision of Static Equivalence . . . . . 197--217
   \cStefan Ciobâc\ua and   
   Stéphanie Delaune and   
                   Steve Kremer   Computing Knowledge in Security
                                  Protocols Under Convergent Equational
                                  Theories . . . . . . . . . . . . . . . . 219--262
          Yannick Chevalier and   
       Michaël Rusinowitch   Decidability of Equivalence of Symbolic
                                  Derivations  . . . . . . . . . . . . . . 263--292

Journal of Automated Reasoning
Volume 48, Number 3, March, 2012

             Mnacho Echenim and   
                Nicolas Peltier   An Instantiation Scheme for
                                  Satisfiability Modulo Theories . . . . . 293--362
                       Jan Otop   E-unification with Constants vs. General
                                  E-unification  . . . . . . . . . . . . . 363--390
         Bela\"\id Benhamou and   
               Lionel Paris and   
                  Pierre Siegel   Dealing with Satisfiability and $n$-ary
                                  CSPs in a Logical Framework  . . . . . . 391--417

Journal of Automated Reasoning
Volume 48, Number 4, April, 2012

              Freek Verbeek and   
                Julien Schmaltz   Proof Pearl: A Formal Proof of Dally and
                                  Seitz' Necessary and Sufficient
                                  Condition for Deadlock-Free Routing in
                                  Interconnection Networks . . . . . . . . 419--439
   Véronique Cortier and   
       Stéphanie Delaune   Decidability and Combination Results for
                                  Two Notions of Knowledge in Security
                                  Protocols  . . . . . . . . . . . . . . . 441--487
        Predrag Jani\vci\'c and   
             Julien Narboux and   
                 Pedro Quaresma   The Area Method  . . . . . . . . . . . . 489--532


Journal of Automated Reasoning
Volume 49, Number 1, June, 2012

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

Journal of Automated Reasoning
Volume 49, Number 2, August, 2012

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

Journal of Automated Reasoning
Volume 49, Number 3, October, 2012

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

Journal of Automated Reasoning
Volume 49, Number 4, December, 2012

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


Journal of Automated Reasoning
Volume 50, Number 1, January, 2013

           Jose Gaintzarain and   
           Montserrat Hermo and   
                Paqui Lucio and   
             Marisa Navarro and   
                Fernando Orejas   Invariant-Free Clausal Temporal
                                  Resolution . . . . . . . . . . . . . . . 1--49
              Miquel Bofill and   
                   Albert Rubio   Paramodulation with Non-Monotonic
                                  Orderings and Simplification . . . . . . 51--98
            James P. Bridge and   
       Lawrence Charles Paulson   Case Splitting in an Automatic Theorem
                                  Prover for Real-Valued Special Functions 99--117

Journal of Automated Reasoning
Volume 50, Number 2, February, 2013

           Andrzej Trybulec and   
          Artur Kornilowicz and   
             Adam Naumowicz and   
             Krystyna Kuperberg   Formal Mathematics for Mathematicians    119--121
                    Jesse Alama   Eliciting Implicit Assumptions of Mizar
                                  Proofs by Property Omission  . . . . . . 123--133
         Johan G. F. Belinfante   The GOEDEL Program . . . . . . . . . . . 135--146
      Marco Bright Caminati and   
              Giuseppe Rosolini   Custom Automations in Mizar  . . . . . . 147--160
                Yuichi Futa and   
           Hiroyuki Okazaki and   
               Yasunari Shidama   Formalization of Definitions and
                                  Theorems Related to an Elliptic Curve
                                  Over a Finite Prime Field by Using Mizar 161--172
                  John Harrison   The HOL Light Theory of Euclidean Space  173--190
               Mihnea Iancu and   
           Michael Kohlhase and   
               Florian Rabe and   
                    Josef Urban   The Mizar Mathematical Library in OMDoc:
                                  Translation and Applications . . . . . . 191--202
            Artur Korni\l owicz   On Rewriting Rules in Mizar  . . . . . . 203--210
                  Jan Mycielski   On the Formalization of Theories . . . . 211--216
                    Karol P\kak   Methods of Lemma Extraction in Natural
                                  Deduction Proofs . . . . . . . . . . . . 217--228
                Josef Urban and   
             Piotr Rudnicki and   
                Geoff Sutcliffe   ATP and Presentation Service for Mizar
                                  Formalizations . . . . . . . . . . . . . 229--241

Journal of Automated Reasoning
Volume 50, Number 3, March, 2013

              Clark Barrett and   
              Morgan Deters and   
          Leonardo de Moura and   
            Albert Oliveras and   
                    Aaron Stump   6 Years of SMT--COMP . . . . . . . . . . 243--277
               Nao Hirokawa and   
            Aart Middeldorp and   
                   Harald Zankl   Uncurrying for Termination and
                                  Complexity . . . . . . . . . . . . . . . 279--315
              Sarah Winkler and   
              Haruhiko Sato and   
            Aart Middeldorp and   
              Masahito Kurihara   Multi-Completion with Termination Tools  317--354

Journal of Automated Reasoning
Volume 50, Number 4, April, 2013

         Rajeev Goré and   
                Linh Anh Nguyen   ExpTime Tableaux for Using Sound Global
                                  Caching  . . . . . . . . . . . . . . . . 355--381
                David Sabel and   
   Manfred Schmidt-Schauß   A Two-Valued Logic for Properties of
                                  Strict Functional Programs Allowing
                                  Partial Functions  . . . . . . . . . . . 383--421
               Sylvie Boldo and   
François Clément and   
Jean-Christophe Filliâtre and   
             Micaela Mayero and   
        Guillaume Melquiond and   
                    Pierre Weis   Wave Equation Numerical Resolution: A
                                  Comprehensive Mechanized Proof of a C
                                  Program  . . . . . . . . . . . . . . . . 423--456


Journal of Automated Reasoning
Volume 51, Number 1, June, 2013

     Nikolaj Bjòrner and   
   Viorica Sofronie-Stokkermans   Preface: Special Issue of Selected
                                  Extended Papers of CADE-23 . . . . . . . 1--2
            Didier Galmiche and   
             Daniel Méry   A Connection-based Characterization of
                                  Bi-intuitionistic Validity . . . . . . . 3--26
            Lars Noschinski and   
               Fabian Emmes and   
              Jürgen Giesl   Analyzing Innermost Runtime Complexity
                                  of Term Rewriting by Dependency Pairs    27--56
                  Chad E. Brown   Reducing Higher-Order Theorem Proving to
                                  a Sequence of SAT Problems . . . . . . . 57--77
          Dejan Jovanovi\'c and   
              Leonardo de Moura   Cutting to the Chase . . . . . . . . . . 79--108
Jasmin Christian Blanchette and   
          Sascha Böhme and   
            Lawrence C. Paulson   Extending Sledgehammer with SMT Solvers  109--128

Journal of Automated Reasoning
Volume 51, Number 2, August, 2013

              Mauro Ferrari and   
         Camillo Fiorentini and   
                  Guido Fiorino   Contraction-Free Linear Depth Sequent
                                  Calculi for Intuitionistic Propositional
                                  Logic with the Subformula Property and
                                  Minimal Depth Counter-Models . . . . . . 129--149
  César Muñoz and   
              Anthony Narkawicz   Formalization of Bernstein Polynomials
                                  and Applications to Global Optimization  151--196
          Serenella Cerrito and   
            Marta Cialdea Mayer   A Tableau Based Decision Procedure for
                                  an Expressive Fragment of Hybrid Logic
                                  with Binders, Converse and Global
                                  Modalities . . . . . . . . . . . . . . . 197--239

Journal of Automated Reasoning
Volume 51, Number 3, October, 2013

                 Sandip Ray and   
                    Rob Sumners   Specification and Verification of
                                  Concurrent Programs Through Refinements  241--280
               Carles Creus and   
              Guillem Godoy and   
          Francesc Massanes and   
                  Ashish Tiwari   Non-Linear Rewrite Closure and Weak
                                  Normalization  . . . . . . . . . . . . . 281--324
          Christopher Lynch and   
             Quang-Trung Ta and   
                 Duc-Khanh Tran   SMELS: Satisfiability Modulo Equality
                                  with Lazy Superposition  . . . . . . . . 325--356

Journal of Automated Reasoning
Volume 51, Number 4, December, 2013

            Christian Sternagel   Proof Pearl--- A Mechanized Proof of
                                  GHC's Mergesort  . . . . . . . . . . . . 357--370
               Carles Creus and   
      Adri\`a Gascón and   
                  Guillem Godoy   Emptiness and Finiteness for Tree
                                  Automata with Global Reflexive
                                  Disequality Constraints  . . . . . . . . 371--400
              Matthias Baaz and   
                  Ori Lahav and   
                  Anna Zamansky   Finite-valued Semantics for Canonical
                                  Labelled Calculi . . . . . . . . . . . . 401--430
                 Alexei Lisitsa   Finite Reasons for Safety  . . . . . . . 431--451
                  Clark Barrett   Book Review: \booktitleDecision
                                  Procedures: An Algorithmic Point of
                                  View, by Daniel Kroening and Ofer
                                  Strichman, Springer--Verlag, 2008  . . . 453--456


Journal of Automated Reasoning
Volume 52, Number 1, January, 2014

          Eugenio G. Omodeo and   
           Alexandru I. Tomescu   Set Graphs. III. Proof Pearl: Claw-Free
                                  Graphs Mirrored into Transitive
                                  Hereditarily Finite Sets . . . . . . . . 1--29
             Matthew Gwynne and   
                Oliver Kullmann   Generalising Unit-Refutation
                                  Completeness and SLUR via Nested Input
                                  Resolution . . . . . . . . . . . . . . . 31--65
                  Guido Fiorino   Terminating Calculi for Propositional
                                  Dummett Logic with Subformula Property   67--97
           Marta R. Hidalgo and   
             Robert Joan-Arinyo   The Reachability Problem in Constructive
                                  Geometric Constraint Solving Based
                                  Dynamic Geometry . . . . . . . . . . . . 99--122

Journal of Automated Reasoning
Volume 52, Number 2, February, 2014

               Clemens Ballarin   Locales: A Module System for
                                  Mathematical Theories  . . . . . . . . . 123--153
               Temur Kutsia and   
                 Jordi Levy and   
                 Mateu Villaret   Anti-unification for Unranked Terms and
                                  Hedges . . . . . . . . . . . . . . . . . 155--190
                Jesse Alama and   
                 Tom Heskes and   
       Daniel Kühlwein and   
        Evgeni Tsivtsivadze and   
                    Josef Urban   Premise Selection for Mathematics by
                                  Corpus Analysis and Kernel Methods . . . 191--213
              Jonghyun Park and   
              Jeongbong Seo and   
               Sungwoo Park and   
                     Gyesik Lee   Mechanizing Metatheory Without Typing
                                  Contexts . . . . . . . . . . . . . . . . 215--239

Journal of Automated Reasoning
Volume 52, Number 3, March, 2014

              Eyad Alkassar and   
          Sascha Böhme and   
              Kurt Mehlhorn and   
            Christine Rizkallah   A Framework for the Verification of
                                  Certifying Computations  . . . . . . . . 241--273
           Alexander Malkis and   
               Anindya Banerjee   On Automation in the Verification of
                                  Software Barriers: Experience Report . . 275--329
      M. J. Hidalgo-Doblado and   
J. A. Alonso-Jiménez and   
     J. Borrego-Díaz and   
 F. J. Martín-Mateos and   
               J. L. Ruiz-Reina   Formally Verified Tableau-Based
                                  Reasoners for a Description Logic  . . . 331--360

Journal of Automated Reasoning
Volume 52, Number 4, April, 2014

              Mike Stannett and   
    István Németi   Using Isabelle/HOL to Verify First-Order
                                  Relativity Theory  . . . . . . . . . . . 361--378
                   Min Zhou and   
                     Fei He and   
               Bow-Yaw Wang and   
                    Ming Gu and   
                   Jiaguang Sun   Array Theory of Bounded Elements and its
                                  Applications . . . . . . . . . . . . . . 379--405
              Mark Kaminski and   
                    Gert Smolka   A Goal-Directed Decision Procedure for
                                  Hybrid PDL . . . . . . . . . . . . . . . 407--450
                 Chunhan Wu and   
             Xingyuan Zhang and   
                Christian Urban   A Formalisation of the Myhill--Nerode
                                  Theorem Based on Regular Expressions . . 451--480


Journal of Automated Reasoning
Volume 53, Number 1, June, 2014

            Yevgeny Kazakov and   
       Markus Krötzsch and   
  Franti\vsek Siman\vcík   The Incredible ELK . . . . . . . . . . . 1--61
            Reynald Affeldt and   
            Manabu Hagiwara and   
       Jonas Sénizergues   Formalization of Shannon's Theorems  . . 63--103

Journal of Automated Reasoning
Volume 53, Number 2, August, 2014

          Julianna Zsidó   Theorem of Three Circles in Coq  . . . . 105--127
              Stijn de Gouw and   
              Frank de Boer and   
                   Jurriaan Rot   Proof Pearl: The KeY to Correct and
                                  Stable Sorting . . . . . . . . . . . . . 129--139
            James P. Bridge and   
             Sean B. Holden and   
            Lawrence C. Paulson   Machine Learning for First-Order Theorem
                                  Proving  . . . . . . . . . . . . . . . . 141--172
            Cezary Kaliszyk and   
                    Josef Urban   Learning-Assisted Automated Reasoning
                                  with Flyspeck  . . . . . . . . . . . . . 173--213

Journal of Automated Reasoning
Volume 53, Number 3, October, 2014

                  Jiewen Wu and   
            Alexander Hudek and   
                David Toman and   
                  Grant Weddell   Absorption for ABoxes  . . . . . . . . . 215--243
                Birte Glimm and   
               Ian Horrocks and   
                Boris Motik and   
            Giorgos Stoilos and   
                       Zhe Wang   HermiT: An OWL 2 Reasoner  . . . . . . . 245--269
            Thomas Braibant and   
      Jacques-Henri Jourdan and   
                 David Monniaux   Implementing and Reasoning About
                                  Hash-consed Data Structures in Coq . . . 271--304
            Marta Cialdea Mayer   Extended Decision Procedure for a
                                  Fragment of HL with Binders  . . . . . . 305--315

Journal of Automated Reasoning
Volume 53, Number 4, December, 2014

             Hicham Bensaid and   
                Nicolas Peltier   A Complete Superposition Calculus for
                                  Primal Grammars  . . . . . . . . . . . . 317--350
        Andreas Steigmiller and   
                Birte Glimm and   
                Thorsten Liebig   Reasoning with Nominal Schemas through
                                  Absorption . . . . . . . . . . . . . . . 351--405
             Umair Siddique and   
                    Osman Hasan   On the Formalization of Gamma Function
                                  in HOL . . . . . . . . . . . . . . . . . 407--429


Journal of Automated Reasoning
Volume 54, Number 1, January, 2015

   Érik Martin-Dorel and   
           Guillaume Hanrot and   
             Micaela Mayero and   
           Laurent Théry   Formally Verified Certificate Checkers
                                  for Hardest-to-Round Computation . . . . 1--29
             Kamalesh Ghosh and   
            Pallab Dasgupta and   
                      S. Ramesh   Automated Planning as an Early
                                  Verification Tool for Distributed
                                  Control  . . . . . . . . . . . . . . . . 31--68
       Maria Paola Bonacina and   
                  Moa Johansson   On Interpolation in Automated Theorem
                                  Proving  . . . . . . . . . . . . . . . . 69--97
            Cezary Kaliszyk and   
                    Josef Urban   Erratum to: Learning-Assisted Automated
                                  Reasoning with Flyspeck  . . . . . . . . 99--99

Journal of Automated Reasoning
Volume 54, Number 2, February, 2015

               Harald Zankl and   
        Bertram Felgenhauer and   
                Aart Middeldorp   Labelings for Decreasing Diagrams  . . . 101--133
               Sylvie Boldo and   
      Jacques-Henri Jourdan and   
               Xavier Leroy and   
            Guillaume Melquiond   Verified Compilation of Floating-Point
                                  Computations . . . . . . . . . . . . . . 135--163
               Simon Foster and   
                   Georg Struth   On the Fine-Structure of Regular Algebra 165--197

Journal of Automated Reasoning
Volume 54, Number 3, March, 2015

              Bernhard Reus and   
         Nathaniel Charlton and   
                   Ben Horsfall   Symbolic Execution Proofs for Higher
                                  Order Store Programs . . . . . . . . . . 199--284

Journal of Automated Reasoning
Volume 54, Number 4, April, 2015

          Anthony Narkawicz and   
  César Muñoz and   
                    Aaron Dutle   Formally-Verified Decision Procedures
                                  for Univariate Polynomial Computation
                                  Based on Sturm's and Tarski's Theorems   285--326
          Francesco Alberti and   
            Silvio Ghilardi and   
              Natasha Sharygina   Decision Procedures for Flat Array
                                  Properties . . . . . . . . . . . . . . . 327--352
       Maria Paola Bonacina and   
                  Moa Johansson   Interpolation Systems for Ground Proofs
                                  in Automated Deduction: a Survey . . . . 353--390


Journal of Automated Reasoning
Volume 55, Number 1, June, 2015

            Lawrence C. Paulson   A Mechanised Proof of Gödel's
                                  Incompleteness Theorems Using Nominal
                                  Isabelle . . . . . . . . . . . . . . . . 1--37
           Francisco Botana and   
         Markus Hohenwarter and   
        Predrag Jani\vci\'c and   
Zoltán Kovács and   
            Ivan Petrovi\'c and   
         Tomás Recio and   
               Simon Weitzhofer   Automated Theorem Proving in GeoGebra:
                                  Current Achievements . . . . . . . . . . 39--59
               David R. Cok and   
                Aaron Stump and   
                    Tjark Weber   The 2013 Evaluation of SMT--COMP and
                                  SMT--LIB . . . . . . . . . . . . . . . . 61--90

Journal of Automated Reasoning
Volume 55, Number 2, August, 2015

       Daniel Kühlwein and   
                    Josef Urban   MaLeS: A Framework for Automatic Tuning
                                  of Automated Theorem Provers . . . . . . 91--116
                Jared Davis and   
               Magnus O. Myreen   The Reflective Milawa Theorem Prover is
                                  Sound (Down to the Machine Code that
                                  Runs it) . . . . . . . . . . . . . . . . 117--183
            Marta Cialdea Mayer   Erratum to: ``Extension of a Decision
                                  Procedure for a Fragment of Hybrid Logic
                                  with Binders'' . . . . . . . . . . . . . 185--185

Journal of Automated Reasoning
Volume 55, Number 3, October, 2015

    Krystyna Trybulec Kuperberg   Andrzej Trybulec --- in Memoriam . . . . 187--190
             Adam Grabowski and   
        Artur Korni\l owicz and   
                 Adam Naumowicz   Four Decades of Mizar  . . . . . . . . . 191--198
                  Chad E. Brown   Reconsidering Pairs and Functions as
                                  Sets . . . . . . . . . . . . . . . . . . 199--210
                 Adam Grabowski   Mechanizing Complemented Lattices Within
                                  Mizar Type System  . . . . . . . . . . . 211--221
                  John Harrison   Formal Proofs of Hypergeometric Sums . . 223--243
            Cezary Kaliszyk and   
                    Josef Urban   MizAR 40 for Mizar 40  . . . . . . . . . 245--256
            Artur Korni\l owicz   Definitional Expansions in Mizar . . . . 257--268
            Alexander Lyaletski   Evidence Algorithm and Inference Search
                                  in First-Order Logics  . . . . . . . . . 269--284
                 Adam Naumowicz   Automating Boolean Set Operations in
                                  Mizar Proof Checking with the Aid of an
                                  External SAT Solver  . . . . . . . . . . 285--294
                    Karol P\kak   Improving Legibility of Formal Proofs
                                  Based on the Close Reference Principle
                                  is NP--Hard  . . . . . . . . . . . . . . 295--306

Journal of Automated Reasoning
Volume 55, Number 4, December, 2015

               Amy P. Felty and   
         Alberto Momigliano and   
               Brigitte Pientka   The Next 700 Challenge Problems for
                                  Reasoning with Higher-Order Abstract
                                  Syntax Representations . . . . . . . . . 307--372
                 Andrea Asperti   Reverse Complexity . . . . . . . . . . . 373--388
  Christoph Benzmüller and   
                Nik Sultana and   
        Lawrence C. Paulson and   
              Frank Theiß   The Higher-Order Prover Leo-II . . . . . 389--404


Journal of Automated Reasoning
Volume 56, Number 1, January, 2016

            Jesper Bengtson and   
             Joachim Parrow and   
                    Tjark Weber   Psi-Calculi in Isabelle  . . . . . . . . 1--47
        Martin Gagné and   
          Pascal Lafourcade and   
           Yassine Lakhnech and   
          Reihaneh Safavi-Naini   Automated Proofs of Block Cipher Modes
                                  of Operation . . . . . . . . . . . . . . 49--94

Journal of Automated Reasoning
Volume 56, Number 2, February, 2016

          Peter Baumgartner and   
             Wolfgang Bibel and   
              Richard Waldinger   In Memory of Mark Stickel  . . . . . . . 95--98
             Donald W. Loveland   Mark Stickel: His Earliest Work  . . . . 99--112
       Maria Paola Bonacina and   
              David A. Plaisted   Semantically-Guided Goal-Sensitive
                                  Reasoning: Model Representation  . . . . 113--141
                   Hantao Zhang   An Experiment with Satisfiability Modulo
                                  SAT  . . . . . . . . . . . . . . . . . . 143--154
Jasmin Christian Blanchette and   
          Sascha Böhme and   
             Mathias Fleury and   
       Steffen Juilf Smolka and   
            Albert Steckermeier   Semi-intelligible Isar Proofs from
                                  Machine-Generated Proofs . . . . . . . . 155--200

Journal of Automated Reasoning
Volume 56, Number 3, March, 2016

               Gerwin Klein and   
                   Ruben Gamboa   Interactive Theorem Proving  . . . . . . 201--203
                     Rob Arthan   On Definitions of Constants and Types in
                                  HOL  . . . . . . . . . . . . . . . . . . 205--219
               Ramana Kumar and   
                 Rob Arthan and   
           Magnus O. Myreen and   
                    Scott Owens   Self-Formalisation of Higher-Order Logic 221--259
            Daniel Matichuk and   
                Toby Murray and   
                Makarius Wenzel   Eisbach: A Proof Method Language for
                                  Isabelle . . . . . . . . . . . . . . . . 261--282
             Sandrine Blazy and   
            Vincent Laporte and   
                David Pichardie   Verified Abstract Interpretation
                                  Techniques for Disassembling Low-level
                                  Self-modifying Code  . . . . . . . . . . 283--308
             Timothy Bourke and   
     Robert J. van Glabbeek and   
              Peter Höfner   Mechanizing a Process Algebra for
                                  Network Protocols  . . . . . . . . . . . 309--341
          Christian Doczkal and   
                    Gert Smolka   Completeness and Decidability Results
                                  for CTL in Constructive Type Theory  . . 343--365
              Jeremy Avigad and   
            Robert Y. Lewis and   
                      Cody Roux   A Heuristic Prover for Real Inequalities 367--386

Journal of Automated Reasoning
Volume 56, Number 4, April, 2016

               Claire Dross and   
            Sylvain Conchon and   
             Johannes Kanig and   
               Andrei Paskevich   Adding Decision Procedures to SMT
                                  Solvers Using Axioms with Triggers . . . 387--457
        Friedrich Slivovsky and   
                 Stefan Szeider   Quantifier Reordering for QBF  . . . . . 459--477


Journal of Automated Reasoning
Volume 57, Number 1, June, 2016

            Daniel Kroening and   
             Andrey Rybalchenko   Preface: Special Issue on Interpolation  1--2
        Matthias Schlaipfer and   
            Georg Weissenbacher   Labelled Interpolation Systems for
                                  Hyper-Resolution, Clausal, and Local
                                  Proofs . . . . . . . . . . . . . . . . . 3--36
              Nishant Totla and   
                    Thomas Wies   Complete Instantiation-Based
                                  Interpolation  . . . . . . . . . . . . . 37--65
         Jürgen Christ and   
                Jochen Hoenicke   Proof Tree Preserving Tree Interpolation 67--95

Journal of Automated Reasoning
Volume 57, Number 2, August, 2016

                 M. Echenim and   
                     N. Peltier   A Superposition Calculus for Abductive
                                  Reasoning  . . . . . . . . . . . . . . . 97--134
                    Pierre Roux   Formal Proofs of Rounding Error Bounds:
                                  With Application to an Automatic
                                  Positive Definiteness Check  . . . . . . 135--156
               Peter Franek and   
            Stefan Ratschan and   
              Piotr Zgliczynski   Quasi-decidability of a Fragment of the
                                  First-Order Theory of Real Numbers . . . 157--185

Journal of Automated Reasoning
Volume 57, Number 3, October, 2016

   Érik Martin-Dorel and   
            Guillaume Melquiond   Proving Tight Bounds on Univariate
                                  Expressions with Elementary Functions in
                                  Coq  . . . . . . . . . . . . . . . . . . 187--217
Jasmin Christian Blanchette and   
            David Greenaway and   
            Cezary Kaliszyk and   
       Daniel Kühlwein and   
                    Josef Urban   A Learning-Based Fact Selector for
                                  Isabelle/HOL . . . . . . . . . . . . . . 219--244
     Thierry Boy de la Tour and   
                Nicolas Peltier   Proof Generalization in LK by Second
                                  Order Unifier Minimization . . . . . . . 245--280

Journal of Automated Reasoning
Volume 57, Number 4, December, 2016

             Tuan-Hung Pham and   
               Andrew Gacek and   
              Michael W. Whalen   Reasoning About Algebraic Data Types
                                  with Abstractions  . . . . . . . . . . . 281--318
               Robbert Krebbers   A Formal C Memory Model for Separation
                                  Logic  . . . . . . . . . . . . . . . . . 319--387


Journal of Automated Reasoning
Volume 58, Number 1, January, 2017

      Stéphane Demri and   
               Deepak Kapur and   
           Christoph Weidenbach   Preface  . . . . . . . . . . . . . . . . 1--2
          Jürgen Giesl and   
       Cornelius Aschermann and   
          Marc Brockschmidt and   
               Fabian Emmes and   
              Florian Frohn and   
               Carsten Fuhs and   
                Jera Hensel and   
               Carsten Otto and   
        Martin Plücker and   
       Peter Schneider-Kamp and   
        Thomas Ströder and   
        Stephanie Swiderski and   
           René Thiemann   Analyzing Program Termination and
                                  Complexity Automatically with AProVE . . 3--31
        Thomas Ströder and   
          Jürgen Giesl and   
          Marc Brockschmidt and   
              Florian Frohn and   
               Carsten Fuhs and   
                Jera Hensel and   
       Peter Schneider-Kamp and   
           Cornelius Aschermann   Automatically Proving Termination and
                                  Memory Safety for Programs with Pointer
                                  Arithmetic . . . . . . . . . . . . . . . 33--65
    \.Ismail \.Ilkan Ceylan and   
         Rafael Peñaloza   The Bayesian Ontology Language $
                                  \mathcal {BEL} $ . . . . . . . . . . . . 67--95
         Marijn J. H. Heule and   
              Martina Seidl and   
                    Armin Biere   Solution Validation and Extraction for
                                  QBF Preprocessing  . . . . . . . . . . . 97--125
        Aleksandar Zelji\'c and   
 Christoph M. Wintersteiger and   
            Philipp Rümmer   An Approximation Framework for Solvers
                                  and Decision Procedures  . . . . . . . . 127--147
Jasmin Christian Blanchette and   
             Andrei Popescu and   
                Dmitriy Traytel   Soundness and Completeness Proofs by
                                  Coinductive Methods  . . . . . . . . . . 149--179
             Michael Beeson and   
                      Larry Wos   Finding Proofs in Tarskian Geometry  . . 181--207

Journal of Automated Reasoning
Volume 58, Number 2, February, 2017

              Gabriel Braun and   
                 Julien Narboux   A Synthetic Proof of Pappus' Theorem in
                                  Tarski's Geometry  . . . . . . . . . . . 209--230
Ana Cristina Rocha-Oliveira and   
  André Luiz Galdino and   
   Mauricio Ayala-Rincón   Confluence of Orthogonal Term Rewriting
                                  Systems in the Prototype Verification
                                  System . . . . . . . . . . . . . . . . . 231--251
            M. Ganesalingam and   
                   W. T. Gowers   A Fully Automatic Theorem Prover with
                                  Human-Style Output . . . . . . . . . . . 253--291
      Alexander Baumgartner and   
               Temur Kutsia and   
                 Jordi Levy and   
                 Mateu Villaret   Higher-Order Pattern Anti-Unification in
                                  Linear Time  . . . . . . . . . . . . . . 293--310

Journal of Automated Reasoning
Volume 58, Number 3, March, 2017

                  Amy Felty and   
                Aart Middeldorp   Preface: Selected Extended Papers of
                                  CADE 2015  . . . . . . . . . . . . . . . 311--312
            Edward Zulkoski and   
              Curtis Bright and   
              Albert Heinle and   
            Ilias Kotsireas and   
        Krzysztof Czarnecki and   
                   Vijay Ganesh   Combining SAT Solvers with Computer
                                  Algebra Systems to Verify Combinatorial
                                  Conjectures  . . . . . . . . . . . . . . 313--339
            Andrew Reynolds and   
    Jasmin Christian Blanchette   A Decision Procedure for (Co)datatypes
                                  in SMT Solvers . . . . . . . . . . . . . 341--362
              Vijay D'Silva and   
                 Caterina Urban   Abstract Interpretation as Automated
                                  Deduction  . . . . . . . . . . . . . . . 363--390
         José Iborra and   
              Naoki Nishida and   
        Germán Vidal and   
                 Akihisa Yamada   Relative Termination via Dependency
                                  Pairs  . . . . . . . . . . . . . . . . . 391--411

Journal of Automated Reasoning
Volume 58, Number 4, April, 2017

         Jean-Marie Lagniez and   
                 Pierre Marquis   On Preprocessing Techniques and Their
                                  Impact on Propositional Model Counting   413--481
                   Manuel Eberl   Proving Divide and Conquer Complexities
                                  in Isabelle/HOL  . . . . . . . . . . . . 483--508
       Jesús Aransay and   
            Jose Divasón   A Formalisation in HOL of the
                                  Fundamental Theorem of Linear Algebra
                                  and Its Application to the Solution of
                                  the Least Squares Problem  . . . . . . . 509--535


Journal of Automated Reasoning
Volume 59, Number 1, June, 2017

          Jürgen Giesl and   
                   Jan Hoffmann   Preface: Special Issue on Automatic
                                  Resource Bound Analysis  . . . . . . . . 1--2
                Moritz Sinn and   
            Florian Zuleger and   
                   Helmut Veith   Complexity and Resource Bound Analysis
                                  of Imperative Programs Using Difference
                                  Constraints  . . . . . . . . . . . . . . 3--45
              Elvira Albert and   
     Antonio Flores-Montoya and   
               Samir Genaim and   
          Enrique Martin-Martin   Rely-Guarantee Termination and Cost
                                  Analyses of Loops with Concurrent
                                  Interleavings  . . . . . . . . . . . . . 47--85
               Steffen Jost and   
          Pedro Vasconcelos and   
       Mário Florido and   
                  Kevin Hammond   Type-Based Cost Analysis for Lazy
                                  Functional Languages . . . . . . . . . . 87--120
              Florian Frohn and   
          Jürgen Giesl and   
                Jera Hensel and   
       Cornelius Aschermann and   
            Thomas Ströder   Lower Bounds for Runtime Complexity of
                                  Term Rewriting . . . . . . . . . . . . . 121--163

Journal of Automated Reasoning
Volume 59, Number 2, August, 2017

       Maria Paola Bonacina and   
              David A. Plaisted   Semantically-Guided Goal-Sensitive
                                  Reasoning: Inference System and
                                  Completeness . . . . . . . . . . . . . . 165--218
           André Platzer   A Complete Uniform Substitution Calculus
                                  for Differential Dynamic Logic . . . . . 219--265
          Christoph Walther and   
                  Nathan Wasser   Fermat, Euler, Wilson --- Three Case
                                  Studies in Number Theory . . . . . . . . 267--286

Journal of Automated Reasoning
Volume 59, Number 3, October, 2017

            Zakaria Chihani and   
                Dale Miller and   
                  Fabien Renaud   A Semantic Framework for Proof Evidence  287--330
                   Jie Zhou and   
              Dingkang Wang and   
                        Yao Sun   Automated Reducible Geometric Theorem
                                  Proving and Discovery by Gröbner Basis
                                  Method . . . . . . . . . . . . . . . . . 331--344
            Johannes Hölzl   Markov Chains and Markov Decision
                                  Processes in Isabelle/HOL  . . . . . . . 345--387

Journal of Automated Reasoning
Volume 59, Number 4, December, 2017

              Jeremy Avigad and   
        Johannes Hölzl and   
                   Luke Serafin   A Formally Verified Proof of the Central
                                  Limit Theorem  . . . . . . . . . . . . . 389--423
    Luís Cruz-Filipe and   
              Kim S. Larsen and   
           Peter Schneider-Kamp   Formally Proving Size Optimality of
                                  Sorting Networks . . . . . . . . . . . . 425--454
               Bijan Parsia and   
        Nicolas Matentzoglu and   
 Rafael S. Gonçalves and   
                Birte Glimm and   
            Andreas Steigmiller   The OWL Reasoner Evaluation (ORE) 2015
                                  Competition Report . . . . . . . . . . . 455--482
                Geoff Sutcliffe   The TPTP Problem Library and Associated
                                  Infrastructure . . . . . . . . . . . . . 483--502


Journal of Automated Reasoning
Volume 60, Number 1, January, 2018

César A. Muñoz and   
          Sanjai Rayadurgam and   
                 Oksana Tkachuk   Selected Extended Papers of NFM 2016:
                                  Preface  . . . . . . . . . . . . . . . . 1--2
             Julian Brunner and   
                  Peter Lammich   Formal Verification of an Executable LTL
                                  Model Checker with Partial Order
                                  Reduction  . . . . . . . . . . . . . . . 3--21
                  Shaobo He and   
         Shuvendu K. Lahiri and   
           Zvonimir Rakamari\'c   Verifying Relative Safety, Accuracy, and
                                  Termination for Program Approximations   23--42
                 Susmit Jha and   
            Vasumathi Raman and   
               Dorsa Sadigh and   
               Sanjit A. Seshia   Safe Autonomy Under Perception
                                  Uncertainty Using Chance-Constrained
                                  Temporal Logic . . . . . . . . . . . . . 43--62
                Josh Newell and   
                 Linna Pang and   
             David Tremaine and   
               Alan Wassyng and   
                   Mark Lawford   Translation of IEC 61131-3 Function
                                  Block Diagrams to PVS for Formal
                                  Verification with Real-Time Nuclear
                                  Application  . . . . . . . . . . . . . . 63--84
      Muhammad Usama Sardar and   
                  Nida Afaq and   
                Osman Hasan and   
            Khaza Anuarul Hoque   Towards Probabilistic Formal Analysis of
                                  SATS--Simultaneously Moving Aircraft
                                  (SATS--SMA)  . . . . . . . . . . . . . . 85--105
                 Yi-Chin Wu and   
            Vasumathi Raman and   
          Blake C. Rawlings and   
  Stéphane Lafortune and   
               Sanjit A. Seshia   Synthesis of Obfuscation Policies to
                                  Ensure Privacy and Utility . . . . . . . 107--131

Journal of Automated Reasoning
Volume 60, Number 2, February, 2018

                John Slaney and   
       Bruno Woltzenlogel Paleo   Conflict Resolution: A First-Order
                                  Resolution Calculus with Decision
                                  Literals and Conflict-Driven Clause
                                  Learning . . . . . . . . . . . . . . . . 133--156
           Zoltan A. Kocsis and   
                     Jerry Swan   Genetic Programming $ \varvec {+} $
                                  Proof Search $ \varvec { = } $ Automatic
                                  Improvement  . . . . . . . . . . . . . . 157--176
             Laura Bozzelli and   
    César Sánchez   Visibly Linear Temporal Logic  . . . . . 177--220
               Filipe Casal and   
              João Rasga   Many-Sorted Equivalence of Shiny and
                                  Strongly Polite Theories . . . . . . . . 221--236
                  Marco Maggesi   A Formalization of Metric Spaces in HOL
                                  Light  . . . . . . . . . . . . . . . . . 237--254

Journal of Automated Reasoning
Volume 60, Number 3, March, 2018

             Sandrine Blazy and   
                 Marsha Chechik   Selected Extended Papers of VSTTE 2016   255--256
                   Gang Tan and   
                 Greg Morrisett   Bidirectional Grammars for Machine-Code
                                  Decoding and Encoding  . . . . . . . . . 257--277
             Kensuke Kojima and   
           Akifumi Imanishi and   
               Atsushi Igarashi   Automated Verification of Functional
                                  Correctness of Race-Free GPU Programs    279--298
                 Dirk Beyer and   
             Matthias Dangl and   
                Philipp Wendler   A Unifying View on SMT-Based Software
                                  Verification . . . . . . . . . . . . . . 299--335
              Moritz Kiefer and   
          Vladimir Klebanov and   
                Mattias Ulbrich   Relational Program Reasoning Using
                                  Compiler IR  . . . . . . . . . . . . . . 337--363
            Martin Clochard and   
      Léon Gondelman and   
           Mário Pereira   The Matrix Reproved (Verification Pearl) 365--383

Journal of Automated Reasoning
Volume 60, Number 4, April, 2018

        Nicolas Matentzoglu and   
               Bijan Parsia and   
                    Uli Sattler   OWL Reasoning: Subsumption Test Hardness
                                  and Modularity . . . . . . . . . . . . . 385--419
               Luis Aguirre and   
 Narciso Martí-Oliet and   
            Miguel Palomino and   
                    Isabel Pita   Sentence-Normalized Conditional
                                  Narrowing Modulo in Rewriting Logic and
                                  Maude  . . . . . . . . . . . . . . . . . 421--463
             Salvador Lucas and   
   Raúl Gutiérrez   Automatic Synthesis of Logical Models
                                  for Order-Sorted First-Order Theories    465--501
                Eric Braude and   
              Satbek Abdyldayev   Generalizing Morley's and Other Theorems
                                  with Automated Realization . . . . . . . 503--526
                John Slaney and   
       Bruno Woltzenlogel Paleo   Erratum to: Conflict Resolution: A
                                  First-Order Resolution Calculus with
                                  Decision Literals and Conflict-Driven
                                  Clause Learning  . . . . . . . . . . . . 527--527


Journal of Automated Reasoning
Volume 61, Number 1--4, June, 2018

              Jeremy Avigad and   
Jasmin Christian Blanchette and   
               Gerwin Klein and   
           Lawrence Paulson and   
             Andrei Popescu and   
                Gregor Snelting   Introduction to Milestones in
                                  Interactive Theorem Proving  . . . . . . 1--8
          Grzegorz Bancerek and   
        Czes\law Byli\'nski and   
             Adam Grabowski and   
         Artur Korni\lowicz and   
          Roman Matuszewski and   
             Adam Naumowicz and   
                    Karol P\kak   The Role of the Mizar Mathematical
                                  Library for Interactive Proof
                                  Development in Mizar . . . . . . . . . . 9--32
                Yves Bertot and   
            Laurence Rideau and   
           Laurent Théry   Distant Decimals of $ \pi $: Formal
                                  Proofs of Some Algorithms Computing Them
                                  and Guarantees of Exact Computation  . . 33--71
                  Fabian Immler   A Verified ODE Solver and the Lorenz
                                  Attractor  . . . . . . . . . . . . . . . 73--111
      Thomas Bauereiß and   
     Armando Pesenti Gritti and   
             Andrei Popescu and   
                Franco Raimondi   CoSMed: A Confidentiality-Verified
                                  Social Media Platform  . . . . . . . . . 113--139
                   Hao Chen and   
                Xiongnan Wu and   
                 Zhong Shao and   
           Joshua Lockerman and   
                     Ronghui Gu   Toward Compositional Verification of
                                  Interruptible OS Kernels and Device
                                  Drivers  . . . . . . . . . . . . . . . . 141--189
         Cornelius Diekmann and   
                 Lars Hupel and   
           Julius Michaelis and   
        Maximilian Haslbeck and   
                    Georg Carle   Verified iptables Firewall Analysis and
                                  Verification . . . . . . . . . . . . . . 191--242
             Andreas Lochbihler   Mechanising a Type-Safe Model of
                                  Multithreaded Java with a Verified
                                  Compiler . . . . . . . . . . . . . . . . 243--332
Jasmin Christian Blanchette and   
             Mathias Fleury and   
              Peter Lammich and   
           Christoph Weidenbach   A Verified SAT Solver Framework with
                                  Learn, Forget, Restart, and
                                  Incrementality . . . . . . . . . . . . . 333--365
               Qinxiang Cao and   
           Lennart Beringer and   
            Samuel Gruetter and   
               Josiah Dodds and   
                Andrew W. Appel   VST-Floyd: A Separation Logic Tool to
                                  Verify Correctness of C Programs . . . . 367--422
             \Lukasz Czajka and   
                Cezary Kaliszyk   Hammer for Coq: Automation for Dependent
                                  Type Theory  . . . . . . . . . . . . . . 423--453
           Anders Schlichtkrull   Formalization of the Resolution Calculus
                                  for First-Order Logic  . . . . . . . . . 455--484
         Mohammad Abdulaziz and   
            Michael Norrish and   
                Charles Gretton   Formally Verified Algorithms for
                                  Upper-Bounding State Space Diameters . . 485--520
          Christian Doczkal and   
                    Gert Smolka   Regular Language Representations in the
                                  Constructive Type Theory of Coq  . . . . 521--553


Journal of Automated Reasoning
Volume 62, Number 1, January, 2019

              Pierre Boutry and   
               Charly Gries and   
             Julien Narboux and   
                 Pascal Schreck   Parallel Postulates and Continuity
                                  Axioms: A Mechanized Study in
                                  Intuitionistic Logic Using Coq . . . . . 1--68
                   Wenda Li and   
       Grant Olney Passmore and   
            Lawrence C. Paulson   Deciding Univariate Polynomial Problems
                                  Using Untrusted Certificates in
                                  Isabelle\slash HOL . . . . . . . . . . . 69--91
              Stijn de Gouw and   
           Frank S. de Boer and   
                  Richard Bubel   Verifying OpenJDK's Sort Method for
                                  Generic Collections  . . . . . . . . . . 93--126
              Mauro Ferrari and   
             Camillo Fiorentini   Goal-Oriented Proof-Search in Natural
                                  Deduction for Intuitionistic
                                  Propositional Logic  . . . . . . . . . . 127--167

Journal of Automated Reasoning
Volume 62, Number 2, February, 2019

Jasmin Christian Blanchette and   
                   Stephan Merz   Selected Extended Papers of ITP 2016:
                                  Preface  . . . . . . . . . . . . . . . . 169--170
              Hing-Lun Chan and   
                Michael Norrish   Proof Pearl: Bounding Least Common
                                  Multiples with Triangles . . . . . . . . 171--192
     Thomas Grégoire and   
                  Adam Chlipala   Mostly Automated Formal Verification of
                                  Loop Dependencies with Applications to
                                  Distributed Stencil Algorithms . . . . . 193--213
              Fabian Immler and   
                Christoph Traut   The Flow of ODEs: Formalization of
                                  Variational Equation and Poincaré Map . . 215--236
          Ond\vrej Kun\vcar and   
                 Andrei Popescu   From Types to Sets by Local Type
                                  Definition in Higher-Order Logic . . . . 237--260
              Peter Lammich and   
               S. Reza Sefidgar   Formalizing Network Flow Algorithms: a
                                  Refinement Approach in Isabelle/HOL  . . 261--280
             Assia Mahboubi and   
        Guillaume Melquiond and   
            Thomas Sibut-Pinote   Formally Verified Approximations of
                                  Definite Integrals . . . . . . . . . . . 281--300

Journal of Automated Reasoning
Volume 62, Number 3, March, 2019

                  Filip Mari\'c   Fast Formal Proof of the
                                  Erd\Hos--Szekeres Conjecture for Convex
                                  Polygons with at Most $6$ Points . . . . 301--329
  Arthur Charguéraud and   
        François Pottier   Verifying the Correctness and Amortized
                                  Complexity of a Union--Find
                                  Implementation in Separation Logic with
                                  Time Credits . . . . . . . . . . . . . . 331--365
              Tobias Nipkow and   
                  Hauke Brinkop   Amortized Complexity Verified  . . . . . 367--391
          Alexander Leitsch and   
                    Anela Lolic   Extraction of Expansion Trees  . . . . . 393--430

Journal of Automated Reasoning
Volume 62, Number 4, April, 2019

             Xingyuan Zhang and   
                Christian Urban   Selected Extended Papers of ITP 2015:
                                  Preface  . . . . . . . . . . . . . . . . 431--432
Frédéric Besson and   
             Sandrine Blazy and   
                   Pierre Wilke   A Verified CompCert Front-End for a
                                  Memory Model Supporting Pointer
                                  Arithmetic and Uninitialised Data  . . . 433--480
                  Peter Lammich   Refinement to Imperative HOL . . . . . . 481--503
      Sylvain Boulmé and   
      Alexandre Maréchal   Refinement to Certify Abstract
                                  Interpretations: Illustrated on
                                  Linearization for Polyhedra  . . . . . . 505--530
          Ond\vrej Kun\vcar and   
                 Andrei Popescu   A Consistent Foundation for Isabelle/HOL 531--555


Journal of Automated Reasoning
Volume 63, Number 1, June, 2019

              Gilles Barthe and   
            Gustavo Betarte and   
           Juan Diego Campo and   
                    Carlos Luna   System-Level Non-interference of
                                  Constant-Time Cryptography. Part I:
                                  Model  . . . . . . . . . . . . . . . . . 1--51
              Peter Lammich and   
             Andreas Lochbihler   Automatic Refinement to Efficient Data
                                  Structures: a Comparison of Two
                                  Approaches . . . . . . . . . . . . . . . 53--94
              Gabriel Ebner and   
               Stefan Hetzl and   
          Alexander Leitsch and   
               Giselle Reis and   
                  Daniel Weller   On the Generation of Quantified Lemmas   95--126
       Tomá\vs Peitl and   
        Friedrich Slivovsky and   
                 Stefan Szeider   Long-Distance $Q$-Resolution with
                                  Dependency Schemes . . . . . . . . . . . 127--155

Journal of Automated Reasoning
Volume 63, Number 2, August, 2019

     Peter Lefanu Lumsdaine and   
               Nicolas Tabareau   Preface: Special Issue on Homotopy Type
                                  Theory and Univalent Foundations . . . . 157--158
                 Marc Bezem and   
            Thierry Coquand and   
                    Simon Huber   The Univalence Axiom in Cubical Sets . . 159--171
                    Simon Huber   Canonicity for Cubical Type Theory . . . 173--210
              Lars Birkedal and   
              Ale\vs Bizjak and   
            Ranald Clouston and   
       Hans Bugge Grathwohl and   
               Bas Spitters and   
                 Andrea Vezzosi   Guarded Cubical Type Theory  . . . . . . 211--253
             Guillaume Brunerie   The James Construction and $ \pi_4
                                  (\mathbb {S}^3) $ in Homotopy Type
                                  Theory . . . . . . . . . . . . . . . . . 255--284
            Benedikt Ahrens and   
              Ralph Matthes and   
           Anders Mörtberg   From Signatures to Monads in UniMath . . 285--318
Mauricio Ayala-Rincón and   
      César Muñoz   Selected Extended Papers of ITP 2017 . . 319--321
          Xavier Allamigeon and   
                Ricardo D. Katz   A Formalization of Convex Polyhedra
                                  Based on the Simplex Method  . . . . . . 323--345
         Alexander Bentkamp and   
Jasmin Christian Blanchette and   
                Dietrich Klakow   A Formal Proof of the Expressiveness of
                                  Deep Learning  . . . . . . . . . . . . . 347--368
Frédéric Besson and   
             Sandrine Blazy and   
                   Pierre Wilke   CompCertS: a Memory-Aware Verified C
                                  Compiler Using a Pointer as Integer
                                  Semantics  . . . . . . . . . . . . . . . 369--392
            Yannick Forster and   
                    Gert Smolka   Call-by-Value Lambda Calculus as a Model
                                  of Computation in Coq  . . . . . . . . . 393--413
              Dominik Kirst and   
                    Gert Smolka   Categoricity Results and Large Model
                                  Constructions for Second-Order ZF in
                                  Dependent Type Theory  . . . . . . . . . 415--438
             Andreas Lochbihler   Effect Polymorphism in Higher-Order
                                  Logic (Proof Pearl)  . . . . . . . . . . 439--462
     Adam Sandberg Ericsson and   
           Magnus O. Myreen and   
    Johannes Åman Pohjola   A Verified Generational Garbage
                                  Collector for CakeML . . . . . . . . . . 463--488
           Yannick Zakowski and   
              David Cachera and   
           Delphine Demange and   
              Gustavo Petri and   
            David Pichardie and   
         Suresh Jagannathan and   
                      Jan Vitek   Verifying a Concurrent Garbage Collector
                                  with a Rely-Guarantee Methodology  . . . 489--515
                     Bohua Zhan   Formalization of the Fundamental Group
                                  in Untyped Set Theory Using Auto2  . . . 517--538

Journal of Automated Reasoning
Volume 63, Number 3, October, 2019

                        Jia Tao   A PSpace Algorithm for Acyclic Epistemic
                                  $ {\rm DL}(\mathcal {ALCS})5_m $ . . . . 539--555
            Cezary Kaliszyk and   
                    Karol P\kak   Semantics of Mizar as an Isabelle Object
                                  Logic  . . . . . . . . . . . . . . . . . 557--595
           Olaf Beyersdorff and   
           Joshua Blinkhorn and   
                 Leroy Chew and   
             Renate Schmidt and   
                    Martin Suda   Reinterpreting Dependency Schemes:
                                  Soundness Meets Incompleteness in DQBF   597--623
                    Dale Miller   Mechanized Metatheory Revisited  . . . . 625--665
              Hing-Lun Chan and   
                Michael Norrish   Classification of Finite Fields with
                                  Applications . . . . . . . . . . . . . . 667--693
  Lu\'ìs Cruz-Filipe and   
         Joao Marques-Silva and   
           Peter Schneider-Kamp   Formally Verifying the Solution to the
                                  Boolean Pythagorean Triples Problem  . . 695--722
                 Wenxi Wang and   
  Harald Sòndergaard and   
               Peter J. Stuckey   Wombit: a Portfolio Bit-Vector Solver
                                  Using Word-Level Propagation . . . . . . 723--762
         Mohammad Abdulaziz and   
            Lawrence C. Paulson   An Isabelle/HOL Formalisation of Green's
                                  Theorem  . . . . . . . . . . . . . . . . 763--786
                 Li-Ming Li and   
               Zhi-Ping Shi and   
                  Yong Guan and   
            Qian-Ying Zhang and   
                   Yong-Dong Li   Formalization of Geometric Algebra in
                                  HOL Light  . . . . . . . . . . . . . . . 787--808

Journal of Automated Reasoning
Volume 63, Number 4, December, 2019

           Iliano Cervesato and   
       Maribel Fernández   Preface to the Special Issue on
                                  Linearity  . . . . . . . . . . . . . . . 809--811
            Patrick Baillot and   
              Gilles Barthe and   
                   Ugo Dal Lago   Implicit Computational Complexity of
                                  Subrecursive Definitions and
                                  Applications to Cryptographic Proofs . . 813--855
              Quentin Heath and   
                    Dale Miller   A Proof Theory for Model Checking  . . . 857--885
                     Ian Mackie   Linear Numeral Systems . . . . . . . . . 887--909
                Matteo Acclavio   Proof Diagrams for Multiplicative Linear
                                  Logic: Syntax and Semantics  . . . . . . 911--939
               Luca Paolini and   
              Mauro Piccolo and   
               Margherita Zorzi   QPCF: Higher-Order Languages and Quantum
                                  Circuits . . . . . . . . . . . . . . . . 941--966
     Mohamed Yousri Mahmoud and   
                   Amy P. Felty   Formalization of Metatheory of the
                                  Quipper Quantum Programming Language in
                                  a Linear Logic . . . . . . . . . . . . . 967--1002
              Clark Barrett and   
               Temesghen Kahsai   Selected Extended Papers of NFM 2017:
                                  Preface  . . . . . . . . . . . . . . . . 1003--1004
             Andrew Sogokon and   
            Paul B. Jackson and   
              Taylor T. Johnson   Verifying Safety and Persistence in
                                  Hybrid Systems Using Flowpipes and
                                  Continuous Invariants  . . . . . . . . . 1005--1029
            Tommaso Dreossi and   
     Alexandre Donzé and   
               Sanjit A. Seshia   Compositional Falsification of
                                  Cyber-Physical Systems with Machine
                                  Learning Components  . . . . . . . . . . 1031--1053
                 Susmit Jha and   
                Tuhin Sahai and   
            Vasumathi Raman and   
           Alessandro Pinto and   
                Michael Francis   Explaining AI Decisions Using Efficient
                                  Methods for Learning Sparse Boolean
                                  Formulae . . . . . . . . . . . . . . . . 1055--1075
              Hadar Frenkel and   
              Orna Grumberg and   
                Sarai Sheinvald   An Automata-Theoretic Approach to
                                  Model-Checking Systems and
                                  Specifications Over Infinite Data
                                  Domains  . . . . . . . . . . . . . . . . 1077--1101
      Bernhard K. Aichernig and   
                 Martin Tappler   Efficient Active Automata Learning via
                                  Mutation Testing . . . . . . . . . . . . 1103--1134


Journal of Automated Reasoning
Volume 64, Number 1, January, 2020

           Cheng-Chao Huang and   
                    Ming Xu and   
                     Zhi-Bin Li   A Conflict-Driven Solving Procedure for
                                  Poly-Power Constraints . . . . . . . . . 1--20
                Linh Anh Nguyen   ExpTime Tableaux with Global Caching for
                                  Hybrid PDL . . . . . . . . . . . . . . . 21--52
  Christoph Benzmüller and   
                  Dana S. Scott   Automating Free Logic in HOL, with an
                                  Experimental Application in Category
                                  Theory . . . . . . . . . . . . . . . . . 53--72
             Xingyuan Zhang and   
            Christian Urban and   
                     Chunhan Wu   Priority Inheritance Protocol Proved
                                  Correct  . . . . . . . . . . . . . . . . 73--95
              Paula Chocron and   
            Pascal Fontaine and   
          Christophe Ringeissen   Politeness and Combination Methods for
                                  Theories with Bridging Functions . . . . 97--134
            Marta Cialdea Mayer   A Prover Dealing with Nominals, Binders,
                                  Transitivity and Relation Hierarchies    135--165

Journal of Automated Reasoning
Volume 64, Number 2, February, 2020

                 Salvador Lucas   Using Well-Founded Relations for Proving
                                  Operational Termination  . . . . . . . . 167--195
          Peter Baumgartner and   
              Renate A. Schmidt   Blocking and Other Enhancements for
                                  Bottom-Up Model Generation Methods . . . 197--251
                 M. Echenim and   
                     N. Peltier   Combining Induction and Saturation-Based
                                  Theorem Proving  . . . . . . . . . . . . 253--294
 Maximiliano Cristiá and   
               Gianfranco Rossi   Solving Quantifier-Free First-Order
                                  Constraints Over Finite Sets and Binary
                                  Relations  . . . . . . . . . . . . . . . 295--330
                   Wenda Li and   
            Lawrence C. Paulson   Evaluating Winding Numbers and Counting
                                  Complex Roots Through Cauchy Indices in
                                  Isabelle/HOL . . . . . . . . . . . . . . 331--360

Journal of Automated Reasoning
Volume 64, Number 3, March, 2020

                Armin Biere and   
             Cesare Tinelli and   
           Christoph Weidenbach   Preface to the Special Issue on
                                  Automated Reasoning Systems  . . . . . . 361--362
   Sebastiaan J. C. Joosten and   
       René Thiemann and   
                 Akihisa Yamada   A Verified Implementation of Algebraic
                                  Numbers in Isabelle/HOL  . . . . . . . . 363--389
              Matt Kaufmann and   
              J. Strother Moore   Limited Second--Order Functionality in a
                                  First--Order Setting . . . . . . . . . . 391--422
         Roberto Sebastiani and   
                Patrick Trentin   OptiMathSAT: A Tool for Optimization
                                  Modulo Theories  . . . . . . . . . . . . 423--460
       Cláudia Nalon and   
            Ullrich Hustadt and   
                    Clare Dixon   A Resolution--Based Theorem Prover for $
                                  \mathsf {K}_n $: Architecture,
                                  Refinements, Strategies and Experiments  461--484
             Haniel Barbosa and   
Jasmin Christian Blanchette and   
             Mathias Fleury and   
                Pascal Fontaine   Scalable Fine--Grained Proofs for
                                  Formula Processing . . . . . . . . . . . 485--510
              Leonardo de Moura   Preface: Selected Extended Papers of
                                  CADE 2017  . . . . . . . . . . . . . . . 511--511
                  Peter Lammich   Efficient Verified (UN)SAT Certificate
                                  Checking . . . . . . . . . . . . . . . . 513--532
         Marijn J. H. Heule and   
             Benjamin Kiesl and   
                    Armin Biere   Strong Extension--Free Proof Systems . . 533--554
                Gadi Tellez and   
              James Brotherston   Automatically Verifying Temporal
                                  Properties of Pointer Programs with
                                  Cyclic Proof . . . . . . . . . . . . . . 555--578
       Maria Paola Bonacina and   
Stéphane Graham-Lengrand and   
              Natarajan Shankar   Conflict-Driven Satisfiability for
                                  Theory Combination: Transition System
                                  and Completeness . . . . . . . . . . . . 579--609
             Andreas Teucke and   
           Christoph Weidenbach   SPASS-AR: A First--Order Theorem Prover
                                  Based on Approximation--Refinement into
                                  the Monadic Shallow Linear Fragment  . . 611--640

Journal of Automated Reasoning
Volume 64, Number 4, April, 2020

              Lorenzo Gheri and   
                 Andrei Popescu   A Formalized General Theory of Syntax
                                  with Bindings: Extended Version  . . . . 641--675
              Siddhartha Gadgil   Homogeneous Length Functions on Groups:
                                  Intertwined Computer and Human Proofs    677--688
            G. I. Moghaddam and   
             R. Padmanabhan and   
                     Yang Zhang   Automated Reasoning with Power Maps  . . 689--697
        Jose Divasón and   
   Sebastiaan J. C. Joosten and   
       René Thiemann and   
                 Akihisa Yamada   A Verified Implementation of the
                                  Berlekamp--Zassenhaus Factorization
                                  Algorithm  . . . . . . . . . . . . . . . 699--735
             Mnacho Echenim and   
         Hervé Guiol and   
                Nicolas Peltier   Formalizing the Cox--Ross--Rubinstein
                                  Pricing of European Derivatives in
                                  Isabelle/HOL . . . . . . . . . . . . . . 737--765
            Ricardo Peña   An Assertional Proof of Red--Black Trees
                                  Using Dafny  . . . . . . . . . . . . . . 767--791

Journal of Automated Reasoning
Volume 64, Number 5, June, 2020

              Jeremy Avigad and   
                 Assia Mahboubi   Preface: Selected Extended Papers from
                                  Interactive Theorem Proving 2018 . . . . 793--794
          Christian Doczkal and   
                    Damien Pous   Graph Theory in Coq: Minors, Treewidth,
                                  and Isomorphisms . . . . . . . . . . . . 795--825
       René Thiemann and   
             Ralph Bottesch and   
        Jose Divasón and   
            Max W. Haslbeck and   
   Sebastiaan J. C. Joosten and   
                 Akihisa Yamada   Formalizing the LLL Basis Reduction
                                  Algorithm and the LLL Factorization
                                  Algorithm in Isabelle/HOL  . . . . . . . 827--856
         Matthew L. Daggitt and   
                Ran Zmigrod and   
             Timothy G. Griffin   A Relaxation of Üresin and Dubois'
                                  Asynchronous Fixed--Point Theory in Agda 857--877
               Manuel Eberl and   
            Max W. Haslbeck and   
                  Tobias Nipkow   Verified Analysis of Random Binary Tree
                                  Structures . . . . . . . . . . . . . . . 879--910
         Hira Taqdees Syeda and   
                   Gerwin Klein   Formal Reasoning Under Cached Address
                                  Translation  . . . . . . . . . . . . . . 911--945
            Matthieu Sozeau and   
             Abhishek Anand and   
              Simon Boulier and   
                Cyril Cohen and   
            Yannick Forster and   
               Fabian Kunze and   
            Gregory Malecha and   
           Nicolas Tabareau and   
       Théo Winterhalter   The MetaCoq Project  . . . . . . . . . . 947--999

Journal of Automated Reasoning
Volume 64, Number 6, August, 2020

            Guillaume Burel and   
             Guillaume Bury and   
    Raphaël Cauderlier and   
             David Delahaye and   
          Pierre Halmagrand and   
                Olivier Hermant   First-Order Automated Reasoning with
                                  Theories: When Deduction Modulo Theory
                                  Meets Practice . . . . . . . . . . . . . 1001--1050
          Ákos Hajdu and   
          Zoltán Micskei   Efficient Strategies for CEGAR-Based
                                  Model Checking . . . . . . . . . . . . . 1051--1091
               Clemens Ballarin   Exploring the Structure of an Algebra
                                  Text with Locales  . . . . . . . . . . . 1093--1121
            Reynald Affeldt and   
           Jacques Garrigue and   
               Takafumi Saikawa   A Library for Formalization of Linear
                                  Error-Correcting Codes . . . . . . . . . 1123--1164

Journal of Automated Reasoning
Volume 64, Number 7, October, 2020

            Didier Galmiche and   
             Stephan Schulz and   
             Roberto Sebastiani   Preface: Special Issue of Selected
                                  Extended Papers from IJCAR 2018  . . . . 1165--1167
       Anders Schlichtkrull and   
          Jasmin Blanchette and   
            Dmitriy Traytel and   
                   Uwe Waldmann   Formalizing Bachmair and Ganzinger's
                                  Ordered Resolution Prover  . . . . . . . 1169--1195
     Dominique Larchey-Wendling   Constructive Decision via
                                  Redundancy-Free Proof-Search . . . . . . 1197--1219
                     Anupam Das   From QBFs to MALL and Back via Focussing 1221--1245
             Benjamin Kiesl and   
 Adrián Rebola-Pardo and   
         Marijn J. H. Heule and   
                    Armin Biere   Simulating Strong Practical Proof
                                  Systems with Extended Resolution . . . . 1247--1267
             Marcelo Finger and   
                   Sandro Preto   Probably Partially True: Satisfiability
                                  for \Lukasiewicz Infinitely Valued
                                  Probabilistic Logic and Related Topics   1269--1286
          Oskar Abrahamsson and   
                     Son Ho and   
            Hrutvik Kanabar and   
               Ramana Kumar and   
           Magnus O. Myreen and   
            Michael Norrish and   
                  Yong Kiam Tan   Proof-Producing Synthesis of CakeML from
                                  Monadic HOL Functions  . . . . . . . . . 1287--1306
            Sylvain Conchon and   
             David Declerck and   
                Fatiha Za\"\idi   Parameterized Model Checking on the TSO
                                  Weak Memory Model  . . . . . . . . . . . 1307--1330
                 Dirk Beyer and   
                Marieke Huisman   Selected and Extended Papers from TACAS
                                  2018: Preface  . . . . . . . . . . . . . 1331--1332
             Kshitij Bansal and   
              Eric Koskinen and   
                     Omer Tripp   Synthesizing Precise and Useful
                                  Commutativity Conditions . . . . . . . . 1333--1359
               Randal E. Bryant   Chain Reduction for Binary and
                                  Zero-Suppressed Decision Diagrams  . . . 1361--1391
            Adrien Champion and   
               Tomoya Chiba and   
            Naoki Kobayashi and   
                   Ryosuke Sato   ICE-Based Refinement Type Discovery for
                                  Higher-Order Functional Programs . . . . 1393--1418
                Peter Chini and   
               Roland Meyer and   
               Prakash Saivasan   Fine-Grained Complexity of Safety
                                  Verification . . . . . . . . . . . . . . 1419--1444
             Gabriele Costa and   
          Letterio Galletta and   
           Pierpaolo Degano and   
                David Basin and   
                   Chiara Bodei   Natural Projection as Partial Model
                                  Checking . . . . . . . . . . . . . . . . 1445--1481
             Arnd Hartmanns and   
           Sebastian Junges and   
        Joost-Pieter Katoen and   
                   Tim Quatmann   Multi-cost Bounded Tradeoff Analysis in
                                  MDP  . . . . . . . . . . . . . . . . . . 1483--1522
              Daniel Neider and   
              P. Madhusudan and   
          Shambwaditya Saha and   
                Pranav Garg and   
                    Daejun Park   A Learning-Based Approach to
                                  Synthesizing Invariants for Incomplete
                                  Verification Engines . . . . . . . . . . 1523--1552

Journal of Automated Reasoning
Volume 64, Number 8, December, 2020

            Ullrich Hustadt and   
                  Ana Ozaki and   
                    Clare Dixon   Theorem Proving for Pointwise Metric
                                  Temporal Logic Over the Naturals via
                                  Translations . . . . . . . . . . . . . . 1553--1610
             Salvador Lucas and   
       José Meseguer and   
   Raúl Gutiérrez   The $2$D Dependency Pair Framework for
                                  Conditional Rewrite Systems--- Part II:
                                  Advanced Processors and Implementation
                                  Techniques . . . . . . . . . . . . . . . 1611--1662
               R. Alonderis and   
       R. Pliu\vskevi\vcius and   
    A. Pliu\vskevi\vcien\.e and   
                      H. Giedra   Loop-Type Sequent Calculi for Temporal
                                  Logic  . . . . . . . . . . . . . . . . . 1663--1684
              Gilles Barthe and   
            Gustavo Betarte and   
           Juan Diego Campo and   
                Carlos Luna and   
                David Pichardie   System-Level Non-interference of
                                  Constant-Time Cryptography. Part II:
                                  Verified Static Analysis and Stealth
                                  Memory . . . . . . . . . . . . . . . . . 1685--1729


Journal of Automated Reasoning
Volume 65, Number 1, January, 2021

                  Yong Guan and   
              Jingzhi Zhang and   
                    Yongdong Li   Formalization of Euler--Lagrange
                                  Equation Set Based on Variational
                                  Calculus in HOL Light  . . . . . . . . . 1--29
           Danijela Simi\'c and   
              Filip Mari\'c and   
                  Pierre Boutry   Formalization of the Poincaré Disc Model
                                  of Hyperbolic Geometry . . . . . . . . . 31--73
            Guillaume Ambal and   
         Sergue\"\i Lenglet and   
                   Alan Schmitt   HO$ \pi $ in Coq . . . . . . . . . . . . 75--124
           Olaf Beyersdorff and   
           Joshua Blinkhorn and   
                  Meena Mahajan   Building Strategies into QBF Proofs  . . 125--154

Journal of Automated Reasoning
Volume 65, Number 2, February, 2021

              Jasmin Blanchette   Message from the New Editor-in-Chief . . 155--155
           Dario Cattaruzza and   
           Alessandro Abate and   
                Daniel Kroening   Unbounded-Time Safety Verification of
                                  Guarded LTI Models with Inputs by
                                  Abstract Acceleration  . . . . . . . . . 157--203
              Hing Lun Chan and   
                Michael Norrish   Mechanisation of the AKS Algorithm . . . 205--256
          Thibault Gauthier and   
            Cezary Kaliszyk and   
                Michael Norrish   TacticToe: Learning to Prove with
                                  Tactics  . . . . . . . . . . . . . . . . 257--286
        Michael Färber and   
            Cezary Kaliszyk and   
                    Josef Urban   Machine Learning Guidance for Connection
                                  Tableaux . . . . . . . . . . . . . . . . 287--320
             Andrei Popescu and   
              Peter Lammich and   
                       Ping Hou   CoCon: A Conference Management System
                                  with Formally Verified Document
                                  Confidentiality  . . . . . . . . . . . . 321--356

Journal of Automated Reasoning
Volume 65, Number 3, March, 2021

                    Marco Voigt   Decidable $ \exists^* \forall^* $
                                  First-Order Fragments of Linear Rational
                                  Arithmetic with Uninterpreted Predicates 357--423
            Silvio Ghilardi and   
                   Elena Pagani   Higher-Order Quantifier Elimination,
                                  Counter Simulations and Fault-Tolerant
                                  Systems  . . . . . . . . . . . . . . . . 425--460
                 Dirk Beyer and   
             Matthias Dangl and   
                Philipp Wendler   Correction to: A Unifying View on
                                  SMT-Based Software Verification  . . . . 461--461

Journal of Automated Reasoning
Volume 65, Number 4, April, 2021

 Maximiliano Cristiá and   
               Gianfranco Rossi   Automated Proof of Bell--LaPadula
                                  Security Properties  . . . . . . . . . . 463--478
   Véronique Cortier and   
   Stéphanie Delaune and   
         Vaishnavi Sundararajan   A Decidable Class of Security Protocols
                                  for Both Reachability and Equivalence
                                  Properties . . . . . . . . . . . . . . . 479--520
                  D. Butler and   
              A. Lochbihler and   
               A. Gascón   Formalising $ \Sigma $-Protocols and
                                  Commitment Schemes Using CryptHOL  . . . 521--567
      Zhé Hóu and   
                David Sanan and   
                  Jin Song Dong   An Isabelle/HOL Formalisation of the
                                  SPARC Instruction Set Architecture and
                                  the TSO Memory Model . . . . . . . . . . 569--598

Journal of Automated Reasoning
Volume 65, Number 5, June, 2021

             David M. Cerna and   
          Alexander Leitsch and   
                    Anela Lolic   Schematic Refutations of Formula
                                  Schemata . . . . . . . . . . . . . . . . 599--645
             Christoph Wernhard   Craig Interpolation with Clausal
                                  First-Order Tableaux . . . . . . . . . . 647--690
              Anthony Bordg and   
             Hanna Lachnitt and   
                       Yijun He   Certified Quantum Computation in
                                  Isabelle/HOL . . . . . . . . . . . . . . 691--709

Journal of Automated Reasoning
Volume 65, Number 6, August, 2021

               Xicheng Peng and   
                Qihang Chen and   
                       Mao Chen   Automated Discovery of Geometric
                                  Theorems Based on Vector Equations . . . 711--726
              Mauro Vallati and   
       Luká\vs Chrpa and   
                   Frank Hutter   On the Importance of Domain Model
                                  Configuration for Automated Planning
                                  Engines  . . . . . . . . . . . . . . . . 727--773
            Alexander Steen and   
      Christoph Benzmüller   Extensional Higher-Order Paramodulation
                                  in Leo-III . . . . . . . . . . . . . . . 775--807
 Maximiliano Cristiá and   
               Gianfranco Rossi   Automated Reasoning with Restricted
                                  Intensional Sets . . . . . . . . . . . . 809--890

Journal of Automated Reasoning
Volume 65, Number 7, October, 2021

                Pascal Fontaine   Preface: Special Issue of Selected
                                  Extended Papers of CADE 2019 . . . . . . 891--892
         Alexander Bentkamp and   
          Jasmin Blanchette and   
                   Uwe Waldmann   Superposition with Lambdas . . . . . . . 893--940
            Diego Calvanese and   
            Silvio Ghilardi and   
                  Andrey Rivkin   Model Completeness, Uniform Interpolants
                                  and Superposition Calculus . . . . . . . 941--969
          Vojt\vech Havlena and   
Luká\vs Holík and   
          Tomá\vs Vojnar   Automata Terms in a Lazy WS$k$S Decision
                                  Procedure  . . . . . . . . . . . . . . . 971--999
               Aina Niemetz and   
            Mathias Preiner and   
                 Cesare Tinelli   Towards Satisfiability Modulo Parametric
                                  Bit-vectors  . . . . . . . . . . . . . . 1001--1025
             Andrei Popescu and   
                Dmitriy Traytel   Distilling the Requirements of Gödel's
                                  Incompleteness Theorems with a Proof
                                  Assistant  . . . . . . . . . . . . . . . 1027--1070
            Patrick Trentin and   
             Roberto Sebastiani   Optimization Modulo the Theories of
                                  Signed Bit-Vectors and Floating-Point
                                  Numbers  . . . . . . . . . . . . . . . . 1071--1096

Journal of Automated Reasoning
Volume 65, Number 8, December, 2021

              Koen Claessen and   
           Ann Lillieström   Handling Transitive Relations in
                                  First-Order Automated Reasoning  . . . . 1097--1124
 Maximiliano Cristiá and   
               Gianfranco Rossi   An Automatically Verified Prototype of
                                  the Tokeneer ID Station Specification    1125--1151
              Wilfried Sieg and   
            Farzaneh Derakhshan   Human-Centered Automated Proof Search    1153--1190
                 Salvador Lucas   Derivational Complexity and
                                  Context-Sensitive Rewriting  . . . . . . 1191--1229
   Thaynara Arielly de Lima and   
  André Luiz Galdino and   
   Mauricio Ayala-Rincón   Formalization of Ring Theory in PVS  . . 1231--1263
           Michael Kohlhase and   
                   Florian Rabe   Experiences from Exporting Major Proof
                                  Assistant Libraries  . . . . . . . . . . 1265--1298


Journal of Automated Reasoning
Volume 66, Number 1, February, 2022

               Sarah Sigley and   
               Olaf Beyersdorff   Proof Complexity of Modal Resolution . . 1--41
       Maria Paola Bonacina and   
Stéphane Graham-Lengrand and   
              Natarajan Shankar   Conflict-Driven Satisfiability for
                                  Theory Combination: Lemmas, Modules, and
                                  Proofs . . . . . . . . . . . . . . . . . 43--91
Jonathan Julián Huerta y Munive and   
                   Georg Struth   Predicate Transformer Semantics for
                                  Hybrid Systems . . . . . . . . . . . . . 93--139
            Sadegh Dalvandi and   
             Brijesh Dongol and   
                 Heike Wehrheim   Integrating Owicki--Gries for C11-Style
                                  Memory Models into Isabelle/HOL  . . . . 141--171
           André Platzer   Correction to: Differential Dynamic
                                  Logic for Hybrid Systems . . . . . . . . 173--173

Journal of Automated Reasoning
Volume 66, Number 2, May, 2022

               Sylvie Boldo and   
François Clément and   
                 Micaela Mayero   A Coq Formalization of Lebesgue
                                  Integration of Nonnegative Functions . . 175--213
            Robert Y. Lewis and   
                     Minchao Wu   A Bi-Directional Extensible Interface
                                  Between Lean and Mathematica . . . . . . 215--238
        Piotr Wojciechowski and   
               K. Subramani and   
              R. Chandrasekaran   Analyzing Read-Once Cutting Plane Proofs
                                  in Horn Systems  . . . . . . . . . . . . 239--274

Journal of Automated Reasoning
Volume 66, Number 3, August, 2022

            Nicolas Peltier and   
   Viorica Sofronie-Stokkermans   Special Issue of Selected Extended
                                  Papers of IJCAR 2020 . . . . . . . . . . 275--276
          Joshua Brakensiek and   
               Marijn Heule and   
           David Narváez   The Resolution of Keller's Conjecture    277--300
               Franz Baader and   
                   Deepak Kapur   Deciding the Word Problem for Ground and
                                  Strongly Shallow Identities w.r.t.
                                  Extensional Symbols  . . . . . . . . . . 301--329
                 Ying Sheng and   
                 Yoni Zohar and   
                  Clark Barrett   Polite Combination of Algebraic
                                  Datatypes  . . . . . . . . . . . . . . . 331--355
               Franz Baader and   
                   Jakub Rydval   Using Model Theory to Find Decidable and
                                  Tractable Description Logics with
                                  Concrete Domains . . . . . . . . . . . . 357--407
            Diego Calvanese and   
            Silvio Ghilardi and   
                  Andrey Rivkin   Combination of Uniform Interpolants via
                                  Beth Definability  . . . . . . . . . . . 409--435

Journal of Automated Reasoning
Volume 66, Number 4, November, 2022

           Maria Paola Bonacina   Six Decades of Automated Reasoning:
                                  Papers in Memory of Larry Wos  . . . . . 437--438
             Michael Beeson and   
       Maria Paola Bonacina and   
             Michael Kinyon and   
                Geoff Sutcliffe   Larry Wos: Visions of Automated
                                  Reasoning  . . . . . . . . . . . . . . . 439--461
           Maria Paola Bonacina   Set of Support, Demodulation,
                                  Paramodulation: a Historical Perspective 463--497
               Uwe Waldmann and   
             Sophie Tourret and   
            Simon Robillard and   
              Jasmin Blanchette   A Comprehensive Framework for Saturation
                                  Theorem Proving  . . . . . . . . . . . . 499--539
         Petar Vukmirovi\'c and   
         Alexander Bentkamp and   
          Jasmin Blanchette and   
              Simon Cruanes and   
              Visa Nummelin and   
                 Sophie Tourret   Making Higher-Order Superposition Work   541--564
                  Robert Veroff   A Wos Challenge Met  . . . . . . . . . . 565--574
             Sophie Tourret and   
           Christoph Weidenbach   A Posthumous Contribution by Larry Wos:
                                  Excerpts from an Unpublished Column  . . 575--584
             Andreas Lochbihler   A Mechanized Proof of the Max--Flow
                                  Min--Cut Theorem for Countable Networks
                                  with Applications to Probability Theory  585--610
                Anne Baanen and   
           Sander R. Dahmen and   
           Ashvni Narayanan and   
Filippo A. E. Nuccio Mortarino Majno di Capriglio   A Formalization of Dedekind Domains and
                                  Class Groups of Global Fields  . . . . . 611--637
           Fabio Papacchini and   
       Cláudia Nalon and   
            Ullrich Hustadt and   
                    Clare Dixon   Local is Best: Efficient Reductions to
                                  Modal Logic K  . . . . . . . . . . . . . 639--666
                 Akihisa Yamada   Tuple Interpretations for Termination of
                                  Term Rewriting . . . . . . . . . . . . . 667--688
        Predrag Jani\vci\'c and   
                 Julien Narboux   Theorem Proving as Constraint Solving
                                  with Coherent Logic  . . . . . . . . . . 689--746
            David J. Pearce and   
                Mark Utting and   
                 Lindsay Groves   Verifying Whiley Programs with Boogie    747--803
              Joshua Meyers and   
            David I. Spivak and   
                  Ryan Wisnesky   Fast Left Kan Extensions Using the Chase 805--844
            Dennis de Champeaux   Faster Linear Unification Algorithm  . . 845--860
                Nuno Macedo and   
              Julien Brunel and   
             David Chemouil and   
                   Alcino Cunha   Pardinus: a Temporal Relational Model
                                  Finder . . . . . . . . . . . . . . . . . 861--904
           Mallku Soldevila and   
               Beta Ziliani and   
                Bruno Silvestre   From Specification to Testing: Semantics
                                  Engineering for Lua 5.2  . . . . . . . . 905--952
         Richard Schmoetten and   
             Jake E. Palmer and   
            Jacques D. Fleuriot   Towards Formalising Schutz' Axioms for
                                  Minkowski Spacetime in Isabelle/HOL  . . 953--988
           Wilmer Ricciotti and   
                   James Cheney   A Formalization of SQL with Nulls  . . . 989--1030
Thiago Mendonça Ferreira Ramos and   
       Ariane Alves Almeida and   
   Mauricio Ayala-Rincón   Formalization of the Computational
                                  Theory of a Turing Complete Functional
                                  Language Model . . . . . . . . . . . . . 1031--1063
        Jose Divasón and   
           René Thiemann   A Formalization of the Smith Normal Form
                                  in Higher--Order Logic . . . . . . . . . 1065--1095
        Jose Divasón and   
           René Thiemann   Correction to: A Formalization of the
                                  Smith Normal Form in Higher--Order Logic 1097--1097
           Fabio Papacchini and   
       Cláudia Nalon and   
            Ullrich Hustadt and   
                    Clare Dixon   Correction to: Local is Best: Efficient
                                  Reductions to Modal Logic K  . . . . . . 1099--1099


Journal of Automated Reasoning
Volume 67, Number 1, March, 2023

        Simon Roßkopf and   
                  Tobias Nipkow   A Formalization and Proof Checker for
                                  Isabelle's Metalogic . . . . . . . . . . ??
            Chelsea Edmonds and   
Angeliki Koutsoukou-Argyraki and   
            Lawrence C. Paulson   Formalising Szemerédi's Regularity Lemma
                                  and Roth's Theorem on Arithmetic
                                  Progressions in Isabelle/HOL . . . . . . ??
                  Guido Fiorino   Linear Depth Deduction with Subformula
                                  Property for Intuitionistic Epistemic
                                  Logic  . . . . . . . . . . . . . . . . . ??
                Qinshi Wang and   
                Andrew W. Appel   A Solver for Arrays with Concatenation   ??
             Pedro Quaresma and   
             Pierluigi Graziani   Measuring the Readability of Geometric
                                  Proofs: The Area Method Case . . . . . . ??
       Maria Paola Bonacina and   
                  Sarah Winkler   Semantically-Guided Goal-Sensitive
                                  Reasoning: Decision Procedures and the
                                  Koala Prover . . . . . . . . . . . . . . ??
           Alvaro Velasquez and   
            Ismail Alkhouri and   
               K. Subramani and   
        Piotr Wojciechowski and   
                    George Atia   Optimal Deterministic Controller
                                  Synthesis from Steady-State
                                  Distributions  . . . . . . . . . . . . . ??
            Andrew W. Appel and   
                   Xavier Leroy   Efficient Extensional Binary Tries . . . ??
         Richard Schmoetten and   
             Jake E. Palmer and   
            Jacques D. Fleuriot   Correction: Towards Formalising Schutz'
                                  Axioms for Minkowski Spacetime in
                                  Isabelle/HOL . . . . . . . . . . . . . . ??
         Alexander Bentkamp and   
          Jasmin Blanchette and   
             Sophie Tourret and   
             Petar Vukmirovi\'c   Superposition for Higher-Order Logic . . ??
                    Mak Andrlon   Finding Normal Binary Floating-Point
                                  Factors Efficiently  . . . . . . . . . . ??
               Aaron A. Windsor   Computer-Aided Constructions of
                                  Commafree Codes  . . . . . . . . . . . . ??
              Dominik Kirst and   
                    Marc Hermes   Synthetic Undecidability and
                                  Incompleteness of First-Order Axiom
                                  Systems in Coq . . . . . . . . . . . . . ??

Journal of Automated Reasoning
Volume 67, Number 2, June, 2023

            Aart Middeldorp and   
         Alexander Lochmann and   
           Fabian Mitterwallner   First-Order Theory of Rewriting for
                                  Linear Variable-Separated Rewrite
                                  Systems: Automation, Formalization,
                                  Certification  . . . . . . . . . . . . . ??
                 Emre Yolcu and   
             Scott Aaronson and   
             Marijn J. H. Heule   An Automated Approach to the Collatz
                                  Conjecture . . . . . . . . . . . . . . . ??
              Gabriel Ebner and   
          Jasmin Blanchette and   
                 Sophie Tourret   Unifying Splitting . . . . . . . . . . . ??
 Maximiliano Cristiá and   
              Guido De Luca and   
                    Carlos Luna   An Automatically Verified Prototype of
                                  the Android Permissions System . . . . . ??
                    Oliver Nash   Engel's Theorem in Mathlib . . . . . . . ??
           Alessandro Abate and   
             Haniel Barbosa and   
              Clark Barrett and   
             Cristina David and   
             Pascal Kesseli and   
            Daniel Kroening and   
         Elizabeth Polgreen and   
            Andrew Reynolds and   
                 Cesare Tinelli   Synthesising Programs with Non-trivial
                                  Constants  . . . . . . . . . . . . . . . ??
            Cezary Kaliszyk and   
                    Karol P\kak   Combining Higher-Order Logic with Set
                                  Theory Formalizations  . . . . . . . . . ??
    Luís Cruz-Filipe and   
           Fabrizio Montesi and   
               Marco Peressotti   A Formal Theory of Choreographic
                                  Programming  . . . . . . . . . . . . . . ??

Journal of Automated Reasoning
Volume 67, Number 3, September, 2023

          Hendrik Leidinger and   
           Christoph Weidenbach   SCL(EQ): SCL for First--Order Logic with
                                  Equality . . . . . . . . . . . . . . . . ??
                 Andrei Popescu   Rensets and Renaming-Based Recursion for
                                  Syntax with Bindings Extended Version    ??
                Christian Urban   POSIX Lexing with Derivatives of Regular
                                  Expressions  . . . . . . . . . . . . . . ??
    \vSt\vepán Holub and   
             Martin Ra\vska and   
     \vSt\vepán Starosta   Binary Codes that do not Preserve
                                  Primitivity  . . . . . . . . . . . . . . ??
               Yun-Rong Luo and   
                  Che Cheng and   
              Jie-Hong R. Jiang   A Resolution Proof System for Dependency
                                  Stochastic Boolean Satisfiability  . . . ??
                 Anupam Das and   
              Marianna Girlando   Cyclic Hypersequent System for
                                  Transitive Closure Logic . . . . . . . . ??
            Reynald Affeldt and   
                    Cyril Cohen   Measure Construction by Extension in
                                  Dependent Type Theory with Application
                                  to Integration . . . . . . . . . . . . . ??
              Marco Maggesi and   
            Cosimo Perini Brogi   Mechanising Gödel--Löb Provability Logic
                                  in HOL Light . . . . . . . . . . . . . . ??
             Mnacho Echenim and   
                Nicolas Peltier   A Proof Procedure for Separation Logic
                                  with Inductive Definitions and Data  . . ??
           Joseph E. Reeves and   
         Marijn J. H. Heule and   
               Randal E. Bryant   Preprocessing of Propagation Redundant
                                  Clauses  . . . . . . . . . . . . . . . . ??
                 Ying Sheng and   
         Andres Nötzli and   
            Andrew Reynolds and   
                 Yoni Zohar and   
                 David Dill and   
         Wolfgang Grieskamp and   
                Junkil Park and   
                Shaz Qadeer and   
              Clark Barrett and   
                 Cesare Tinelli   Reasoning About Vectors: Satisfiability
                                  Modulo a Theory of Sequences . . . . . . ??

Journal of Automated Reasoning
Volume 67, Number 4, December, 2023

   Érik Martin-Dorel and   
        Guillaume Melquiond and   
                    Pierre Roux   Enabling Floating-Point Arithmetic in
                                  the Coq Proof Assistant  . . . . . . . . ??
                 Ying Sheng and   
                 Yoni Zohar and   
      Christophe Ringeissen and   
            Andrew Reynolds and   
              Clark Barrett and   
                 Cesare Tinelli   Combining Stable Infiniteness and
                                  (Strong) Politeness  . . . . . . . . . . ??
         Benjamin Böhm and   
               Olaf Beyersdorff   Lower Bounds for QCDCL via Formula Gauge ??
     Philipp G. Haselwarter and   
                   Andrej Bauer   Finitary Type Theories With and Without
                                  Contexts . . . . . . . . . . . . . . . . ??
            Andrzej Indrzejczak   Bisequent Calculus for Four-Valued
                                  Quasi-Relevant Logics: Cut Elimination
                                  and Interpolation  . . . . . . . . . . . ??
               Xicheng Peng and   
            Jingzhong Zhang and   
                   Mao Chen and   
                   Sannyuya Liu   Self-evident Automated Geometric Theorem
                                  Proving Based on Complex Number Identity ??
                  Sen Zheng and   
              Renate A. Schmidt   Saturation-Based Boolean Conjunctive
                                  Query Answering and Rewriting for the
                                  Guarded Quantification Fragments . . . . ??