A homepage for the Decidability Algorithms workgroup.

Involved sites:


  • Thierry Coquand, professor, CSE.
  • David Wahlstedt, post doctor, PLATOS.
  • Anders Mörtberg, Phd student, CSE.
  • Bassel Mannaa, Phd student, CSE.
  • Stevan Andjelkovic, Master Student, CSE.

Funded research projects:

  • European Union's 7th Framework Programme
    ForMath (see wiki page), grant agreement no. 243847.
    Led by Thierry Coquand, with Phd student Anders Mörtberg.
  • ERC Advanced grant project 247219.
    Led by Thierry Coquand, with Phd student Bassel Mannaa.
  • The Swedish Research Council
    Postdoc position, registration number 2008:6902, David Wahlstedt.
    A summary of this project can be found here.

Brief summary:

The aim of this collaboration is to get a better understanding of some decision procedures involving infinite domains, and their constructive justifications.

Seminar series:

To begin, our activity consists of a mini-seminar series. The following topics have been addressed so far:

  • May 25, 2010
    David Wahlstedt
    The size-change principle and the classical justification of its decision procedure.
    The size-change principle for program termination, introduced 2001
    to the functional programming community by Lee, Jones and ben-Amram,
    is a classification of terminating recursive computation rules. It
    generalises lexicographical termination, and its decision algorithm is
    easy to implement (although it is computationally expensive). We
    describe this property and its decision algorithm, whose justification
    uses the infinite version of Ramsey's Theorem.
  • June 15, 2010
    Bassel Mannaa
    Size-change termination and Büchi Automata.
  • August 27, 2010
    Anders Mörtberg
    Quantifier Elimination and Algebraically Closed Fields.
  • September 20, 2020
    (held as a logic seminar at PLATOS)
    David Walhstedt
    Some Ramsey-like theorems in constructive logic and Brouwer's thesis.
    I am going to discuss some ideas about how to deal with
    Ramsey-like theorems in some constructive frameworks, and some aspects
    concerning Brouwer's thesis on bars. I will present two different
    constructive interpretations of Ramsey's theorem, by Theirry Coquand,
    and Vim Weldman and Marc Bezem, respectively. Using these ideas, we
    aim to reason constructively about termination of recursively defined

Other topics to address:

  • S1S: second-order monadic theory of successors
  • LTL