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.

Recipients

  • CADE-24 (2013): Radu Iosif, Adam Rogalewicz, Jirí Simácek - The Tree Width of Separation Logic with Recursive Definitions.
  • CADE-23 (2011): Jasmin C. Blanchette, Sascha Böhme, and Lawrence C. Paulson - Extending Sledgehammer with SMT Solvers.
  • CADE-23 (2011): Kryštof Hoder and Andrei Voronkov - Sine Qua Non for Large Theory Reasoning.
  • CADE-22 (2009): Rajeev Goré and Florian Widmann - An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability.
  • CADE-21 (2007): Leonardo de Moura and Nikolaj Bjørner - Efficient E-Matching for SMT Solvers.
  • CADE-20 (2005): Christian Urban and Christine Tasson - Nominal Techniques in Isabelle/HOL.
  • CADE-18 (2002): Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani - A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.
  • CADE-18 (2002): Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi - The Complexity of the Graded µ-Calculus.
  • CADE-17 (2000): Ian Horrocks, Ulrike Sattler, and Stephan Tobies - Reasoning with Individuals for the Description Logic SHIQ.
  • CADE-16 (1999): Christoph Weidenbach - Towards an Automated Analysis of Security Protocols.
  • CADE-15 (1998): Andreas Nonnengart, Georg Rock and Christoph Weidenbach - On Generating Small Clause Normal Forms.
  • CADE-14 (1997): Hantao Zhang - SATO: An Efficient Propositional Prover.
  • CADE-12 (1994): Geoff Sutcliffe, Christian B. Suttner, and Theodor Yemenis - The TPTP Problem Library.
  • CADE-11 (1992): Sam Owre, John M. Rushby, and Natarajan Shankar - PVS: A Prototype Verification System.
  • CADE-10 (1990): Leo Bachmair and Harald Ganzinger - On Restrictions of Ordered Paramodulation with Simplification.
  • CADE-9 (1988): Alan Bundy - The Use of Explicit Plans to Guide Inductive Proofs.
  • CADE-8 (1986): Leo Bachmair and Nachum Dershowitz - Commutation, Transformation, and Termination.
  • CADE-6 (1982): Robert E. Shostak - Deciding Combinations of Theories.
  • CADE-5 (1980): Joseph A. Goguen - How to Prove Algebraic Inductive Hypotheses Without Induction.
  • CADE-5 (1980): Jean-Marie Hullot - Canonical Forms and Unification.
  • CADE-4 (1979): Peter Andrews - General Matings.
  • CADE-2 (1976) and CADE-3 (1977) considered jointly: Zohar Manna and Richard Waldinger - The Automatic Synthesis of Recursive Programs. (presented at CADE-3).
  • CADE-0 (1968) and CADE-1 (1975) considered jointly: Nicolaas Govert de Bruijn - The Mathematical Language AUTOMATH, its Usage, and Some of its Extensions (presented at CADE-0).

Procedure

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-25 (2015) offers one Skolem award for CADE-20 (2005), one for CADE-14 (1997), one for CADE-8 (1986), and one for CADE-0 (1968) and CADE-1 (1975) considered jointly.
  • CADE-26 (2017) offers one Skolem award for CADE-21 (2007), one for CADE-15 (1998), one for CADE-9 (1988), and one for CADE-2 (1976) and CADE-3 (1977) considered jointly.
  • CADE-27 (2019) offers one Skolem award for CADE-22 (2009), one for CADE-16 (1999), one for CADE-10 (1990), and one for CADE-4 (1979).
  • CADE-28 (2021) offers one Skolem award for CADE-23 (2011), one for CADE-17 (2000), one for CADE-11 (1992), and one for CADE-5 (1980).
  • CADE-29 (2023) offers one Skolem award for CADE-24 (2013), one for CADE-18 (2002), one for CADE-12 (1994), and one for CADE-6 (1982).
  • CADE-30 (2025) offers one Skolem award for CADE-25 (2015), one for CADE-19 (2003), one for CADE-13 (1996), and one for CADE-7 (1984).
  • Steady state is reached in 2027 when CADE-32 offers only one Skolem award.

Citations


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.