Skip to main content
main-content
Top

Journal

Journal of Automated Reasoning

Journal of Automated Reasoning 3/2020

Issue 3/2020

Special Issue: Automated Reasoning Systems / Guest Editors: Armin Biere, Cesare Tinelli, Christoph Weidenbach & Special Issue: Selected Extended Papers of CADE 2017 / Guest Editor: Leonardo de Moura

Table of Contents ( 12 Articles )

13-08-2019 | Issue 3/2020

Preface to the Special Issue on Automated Reasoning Systems

Armin Biere, Cesare Tinelli, Christoph Weidenbach

09-12-2018 | Issue 3/2020 Open Access

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada

17-12-2018 | Issue 3/2020

Limited Second-Order Functionality in a First-Order Setting

Matt Kaufmann, J Strother Moore

15-12-2018 | Issue 3/2020

OptiMathSAT: A Tool for Optimization Modulo Theories

Roberto Sebastiani, Patrick Trentin

17-12-2018 | Issue 3/2020 Open Access

A Resolution-Based Theorem Prover for : Architecture, Refinements, Strategies and Experiments

Cláudia Nalon, Ullrich Hustadt, Clare Dixon

04-01-2019 | Issue 3/2020

Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

17-02-2020 | Issue 3/2020

Preface: Selected Extended Papers of CADE 2017

Leonardo de Moura

04-06-2019 | Issue 3/2020 Open Access

Efficient Verified (UN)SAT Certificate Checking

Peter Lammich

22-02-2019 | Issue 3/2020 Open Access

Strong Extension-Free Proof Systems

Marijn J. H. Heule, Benjamin Kiesl, Armin Biere

09-08-2019 | Issue 3/2020 Open Access

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

Gadi Tellez, James Brotherston

04-01-2019 | Issue 3/2020

Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness

Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar

25-02-2020 | Issue 3/2020

SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Andreas Teucke, Christoph Weidenbach

Current Publications

Premium Partner

    Image Credits