default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 58
Volume 58, Number 1, January 2017
- Stéphane Demri, Deepak Kapur, Christoph Weidenbach
:
Preface - Special Issue of Selected Extended Papers of IJCAR 2014. 1-2 - Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann:
Analyzing Program Termination and Complexity Automatically with AProVE. 3-31 - Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp, Cornelius Aschermann:
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic. 33-65 - Ismail Ilkan Ceylan, Rafael Peñaloza:
The Bayesian Ontology Language $$\mathcal {BEL}$$ BEL. 67-95 - Marijn J. H. Heule, Martina Seidl, Armin Biere:
Solution Validation and Extraction for QBF Preprocessing. 97-125 - Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer:
An Approximation Framework for Solvers and Decision Procedures. 127-147 - Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel:
Soundness and Completeness Proofs by Coinductive Methods. 149-179 - Michael Beeson, Larry Wos:
Finding Proofs in Tarskian Geometry. 181-207
Volume 58, Number 2, February 2017
- Gabriel Braun, Julien Narboux:
A Synthetic Proof of Pappus' Theorem in Tarski's Geometry. 209-230 - Ana Cristina Rocha Oliveira, André Luiz Galdino, Mauricio Ayala-Rincón:
Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. 231-251 - M. Ganesalingam, W. T. Gowers:
A Fully Automatic Theorem Prover with Human-Style Output. 253-291 - Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret:
Higher-Order Pattern Anti-Unification in Linear Time. 293-310
Volume 58, Number 3, March 2017
- Amy P. Felty, Aart Middeldorp:
Preface: Selected Extended Papers of CADE 2015. 311-312 - Edward Zulkoski, Curtis Bright, Albert Heinle, Ilias S. Kotsireas, Krzysztof Czarnecki, Vijay Ganesh:
Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures. 313-339 - Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. 341-362 - Vijay D'Silva, Caterina Urban:
Abstract Interpretation as Automated Deduction. 363-390 - José Iborra, Naoki Nishida, Germán Vidal, Akihisa Yamada:
Relative Termination via Dependency Pairs. 391-411
Volume 58, Number 4, April 2017
- Jean-Marie Lagniez, Pierre Marquis:
On Preprocessing Techniques and Their Impact on Propositional Model Counting. 413-481 - Manuel Eberl:
Proving Divide and Conquer Complexities in Isabelle/HOL. 483-508 - Jesús Aransay, Jose Divasón:
A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem. 509-535
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-10-22 02:17 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
