External Links

    Journal: Journal of Automated Reasoning

    Volume 23, Issue 3-4

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

    Volume 23, Issue 2

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

    Volume 23, Issue 1

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