Summary
Arithmetic theories are logical theories for reasoning about number
systems, such as the integers and reals. Such theories find a
plethora of applications across computer science, including in
algorithmic verification, artificial intelligence, and compiler
optimisation. The appeal of arithmetic theories is their generality:
once a problem has been formalised in a decidable such theory, a
dedicated solver can in principle be used in a push-button fashion
to obtain a solution. Arithmetic theories are also of great
importance for showing decidability and complexity results in a
variety of domains.
Decision procedures for quantifier-free and linear fragments of
arithmetic theories have been among the most intensively studied and
impactful topics in theoretical computer science. However, emerging
applications require more expressive theories, including support for
quantifiers, counting, and non-linear functions. Unfortunately, the
lack of understanding of the computational properties of such
extensions means that existing decision procedures are not
applicable or do not scale.
The overall goal of this proposal is to advance the state-of-the-art
in decision procedures for expressive arithmetic theories. To this
end, starting with a recent breakthrough made by the PI, we will
develop novel and optimal quantifier-elimination procedures for
linear arithmetic theories, which we plan to eventually integrate
into mainstream SMT solvers. Furthermore, we aim to improve
complexity bounds and push the decidability frontier of extensions
of arithmetic theories with counting and non-linear operations. The
proposed research requires to tackle long-standing open
problems---some of them being decades old. In short, the project
will lay algorithmic foundations on which next-generation decision
procedures and reasoners for arithmetic theories will be built.
systems, such as the integers and reals. Such theories find a
plethora of applications across computer science, including in
algorithmic verification, artificial intelligence, and compiler
optimisation. The appeal of arithmetic theories is their generality:
once a problem has been formalised in a decidable such theory, a
dedicated solver can in principle be used in a push-button fashion
to obtain a solution. Arithmetic theories are also of great
importance for showing decidability and complexity results in a
variety of domains.
Decision procedures for quantifier-free and linear fragments of
arithmetic theories have been among the most intensively studied and
impactful topics in theoretical computer science. However, emerging
applications require more expressive theories, including support for
quantifiers, counting, and non-linear functions. Unfortunately, the
lack of understanding of the computational properties of such
extensions means that existing decision procedures are not
applicable or do not scale.
The overall goal of this proposal is to advance the state-of-the-art
in decision procedures for expressive arithmetic theories. To this
end, starting with a recent breakthrough made by the PI, we will
develop novel and optimal quantifier-elimination procedures for
linear arithmetic theories, which we plan to eventually integrate
into mainstream SMT solvers. Furthermore, we aim to improve
complexity bounds and push the decidability frontier of extensions
of arithmetic theories with counting and non-linear operations. The
proposed research requires to tackle long-standing open
problems---some of them being decades old. In short, the project
will lay algorithmic foundations on which next-generation decision
procedures and reasoners for arithmetic theories will be built.
Unfold all
/
Fold all
More information & hyperlinks
| Web resources: | https://cordis.europa.eu/project/id/852769 |
| Start date: | 01-01-2020 |
| End date: | 31-12-2024 |
| Total budget - Public funding: | 1 481 864,00 Euro - 1 481 864,00 Euro |
Cordis data
Original description
Arithmetic theories are logical theories for reasoning about numbersystems, such as the integers and reals. Such theories find a
plethora of applications across computer science, including in
algorithmic verification, artificial intelligence, and compiler
optimisation. The appeal of arithmetic theories is their generality:
once a problem has been formalised in a decidable such theory, a
dedicated solver can in principle be used in a push-button fashion
to obtain a solution. Arithmetic theories are also of great
importance for showing decidability and complexity results in a
variety of domains.
Decision procedures for quantifier-free and linear fragments of
arithmetic theories have been among the most intensively studied and
impactful topics in theoretical computer science. However, emerging
applications require more expressive theories, including support for
quantifiers, counting, and non-linear functions. Unfortunately, the
lack of understanding of the computational properties of such
extensions means that existing decision procedures are not
applicable or do not scale.
The overall goal of this proposal is to advance the state-of-the-art
in decision procedures for expressive arithmetic theories. To this
end, starting with a recent breakthrough made by the PI, we will
develop novel and optimal quantifier-elimination procedures for
linear arithmetic theories, which we plan to eventually integrate
into mainstream SMT solvers. Furthermore, we aim to improve
complexity bounds and push the decidability frontier of extensions
of arithmetic theories with counting and non-linear operations. The
proposed research requires to tackle long-standing open
problems---some of them being decades old. In short, the project
will lay algorithmic foundations on which next-generation decision
procedures and reasoners for arithmetic theories will be built.
Status
SIGNEDCall topic
ERC-2019-STGUpdate Date
27-04-2024
Images
No images available.
Geographical location(s)
