External Links

    Journal: Journal of Automated Reasoning

    Volume 55, Issue 4

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

    Volume 55, Issue 3

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

    Volume 55, Issue 2

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

    Volume 55, Issue 1

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