External Links

    Journal: Journal of Automated Reasoning

    Volume 43, Issue 4

    337 -- 362Geoff Sutcliffe. The TPTP Problem Library and Associated Infrastructure
    363 -- 446Xavier Leroy. A Formally Verified Compiler Back-end

    Volume 43, Issue 3

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

    Volume 43, Issue 2

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

    Volume 43, Issue 1

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