DecidabilityAlgorithms

A homepage for the Decidability Algorithms workgroup.

Involved sites:

Chalmers University of Technology and Göteborg University: Department of Computer Science and Engineering (CSE below).
Göteborg University: Department of Philosophy, Linguistics and Theory of Science (PLATOS below).

Participants:

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