ARiAT
Financiado
Advanced Reasoning in Arithmetic Theories
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, arti...
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.
ver más
Duración del proyecto: 62 meses
Fecha Inicio: 2019-10-08
Fecha Fin: 2024-12-31
Fecha Fin: 2024-12-31
Línea de financiación: concedida
El organismo H2020 notifico la concesión del proyecto el día 2019-10-08
Línea de financiación objetivo
El proyecto se financió a través de la siguiente ayuda:
ERC-2019-STG:
ERC Starting Grant
Cerrada
hace 6 años
Presupuesto
El presupuesto total del proyecto asciende a
1M€
Líder del proyecto
THE CHANCELLOR MASTERS AND SCHOLARS OF THE UN...
No se ha especificado una descripción o un objeto social para esta compañía.
Perfil tecnológico
TRL
4-5
Perfil tecnológico
TRL
4-5
625.24K€ |
Participante