---
title: "Journal of Automated Reasoning 2011 — papers"
description: "Journal of Automated Reasoning 2011 — papers: 1 paper in the Elamur Research library, with our summaries, ranked by citations."
canonical: "https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2011/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2011/)

[home](https://md.research.elamur.ai/free/en/) / [venues](https://md.research.elamur.ai/free/en/venues/) / [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/) / 2011

# Journal of Automated Reasoning 2011 — papers

The works of Journal of Automated Reasoning published in 2011 that our library holds (publisher: Springer Science+Business Media): 1 work, listed below with the most cited first; each has a page with our summary, its key points and its references.

[**30** works that year](#all) · [**1** work in our library](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2011/#works) · [**152** citations of these works](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2011/#works)

## Most cited papers

By their OpenAlex citations; a paper with our summary links to its page here, the others to the original.

1. **[The Locally Nameless Representation ↗](https://doi.org/10.1007/s10817-011-9225-2)**Arthur Charguéraud*149 citations*
2. **[Strongly Typed Term Representations in Coq ↗](https://doi.org/10.1007/s10817-011-9219-0)**Nick Benton, Chung-Kil Hur, Andrew John Kennedy et al.*77 citations*
3. **[Proof Pearl: Regular Expression Equivalence and Relation Algebra ↗](https://doi.org/10.1007/s10817-011-9223-4)**Alexander Krauss, Tobias Nipkow*65 citations*
4. **[A Two-Level Logic Approach to Reasoning About Computations ↗](https://doi.org/10.1007/s10817-011-9218-1)**Andrew Gacek, Dale Miller, Gopalan Nadathur*50 citations*
5. **[Simulating Circuit-Level Simplifications on CNF ↗](https://doi.org/10.1007/s10817-011-9239-9)**Matti J„ärvisalo, Armin Biere, Marijn J. H. Heule*47 citations*
6. **[An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic ↗](https://doi.org/10.1007/s10817-011-9237-y)**Angelo Brillout, Daniel Kroening, Philipp Rümmer et al.*34 citations*
7. **[A Canonical Locally Named Representation of Binding ↗](https://doi.org/10.1007/s10817-011-9229-y)**Randy Pollack, Masahiko Sato, Wilmer Ricciotti*31 citations*
8. **[Analytic Tableaux for Higher-Order Logic with Choice ↗](https://doi.org/10.1007/s10817-011-9233-2)**Julian Backes, Chad E. Brown*31 citations*
9. **[Decreasing Diagrams and Relative Termination ↗](https://doi.org/10.1007/s10817-011-9238-x)**Nao Hirokawa, Aart Middeldorp*24 citations*
10. **[Tractable Extensions of the Description Logic EL with Numerical Datatypes ↗](https://doi.org/10.1007/s10817-011-9235-0)**Despoina Magka, Yevgeny Kazakov, Ian Horrocks*23 citations*

## All works of the year (30)

The most cited first; 1 with our summary link to their page here, the others to the original.

1. **[The Locally Nameless Representation ↗](https://doi.org/10.1007/s10817-011-9225-2)**Arthur Charguéraud*149 citations*
2. **[Strongly Typed Term Representations in Coq ↗](https://doi.org/10.1007/s10817-011-9219-0)**Nick Benton, Chung-Kil Hur, Andrew John Kennedy et al.*77 citations*
3. **[Proof Pearl: Regular Expression Equivalence and Relation Algebra ↗](https://doi.org/10.1007/s10817-011-9223-4)**Alexander Krauss, Tobias Nipkow*65 citations*
4. **[A Two-Level Logic Approach to Reasoning About Computations ↗](https://doi.org/10.1007/s10817-011-9218-1)**Andrew Gacek, Dale Miller, Gopalan Nadathur*50 citations*
5. **[Simulating Circuit-Level Simplifications on CNF ↗](https://doi.org/10.1007/s10817-011-9239-9)**Matti J„ärvisalo, Armin Biere, Marijn J. H. Heule*47 citations*
6. **[An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic ↗](https://doi.org/10.1007/s10817-011-9237-y)**Angelo Brillout, Daniel Kroening, Philipp Rümmer et al.*34 citations*
7. **[A Canonical Locally Named Representation of Binding ↗](https://doi.org/10.1007/s10817-011-9229-y)**Randy Pollack, Masahiko Sato, Wilmer Ricciotti*31 citations*
8. **[Analytic Tableaux for Higher-Order Logic with Choice ↗](https://doi.org/10.1007/s10817-011-9233-2)**Julian Backes, Chad E. Brown*31 citations*
9. **[Decreasing Diagrams and Relative Termination ↗](https://doi.org/10.1007/s10817-011-9238-x)**Nao Hirokawa, Aart Middeldorp*24 citations*
10. **[Tractable Extensions of the Description Logic EL with Numerical Datatypes ↗](https://doi.org/10.1007/s10817-011-9235-0)**Despoina Magka, Yevgeny Kazakov, Ian Horrocks*23 citations*
11. **[ExpTime Tableaux for Using Sound Global Caching ↗](https://doi.org/10.1007/s10817-011-9243-0)**Rajeev Prabhakar Goré, Linh Anh Nguyen*21 citations*
12. **[Proving Termination by Dependency Pairs and Inductive Theorem Proving ↗](https://doi.org/10.1007/s10817-010-9215-9)**Carsten Fuhs, Jürgen Giesl, Michael Parting et al.*17 citations*
13. **[Automated Inference of Finite Unsatisfiability ↗](https://doi.org/10.1007/s10817-010-9216-8)**Koen Claessen, Ann Lillieström*14 citations*
14. **[Monotonicity Inference for Higher-Order Formulas ↗](https://doi.org/10.1007/s10817-011-9234-1)**Jasmin Christian Blanchette, Alexander Krauss*14 citations*
15. **[A Presheaf Environment for the Explicit Fusion Calculus ↗](https://doi.org/10.1007/s10817-011-9224-3)**Filippo Bonchi, Maria Grazia Buscemi, Vincenzo Ciancia et al.*12 citations*
16. **[A List-Machine Benchmark for Mechanized Metatheory ↗](https://doi.org/10.1007/s10817-011-9226-1)**Andrew W. Appel, Robert Dockins, Xavier Leroy*11 citations*
17. **[Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction ↗](https://doi.org/10.1007/s10817-011-9227-0)**Steven Schockaert, Jeroen Janssen, Dirk Vermeir*11 citations*
18. **[A Solution to the PoplMark Challenge Based on de Bruijn Indices ↗](https://doi.org/10.1007/s10817-011-9230-5)**Jérôme Vouillon*9 citations*
19. **[On Explicit Substitution with Names ↗](https://doi.org/10.1007/s10817-011-9222-5)**Kristoffer H. Rose, Roel Bloo, Frédéric Lang*9 citations*
20. **[Paramodulation with Non-Monotonic Orderings and Simplification ↗](https://doi.org/10.1007/s10817-011-9244-z)**Miquel Bofill, Albert Rubio*7 citations*
21. **[Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover ↗](https://doi.org/10.1007/s10817-011-9228-z)**Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen et al.*5 citations*
22. **[Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax ↗](https://doi.org/10.1007/s10817-011-9221-6)**James Cheney, Michael Norrish, René Vestergaard*5 citations*
23. **[PSPACE Tableau Algorithms for Acyclic Modalized ALC ↗](https://doi.org/10.1007/s10817-011-9232-3)**Jia Tao, Giora Slutzki, Vasant Honavar*5 citations*
24. **[Invariant-Free Clausal Temporal Resolution ↗](https://doi.org/10.1007/s10817-011-9241-2)**Jose Gaintzarain, Montserrat Hermo, Paqui Lucio et al.*4 citations*
25. **[A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL ↗](https://doi.org/10.1007/s10817-011-9231-4)**Stefan Berghofer*3 citations*

[See all 30 papers in Journal of Automated Reasoning 2011 — papers →](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2011/papers/)

## Works with our summary in our library (1)

The most cited first (OpenAlex citations plus our library's).

1. **[Premise Selection for Mathematics by Corpus Analysis and Kernel Methods](https://md.research.elamur.ai/free/en/papers/alama-2011-premise-selection-mathematics-corpus-analysis/) [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)**Jesse Alama, Tom Heskes, Daniel Kühlwein, et al.*2011 · 152 citations*

## Top topics

Topics of its works in our library, with the number of works on each.

[Reasoning (1)](https://md.research.elamur.ai/free/en/topics/reasoning/)

## Fields

[Computer Science (1)](https://md.research.elamur.ai/free/en/shelves/computer-science/)

## Top authors

Authors with a page who published here most often: their works here, and the citations of those works.

[🧑‍🔬**Josef Urban**1 work here · 152 citations](https://md.research.elamur.ai/free/en/authors/josef-urban/)

## Top institutions

Institutions on the bylines of its works here, by the number of works.

[🎓**University of Lisbon** Lisbon · Portugal 1 work here](https://md.research.elamur.ai/free/en/universities/university-of-lisbon/) · [🎓**Radboud University Nijmegen** Nijmegen · Netherlands 1 work here](https://md.research.elamur.ai/free/en/universities/radboud-university-nijmegen/) · [🎓**Universidade Nova de Lisboa** Lisbon · Portugal 1 work here](https://md.research.elamur.ai/free/en/universities/universidade-nova-de-lisboa/)

works and citations from OpenAlex and our library.

- [next → Journal of Automated Reasoning 2012](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/)
- [↑ back to Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)