Volume 64, Issue 3

Search all Journal of Automated Reasoning articles

March 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

Issue Editors:

Armin Biere,
Cesare Tinelli,
Christoph Weidenbach,
Leonardo de Moura

12 articles in this issue

Preface to the Special Issue on Automated Reasoning Systems
Armin Biere
Cesare Tinelli
Christoph Weidenbach
EditorialNotes 13 August 2019 Pages: 361 - 362
A Verified Implementation of Algebraic Numbers in Isabelle/HOL
Sebastiaan J. C. Joosten
René Thiemann
Akihisa Yamada
OriginalPaper Open access 09 December 2018 Pages: 363 - 389
Limited Second-Order Functionality in a First-Order Setting
Matt Kaufmann
J Strother Moore
OriginalPaper 17 December 2018 Pages: 391 - 422
OptiMathSAT: A Tool for Optimization Modulo Theories
Roberto Sebastiani
Patrick Trentin
OriginalPaper 15 December 2018 Pages: 423 - 460
A Resolution-Based Theorem Prover for \({\textsf {K}}_{n}^{}\): Architecture, Refinements, Strategies and Experiments
Cláudia Nalon
Ullrich Hustadt
Clare Dixon
OriginalPaper Open access 17 December 2018 Pages: 461 - 484
Scalable Fine-Grained Proofs for Formula Processing
Haniel Barbosa
Jasmin Christian Blanchette
Pascal Fontaine
OriginalPaper 04 January 2019 Pages: 485 - 510
Preface: Selected Extended Papers of CADE 2017
Leonardo de Moura
EditorialNotes 17 February 2020 Pages: 511 - 511
Efficient Verified (UN)SAT Certificate Checking
Peter Lammich
OriginalPaper Open access 04 June 2019 Pages: 513 - 532
Strong Extension-Free Proof Systems
Marijn J. H. Heule
Benjamin Kiesl
Armin Biere
OriginalPaper Open access 22 February 2019 Pages: 533 - 554
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Gadi Tellez
James Brotherston
OriginalPaper Open access 09 August 2019 Pages: 555 - 578
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness
Maria Paola Bonacina
Stéphane Graham-Lengrand
Natarajan Shankar
OriginalPaper 04 January 2019 Pages: 579 - 609
SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment
Andreas Teucke
Christoph Weidenbach
OriginalPaper 25 February 2020 Pages: 611 - 640

Volume 64, Issue 3

Search

Navigation