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

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

# Journal of Automated Reasoning 2012 — papers

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

[**28** works that year](#all) · [**1** work in our library](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/#works) · [**165** citations of these works](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/#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 HOL Light Theory of Euclidean Space ↗](https://doi.org/10.1007/s10817-012-9250-9)**John Harrison*101 citations*
2. **[Formalization of Bernstein Polynomials and Applications to Global Optimization ↗](https://doi.org/10.1007/s10817-012-9256-3)**Cesar A. Munoz, Anthony Joseph Narkawicz*73 citations*
3. **[Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program ↗](https://doi.org/10.1007/s10817-012-9255-4)**Sylvie Boldo, François Clément, Jean-Christophe Filliâtre et al.*69 citations*
4. **[ATP and Presentation Service for Mizar Formalizations ↗](https://doi.org/10.1007/s10817-012-9269-y)**Josef Urban, Piotr Rudnicki, Geoff Sutcliffe*68 citations*
5. **[6 Years of SMT-COMP ↗](https://doi.org/10.1007/s10817-012-9246-5)**Clark Barrett, Morgan Deters, Leonardo de Moura et al.*56 citations*
6. **[The Mizar Mathematical Library in OMDoc: Translation and Applications ↗](https://doi.org/10.1007/s10817-012-9271-4)**Mihnea Iancu, Michael Kohlhase, Florian Rabe et al.*48 citations*
7. **[On Rewriting Rules in Mizar ↗](https://doi.org/10.1007/s10817-012-9261-6)**Artur Korniłowicz*38 citations*
8. **[Methods of Lemma Extraction in Natural Deduction Proofs ↗](https://doi.org/10.1007/s10817-012-9267-0)**Karol Pąk*31 citations*
9. **[Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models ↗](https://doi.org/10.1007/s10817-012-9252-7)**Mauro Ferrari, Camillo Fiorentini, Guido Fiorino*28 citations*
10. **[Formal Mathematics for Mathematicians ↗](https://doi.org/10.1007/s10817-012-9268-z)**Andrzej Trybulec, Artur Korniłowicz, Adam Naumowicz et al.*22 citations*

## All works of the year (28)

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

1. **[The HOL Light Theory of Euclidean Space ↗](https://doi.org/10.1007/s10817-012-9250-9)**John Harrison*101 citations*
2. **[Formalization of Bernstein Polynomials and Applications to Global Optimization ↗](https://doi.org/10.1007/s10817-012-9256-3)**Cesar A. Munoz, Anthony Joseph Narkawicz*73 citations*
3. **[Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program ↗](https://doi.org/10.1007/s10817-012-9255-4)**Sylvie Boldo, François Clément, Jean-Christophe Filliâtre et al.*69 citations*
4. **[ATP and Presentation Service for Mizar Formalizations ↗](https://doi.org/10.1007/s10817-012-9269-y)**Josef Urban, Piotr Rudnicki, Geoff Sutcliffe*68 citations*
5. **[6 Years of SMT-COMP ↗](https://doi.org/10.1007/s10817-012-9246-5)**Clark Barrett, Morgan Deters, Leonardo de Moura et al.*56 citations*
6. **[The Mizar Mathematical Library in OMDoc: Translation and Applications ↗](https://doi.org/10.1007/s10817-012-9271-4)**Mihnea Iancu, Michael Kohlhase, Florian Rabe et al.*48 citations*
7. **[On Rewriting Rules in Mizar ↗](https://doi.org/10.1007/s10817-012-9261-6)**Artur Korniłowicz*38 citations*
8. **[Methods of Lemma Extraction in Natural Deduction Proofs ↗](https://doi.org/10.1007/s10817-012-9267-0)**Karol Pąk*31 citations*
9. **[Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models ↗](https://doi.org/10.1007/s10817-012-9252-7)**Mauro Ferrari, Camillo Fiorentini, Guido Fiorino*28 citations*
10. **[Formal Mathematics for Mathematicians ↗](https://doi.org/10.1007/s10817-012-9268-z)**Andrzej Trybulec, Artur Korniłowicz, Adam Naumowicz et al.*22 citations*
11. **[Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets ↗](https://doi.org/10.1007/s10817-012-9272-3)**Eugenio Giovanni Omodeo, Alexandru Ioan Tomescu*21 citations*
12. **[Proof Pearl—A Mechanized Proof of GHC’s Mergesort ↗](https://doi.org/10.1007/s10817-012-9260-7)**Christian Sternagel*14 citations*
13. **[Uncurrying for Termination and Complexity ↗](https://doi.org/10.1007/s10817-012-9248-3)**Nao Hirokawa, Aart Middeldorp, Harald Zankl*13 citations*
14. **[Multi-Completion with Termination Tools ↗](https://doi.org/10.1007/s10817-012-9249-2)**Sarah Winkler, Haruhiko Sato, Aart Middeldorp et al.*11 citations*
15. **[Custom Automations in Mizar ↗](https://doi.org/10.1007/s10817-012-9266-1)**Marco B. Caminati, Giuseppe Rosolini*9 citations*
16. **[Specification and Verification of Concurrent Programs Through Refinements ↗](https://doi.org/10.1007/s10817-012-9258-1)**Sandip Ray, Rob Sumners*8 citations*
17. **[A Tableau Based Decision Procedure for an Expressive Fragment of Hybrid Logic with Binders, Converse and Global Modalities ↗](https://doi.org/10.1007/s10817-012-9257-2)**Serenella Cerrito, Marta Cialdea Mayer*5 citations*
18. **[Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions ↗](https://doi.org/10.1007/s10817-012-9245-6)**James P. Bridge, Lawrence Charles Paulson*5 citations*
19. **[Preface ↗](https://doi.org/10.1007/s10817-012-9254-5)**Benjamin C. Pierce, Stephanie Weirich*4 citations*
20. **[Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar ↗](https://doi.org/10.1007/s10817-012-9265-2)**Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama*3 citations*
21. **[Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints ↗](https://doi.org/10.1007/s10817-012-9270-5)**Carles Creus, Adrià Gascón, Guillem Godoy*2 citations*
22. **[“Handbook of Practical Logic and Automated Reasoning,” by John R. Harrison, Cambridge University Press, 2009 ↗](https://doi.org/10.1007/s10817-012-9251-8)**Freek Wiedijk*2 citations*
23. **[A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions ↗](https://doi.org/10.1007/s10817-012-9253-6)**David Sabel, Manfred Schmidt-Schauß*1 citation*
24. **[Eliciting Implicit Assumptions of Mizar Proofs by Property Omission ↗](https://doi.org/10.1007/s10817-012-9264-3)**Jesse Alama*1 citation*
25. **[On the Formalization of Theories ↗](https://doi.org/10.1007/s10817-012-9247-4)**Jan Mycielski*1 citation*

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

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

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

1. **[Learning-Assisted Automated Reasoning with Flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/) [Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)**Cezary Kaliszyk, Josef Urban*2012 · 165 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 · 165 citations](https://md.research.elamur.ai/free/en/authors/cezary-kaliszyk/) · [🧑‍🔬**Josef Urban**1 work here · 165 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 2011](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2011/)
- [next → Journal of Automated Reasoning 2013](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2013/)
- [↑ back to Journal of Automated Reasoning](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/)