---
title: "Journal of Automated Reasoning 2012 — all accepted papers"
description: "All 28 papers of Journal of Automated Reasoning 2012, the most cited first; those with our summary link to it."
canonical: "https://research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/papers/"
---
[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/papers/)

[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](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/) / papers

# Journal of Automated Reasoning 2012: all accepted papers

28 papers · the most cited first · [← Journal of Automated Reasoning 2012](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/)

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*
26. **[Non-Linear Rewrite Closure and Weak Normalization ↗](https://doi.org/10.1007/s10817-012-9262-5)**Carles Creus, Guillem Godoy, Francesc Massanes et al.
27. **[SMELS: Satisfiability Modulo Equality with Lazy Superposition ↗](https://doi.org/10.1007/s10817-012-9263-4)**Christopher Lynch, Quang-Trung Ta, Duc-Khanh Tran
28. **[The GOEDEL Program ↗](https://doi.org/10.1007/s10817-012-9259-0)**Johan G. F. Belinfante
- [← back to](https://md.research.elamur.ai/free/en/venues/journal-of-automated-reasoning/2012/) — Journal of Automated Reasoning 2012