External Links

    Journal: Journal of Automated Reasoning

    Volume 51, Issue 4

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

    Volume 51, Issue 3

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

    Volume 51, Issue 2

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

    Volume 51, Issue 1

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