18th International Conference on Logic Programming
July 27th to August 1st 2002
U Roskilde, Denmark
[en] arithmetic ; automata ; Presburger
[en] Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of techniques based on finite automata that lead to decision procedures and other useful algorithms, as well as to a normal form, for the first-order linear theory of the integers, of the reals, and of the integers and reals combined. This approach has led to an implemented tool, which has the so far unique capability of handling the linear. first-order theory of the integers and reals combined.
Communauté française de Belgique - Direction de la recherche scientifique - Actions de recherche concertées ; European IST-FET project ADVANCE (IST-1999-29082)