default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJournal of Automated Reasoning, Volume 47
Volume 47, Number 1, June 2011
- Michael J. C. Gordon, Matt Kaufmann, Sandip Ray:
The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. 1-16 - John Thangarajah
, Lin Padgham:
Computationally Effective Reasoning About Goal Interactions. 17-56 - Louise A. Dennis, Ian Green, Alan Smaill:
The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling. 57-105
Volume 47, Number 2, August 2011
- Renate A. Schmidt, Brigitte Pientka:
Preface: Special Issue of Selected Extended Papers of CADE-22. 107-109 - Koen Claessen, Ann Lillieström:
Automated Inference of Finite Unsatisfiability. 111-132 - Carsten Fuhs, Jürgen Giesl, Michael Parting, Peter Schneider-Kamp, Stephan Swiderski:
Proving Termination by Dependency Pairs and Inductive Theorem Proving. 133-160 - Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura:
On Deciding Satisfiability by Theorem Proving with Speculative Inferences. 161-189 - Peter Baumgartner, Uwe Waldmann:
A Combined Superposition and Model Evolution Calculus. 191-227
Volume 47, Number 3, October 2011
- Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo:
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2. 229-250 - Moa Johansson, Lucas Dixon, Alan Bundy:
Conjecture Synthesis for Inductive Theories. 251-289 - Amine Chaieb:
Formal Power Series. 291-318 - Gianni Ciolli, Graziano Gentili, Marco Maggesi:
A Certified Proof of the Cartan Fixed Point Theorems. 319-336
Volume 47, Number 4, December 2011
- Jürgen Giesl, Reiner Hähnle:
Preface: Special Issue of Selected Extended Papers of IJCAR 2010. 337-339 - Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl:
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. 341-367 - Jasmin Christian Blanchette, Alexander Krauss:
Monotonicity Inference for Higher-Order Formulas. 369-398 - Hans de Nivelle:
Classical Logic with Partial Functions. 399-425 - Despoina Magka, Yevgeny Kazakov, Ian Horrocks:
Tractable Extensions of the Description Logic ${\mathcal{EL}}$ with Numerical Datatypes. 427-450 - Julian Backes, Chad E. Brown:
Analytic Tableaux for Higher-Order Logic with Choice. 451-479 - Nao Hirokawa, Aart Middeldorp:
Decreasing Diagrams and Relative Termination. 481-501
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-01-15 20:50 CET 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:
