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-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-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-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-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


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.


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.


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.


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.


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.


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.


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.


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.