---
title: "Journal of Automated Reasoning 2013 — papers"
description: "Journal of Automated Reasoning 2013 — 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/2013/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2013/)

[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/) / 2013

# Journal of Automated Reasoning 2013 — papers

The works of Journal of Automated Reasoning published in 2013 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.

[**25** works that year](#all) · [**1** work in our library](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2013/#works) · [**112** citations of these works](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2013/#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 Incredible ELK ↗](https://doi.org/10.1007/s10817-013-9296-3)**Yevgeny Kazakov, Markus Krötzsch, František Simančík*230 citations*
2. **[Extending Sledgehammer with SMT Solvers ↗](https://doi.org/10.1007/s10817-013-9278-5)**Jasmin Christian Blanchette, Sascha Böhme, Lawrence Charles Paulson*158 citations*
3. **[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/)**Jesse Alama, Tom Heskes, Daniel Kühlwein et al.*128 citations · our summary*
4. **[Locales: A Module System for Mathematical Theories ↗](https://doi.org/10.1007/s10817-013-9284-7)**Clemens Ballarin*88 citations*
5. **[Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs ↗](https://doi.org/10.1007/s10817-013-9277-6)**Lars Noschinski, Fabian Emmes, Jürgen Giesl*49 citations*
6. **[Finite-valued Semantics for Canonical Labelled Calculi ↗](https://doi.org/10.1007/s10817-013-9273-x)**Matthias Baaz A, Ori Lahav, Anna Zamansky*35 citations*
7. **[Anti-unification for Unranked Terms and Hedges ↗](https://doi.org/10.1007/s10817-013-9285-6)**Temur Kutsia, Jordi Levy, Mateu Villaret*33 citations*
8. **[Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ↗](https://doi.org/10.1007/s10817-013-9283-8)**Chad E. Brown*33 citations*
9. **[Cutting to the Chase ↗](https://doi.org/10.1007/s10817-013-9281-x)**Dejan Jovanović, Leonardo de Moura*29 citations*
10. **[Formalization of Shannon’s Theorems ↗](https://doi.org/10.1007/s10817-013-9298-1)**Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues*27 citations*

## All works of the year (25)

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

1. **[The Incredible ELK ↗](https://doi.org/10.1007/s10817-013-9296-3)**Yevgeny Kazakov, Markus Krötzsch, František Simančík*230 citations*
2. **[Extending Sledgehammer with SMT Solvers ↗](https://doi.org/10.1007/s10817-013-9278-5)**Jasmin Christian Blanchette, Sascha Böhme, Lawrence Charles Paulson*158 citations*
3. **[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/)**Jesse Alama, Tom Heskes, Daniel Kühlwein et al.*128 citations · our summary*
4. **[Locales: A Module System for Mathematical Theories ↗](https://doi.org/10.1007/s10817-013-9284-7)**Clemens Ballarin*88 citations*
5. **[Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs ↗](https://doi.org/10.1007/s10817-013-9277-6)**Lars Noschinski, Fabian Emmes, Jürgen Giesl*49 citations*
6. **[Finite-valued Semantics for Canonical Labelled Calculi ↗](https://doi.org/10.1007/s10817-013-9273-x)**Matthias Baaz A, Ori Lahav, Anna Zamansky*35 citations*
7. **[Anti-unification for Unranked Terms and Hedges ↗](https://doi.org/10.1007/s10817-013-9285-6)**Temur Kutsia, Jordi Levy, Mateu Villaret*33 citations*
8. **[Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ↗](https://doi.org/10.1007/s10817-013-9283-8)**Chad E. Brown*33 citations*
9. **[Cutting to the Chase ↗](https://doi.org/10.1007/s10817-013-9281-x)**Dejan Jovanović, Leonardo de Moura*29 citations*
10. **[Formalization of Shannon’s Theorems ↗](https://doi.org/10.1007/s10817-013-9298-1)**Reynald Affeldt, Manabu Hagiwara, Jonas Sénizergues*27 citations*
11. **[A Framework for the Verification of Certifying Computations ↗](https://doi.org/10.1007/s10817-013-9289-2)**Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn et al.*24 citations*
12. **[Using Isabelle/HOL to Verify First-Order Relativity Theory ↗](https://doi.org/10.1007/s10817-013-9292-7)**Mike Stannett, Istvàn Németi*14 citations*
13. **[Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution ↗](https://doi.org/10.1007/s10817-013-9275-8)**Matthew Gwynne, Oliver Kullmann*13 citations*
14. **[The Reachability Problem in Constructive Geometric Constraint Solving Based Dynamic Geometry ↗](https://doi.org/10.1007/s10817-013-9280-y)**Marta R. Hidalgo, Robert Joan‐Arinyo*11 citations*
15. **[Array Theory of Bounded Elements and its Applications ↗](https://doi.org/10.1007/s10817-013-9293-6)**Min Qi Zhou, Fei He, Bow-Yaw Wang et al.*10 citations*
16. **[“Decision Procedures: An Algorithmic Point of View,” by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008 ↗](https://doi.org/10.1007/s10817-013-9295-4)**Clark Barrett*10 citations*
17. **[A Goal-Directed Decision Procedure for Hybrid PDL ↗](https://doi.org/10.1007/s10817-013-9294-5)**Mark Kaminski, Gert Smolka*6 citations*
18. **[Mechanizing Metatheory Without Typing Contexts ↗](https://doi.org/10.1007/s10817-013-9287-4)**Jong‐Hyun Park, Jeongbong Seo, Sungwoo Park et al.*6 citations*
19. **[Finite Reasons for Safety ↗](https://doi.org/10.1007/s10817-013-9274-9)**Alexei Lisitsa*5 citations*
20. **[Formally Verified Tableau-Based Reasoners for a Description Logic ↗](https://doi.org/10.1007/s10817-013-9291-8)**María-José Hidalgo, José A. Alonso-Jiménez, Joaquín Borrego‐Díaz et al.*5 citations*
21. **[Terminating Calculi for Propositional Dummett Logic with Subformula Property ↗](https://doi.org/10.1007/s10817-013-9276-7)**Guido Fiorino*5 citations*
22. **[A Connection-based Characterization of Bi-intuitionistic Validity ↗](https://doi.org/10.1007/s10817-013-9279-4)**Didier Galmiche, Daniel Méry*4 citations*
23. **[On Automation in the Verification of Software Barriers: Experience Report ↗](https://doi.org/10.1007/s10817-013-9290-9)**Alexander Malkis, Anindya Banerjee*3 citations*
24. **[Preface: Special Issue of Selected Extended Papers of CADE-23 ↗](https://doi.org/10.1007/s10817-013-9282-9)**Nikolaj Bjørner, Viorica Sofronie-Stokkermans*1 citation*
25. **[Theorem of Three Circles in Coq ↗](https://doi.org/10.1007/s10817-013-9299-0)**Julianna Zsidó*1 citation*

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

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

1. **[MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/) [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)**Cezary Kaliszyk, Josef Urban*2013 · 112 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.

[🧑‍🔬**Cezary Kaliszyk**1 work here · 112 citations](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) · [🧑‍🔬**Josef Urban**1 work here · 112 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.

[🎓**Radboud University Nijmegen** Nijmegen · Netherlands 1 work here](https://md.research.elamur.ai/free/en/universities/radboud-university-nijmegen/) · [🎓**Universität Innsbruck** Innsbruck · Austria 1 work here](https://md.research.elamur.ai/free/en/universities/universitat-innsbruck/)

works and citations from OpenAlex and our library.

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