In 2014 CADE Inc. established the Thoralf Skolem Award to reward a CADE paper that has passed the test of time, by being a most influential paper in the field. Beginning with CADE-25 (2015), at every CADE the Skolem Award Committee selects a paper presented at the CADE held 10 years earlier to receive the Skolem award.
Every CADE has its own Skolem award committee, whose office terminates with the CADE for which it was appointed. The CADE board of trustees appoints the chair of the Skolem award committee, and the chair appoints the rest of the committee. The Skolem award committee evaluates the papers and selects those to be awarded, and the chair informs the CADE board of trustees of the final result. Under exceptional circumstances, two awards (ex aequo) or no award may be given.
In order to cover the entire history of CADE, beginning with CADE-25 (2015), in addition to the Skolem award to a paper presented at the CADE held 10 years earlier, every CADE conference offers three additional Skolem awards for papers presented at CADE’s held approximately 20, 30, and 40 years earlier. Whenever a CADE offers multiple Skolem awards, one single Skolem award committee is responsible for all of them. The Skolem award schedule follows. On the account of their workshop status, a few very early CADE’s are combined under one Skolem award.
CADE-24: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Radu Iosif, Adam Rogalewicz, Jirí Simácek
for the paper “The Tree Width of Separation Logic with Recursive Definitions”, published in the CADE-24 proceedings in 2013. The paper is recognized for being the first to show decidability of a fragment of separating logic that can deal with recursively defined data structures such as trees, and thereby triggering extensive research on the decidability and complexity of such fragments.
Presented at CADE-29 The 29th International Conference on Automated Deduction July, 2023
Jürgen Giesl President of CADE Inc.
The Skolem Award Committee consisted of Franz Baader (chair), Clare Dixon, Pascal Fontaine, Martin Giese, Konstantin Korovin, Tobias Nipkow, and Sarah M. Winkler.
CADE-23: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Jasmin C. Blanchette, Sascha Böhme, and Lawrence C. Paulson
for the paper “Extending Sledgehammer with SMT Solvers”, and to
Kryštof Hoder and Andrei Voronkov
for the paper “Sine Qua Non for Large Theory Reasoning”, both published in the CADE-23 proceedings in 2011. The paper by Jasmin Blanchette, Sascha Böhme, and Larry Paulson is recognized for the successful integration of automated solvers into a widely used interactive theorem prover, with a significant speed-up in automating proofs. The paper by Kryštof Hoder and Andrei Voronkov is recognized for bringing to maturity the idea of symbol-based heuristics for axiom selection, with lasting impact on automated reasoning in large theories.
Presented at CADE-28 The 28th International Conference on Automated Deduction July, 2021
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Maria Paola Bonacina (chair), Wolfgang Ahrendt, Thierry Boy de la Tour, Amy Felty, Michael Rusinowitch, Manfred Schmidt-Schauss, Peter Schneider-Kamp.
CADE-22: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Rajeev Goré and Florian Widmann
for the paper “An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability” published in the CADE-22 proceedings in 2009. The paper is recognised for presenting the first decision procedure for propositional dynamic logic which is both theoretically optimal and effective in practice. Previous decision procedures are either suboptimal in the worst case, or worst-case optimal but with poor average-case performance. The solution in this paper thereby closed a problem that had been open for almost 30 years.
Presented at CADE-27 The 27th International Conference on Automated Deduction August, 2019
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Alexander Leitsch (chair), Peter Baumgartner, James Brotherston, Laura Kovacs, Hans de Nivelle, Nicolas Peltier, Renate Schmidt.
CADE-21: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Leonardo de Moura and Nikolaj Bjørner
for the paper “Efficient E-Matching for SMT Solvers” published in the CADE-21 proceedings in 2001. The paper is recognized for proposing efficient new techniques which have importantly advanced the state of the art in quantifier reasoning for SMT.
Presented at CADE-26 The 26th International Conference on Automated Deduction August, 2017
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of John Slaney (chair), Peter Baumgartner, Neil Murray, Renate Schmidt, Aaron Stump, Geoff Suttcliffe, Toby Walsh.
CADE-20: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to:
Christian Urban and Christine Tasson
for the paper “Nominal techniques in Isabelle/HOL” published in the CADE-20 proceedings in 2005. The paper is recognized as being the first to show how to use nominal techniques to deal with bound variables in higher order theorem provers.
Presented at CADE-25 The 25th International Conference on Automated Deduction August, 2015
Maria Paola Bonacina President of CADE Inc.
The Skolem Award Committee consisted of Claude Kirchner (chair), Alessandro Armando, Gilles Barthe, Christopher Lynch, Leonardo de Moura, Uli Sattler, Geoff Sutcliffe, Toby Walsh, Christoph Weidenbach.
CADE-18: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani
for the paper “A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions”, and to
Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi
for the paper “The Complexity of the Graded µ-Calculus”, both published in the CADE-18 proceedings in 2002. The paper by Audemard et al. is recognised for proposing pioneering techniques for the efficient integration of arithmetic decision procedures into a framework for satisfiability modulo theories. Many of those techniques are used in state-of-the-art SMT solvers and contribute to their efficiency. The paper by Kupferman et al. is recognized for showing that the complexity of the satisfiability problem for the modal µ-calculus extended with graded modalities is ExpTime, and thus not harder than for the pure modal µ-calculus, which was a very challenging task for binary coding of the numbers in the graded modalities. The solution is based on the new concept of graded alternating tree automata, which can also be used in other settings.
Presented at CADE-29 The 29th International Conference on Automated Deduction July, 2023
Jürgen Giesl President of CADE Inc.
The Skolem Award Committee consisted of Franz Baader (chair), Clare Dixon, Pascal Fontaine, Martin Giese, Konstantin Korovin, Tobias Nipkow, and Sarah M. Winkler.
CADE-17: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Ian Horrocks, Ulrike Sattler, and Stephan Tobies
for the paper “Reasoning with Individuals for the Description Logic SHIQ”, published in the CADE-17 proceedings in 2000. The paper is recognized for a practical and efficient tableau-based decision procedure for satisfiability in an expressive description logic that has wide applicability in knowledge representation, databases, and the semantic web.
Presented at CADE-28 The 28th International Conference on Automated Deduction July, 2021
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Maria Paola Bonacina (chair), Wolfgang Ahrendt, Thierry Boy de la Tour, Amy Felty, Michael Rusinowitch, Manfred Schmidt-Schauss, Peter Schneider-Kamp.
CADE-16: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Christoph Weidenbach
for the paper “Towards an Automated Analysis of Security Protocols” published in the CADE-16 proceedings in 1999. The paper is recognised for two main contributions to automated deduction: first, its novel application of general theorem proving techniques to a key-exchange security protocol; and, second, its development of new decidability and undecidability results for fragments of monadic Horn theories.
Presented at CADE-27 The 27th International Conference on Automated Deduction August, 2019
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Alexander Leitsch (chair), Peter Baumgartner, James Brotherston, Laura Kovacs, Hans de Nivelle, Nicolas Peltier, Renate Schmidt.
CADE-15: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Andreas Nonnengart, Georg Rock and Christoph Weidenbach
for the paper “On Generating Small Clause Normal Forms” published in the CADE-15 proceedings in 1998. The paper is recognized for recognizing the importance of clause normal form transformation in effective clause-based ATP, and developing foundational techniques that are now used in state-of-the-art ATP systems.
Presented at CADE-26 The 26th International Conference on Automated Deduction August, 2017
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of John Slaney (chair), Peter Baumgartner, Neil Murray, Renate Schmidt, Aaron Stump, Geoff Suttcliffe, Toby Walsh.
CADE-14: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Hantao Zhang
for the paper “SATO: An Efficient Propositional Prover” published in the CADE-14 proceedings in 1997. The paper is recognized for its seminal contribution to the design and implementation of novel techniques, including lazy data structures and clever Boolean constraint propagation that caused a step change in the area and deeply influenced later systems.
Presented at CADE-25 The 25th International Conference on Automated Deduction August, 2015
Maria Paola Bonacina President of CADE Inc.
The Skolem Award Committee consisted of Claude Kirchner (chair), Alessandro Armando, Gilles Barthe, Christopher Lynch, Leonardo de Moura, Uli Sattler, Geoff Sutcliffe, Toby Walsh, Christoph Weidenbach.
CADE-12: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Geoff Sutcliffe, Christian B. Suttner, and Theodor Yemenis
for the paper “The TPTP Problem Library”, published in the CADE-12 proceedings in 1994. This paper introduces the TPTP library of problems for automated theorem provers (ATPs). The library has become the standard for empirical comparisons of ATPs and has given rise to the annual ATP competition CASC.
Presented at CADE-29 The 29th International Conference on Automated Deduction July, 2023
Jürgen Giesl President of CADE Inc.
The Skolem Award Committee consisted of Franz Baader (chair), Clare Dixon, Pascal Fontaine, Martin Giese, Konstantin Korovin, Tobias Nipkow, and Sarah M. Winkler.
CADE-11: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Sam Owre, John M. Rushby, and Natarajan Shankar
for the paper “PVS: A Prototype Verification System”, published in the CADE-11 proceedings in 1992. The paper is recognized for the design of the PVS system as a bridge between automated and interactive reasoning, with embedded decision procedures, simplification, programmable strategies, and proofs as software, as well as for the impact of PVS on deductive verification.
Presented at CADE-28 The 28th International Conference on Automated Deduction July, 2021
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Maria Paola Bonacina (chair), Wolfgang Ahrendt, Thierry Boy de la Tour, Amy Felty, Michael Rusinowitch, Manfred Schmidt-Schauss, Peter Schneider-Kamp.
CADE-10: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Leo Bachmair and Harald Ganzinger
for the paper “On Restrictions of Ordered Paramodulation with Simplification” published in the CADE-10 proceedings in 1990. The paper is recognised for its development of the superposition calculus for equational first-order clauses alongside a new and powerful framework for proving completeness and accommodating redundancy. This framework forms the basis of many advanced modern theorem provers, and has been highly influential in accelerating progress in the area of automated deduction.
Presented at CADE-27 The 27th International Conference on Automated Deduction August, 2019
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Alexander Leitsch (chair), Peter Baumgartner, James Brotherston, Laura Kovacs, Hans de Nivelle, Nicolas Peltier, Renate Schmidt.
CADE-9: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Alan Bundy
for the paper “The Use of Explicit Plans to Guide Inductive Proofs” published in the CADE-9 proceedings in 1988. The paper is recognized as introducing proof planning, inspiring and establishing the research programme as one of the key paradigms of automated reasoning.
Presented at CADE-26 The 26th International Conference on Automated Deduction August, 2017
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of John Slaney (chair), Peter Baumgartner, Neil Murray, Renate Schmidt, Aaron Stump, Geoff Suttcliffe, Toby Walsh.
CADE-8: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Leo Bachmair and Nachum Dershowitz
for the paper “Commutation, Transformation, and Termination” published in the CADE-8 proceedings in 1986. The paper is recognized as laying the foundations of today’s termination theorem proving techniques.
Presented at CADE-25 The 25th International Conference on Automated Deduction August, 2015
Maria Paola Bonacina President of CADE Inc.
The Skolem Award Committee consisted of Claude Kirchner (chair), Alessandro Armando, Gilles Barthe, Christopher Lynch, Leonardo de Moura, Uli Sattler, Geoff Sutcliffe, Toby Walsh, Christoph Weidenbach.
CADE-6: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Robert E. Shostak
for the paper “Deciding Combinations of Theories”, published in the CADE-6 proceedings in 1982. The paper is recognised for the approach to combine theories that was later named “Shostak’s method”, and that was very influential both for the theory and practice of SMT solving.
Presented at CADE-29 The 29th International Conference on Automated Deduction July, 2023
Jürgen Giesl President of CADE Inc.
The Skolem Award Committee consisted of Franz Baader (chair), Clare Dixon, Pascal Fontaine, Martin Giese, Konstantin Korovin, Tobias Nipkow, and Sarah M. Winkler.
CADE-5: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Joseph A. Goguen
for the paper “How to Prove Algebraic Inductive Hypotheses Without Induction”, and to
Jean-Marie Hullot
for the paper “Canonical Forms and Unification”, both published in the CADE-5 proceedings in 1980. The paper by Joe Goguen is recognized for fundamental contributions to the discovery of the inductionless induction method. The paper by Jean-Marie Hullot is recognized for paramount advances to the idea of solving equational unification problems by completion.
Presented at CADE-28 The 28th International Conference on Automated Deduction July, 2021
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Maria Paola Bonacina (chair), Wolfgang Ahrendt, Thierry Boy de la Tour, Amy Felty, Michael Rusinowitch, Manfred Schmidt-Schauss, Peter Schneider-Kamp.
CADE-4: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Peter Andrews
for the paper “General Matings” published in the CADE-4 proceedings in 1979. The paper is recognised for its invention of the generalised mating method for constructing refutations of formulas in negation normal form. This development paved the ground for the subsequent construction of many non-resolution methods in automated deduction, including the well-known connection method.
Presented at CADE-27 The 27th International Conference on Automated Deduction August, 2019
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of Alexander Leitsch (chair), Peter Baumgartner, James Brotherston, Laura Kovacs, Hans de Nivelle, Nicolas Peltier, Renate Schmidt.
CADE-2 and CADE-3: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Zohar Manna and Richard Waldinger
for the paper “The Automatic Synthesis of Recursive Programs” published in the CADE-3 proceedings in 1977. The paper is recognized as a landmark in the development of foundations for research in deductive program synthesis.
Presented at CADE-26 The 26th International Conference on Automated Deduction August, 2017
Christoph Weidenbach President of CADE Inc.
The Skolem Award Committee consisted of John Slaney (chair), Peter Baumgartner, Neil Murray, Renate Schmidt, Aaron Stump, Geoff Suttcliffe, Toby Walsh.
CADE-0 and CADE-1: International Conference on Automated Deduction (CADE) Skolem Award for a CADE paper that has Passed the Test of Time, by being a Most Influential Paper in the field. Presented to
Nicolaas Govert de Bruijn
for the paper “The Mathematical Language AUTOMATH, its Usage, and Some of its Extensions” published in the CADE-0 proceedings in 1968. The paper is recognized for the landmark and remarkable contribution to the design and implementation of higher-order theorem provers.
Presented at CADE-25 The 25th International Conference on Automated Deduction August, 2015
Maria Paola Bonacina President of CADE Inc.
The Skolem Award Committee consisted of Claude Kirchner (chair), Alessandro Armando, Gilles Barthe, Christopher Lynch, Leonardo de Moura, Uli Sattler, Geoff Sutcliffe, Toby Walsh, Christoph Weidenbach.