default search action
Journal of Automated Reasoning, Volume 57
Volume 57, Number 1, June 2016
- Daniel Kroening, Andrey Rybalchenko:
Preface: Special Issue on Interpolation. 1-2 - Matthias Schlaipfer, Georg Weissenbacher:
Labelled Interpolation Systems for Hyper-Resolution, Clausal, and Local Proofs. 3-36 - Nishant Totla, Thomas Wies:
Complete Instantiation-Based Interpolation. 37-65 - Jürgen Christ, Jochen Hoenicke:
Proof Tree Preserving Tree Interpolation. 67-95
Volume 57, Number 2, August 2016
- Mnacho Echenim, Nicolas Peltier:
A Superposition Calculus for Abductive Reasoning. 97-134 - Pierre Roux:
Formal Proofs of Rounding Error Bounds - With Application to an Automatic Positive Definiteness Check. 135-156 - Peter Franek, Stefan Ratschan, Piotr Zgliczynski:
Quasi-decidability of a Fragment of the First-Order Theory of Real Numbers. 157-185
Volume 57, Number 3, October 2016
- Érik Martin-Dorel, Guillaume Melquiond:
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. 187-217 - Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban:
A Learning-Based Fact Selector for Isabelle/HOL. 219-244 - Thierry Boy de la Tour, Nicolas Peltier:
Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization. 245-280
Volume 57, Number 4, December 2016
- Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen:
Reasoning About Algebraic Data Types with Abstractions. 281-318 - Robbert Krebbers:
A Formal C Memory Model for Separation Logic. 319-387
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.