In 1988, Weispfenning published a seminal paper introducing a substitution technique for
quantifier elimination in the linear theories of ordered and valued fields. The original focus …

Quantifier elimination methods for real closed fields are an intensively studied subject from
both theoretical and practical points of view. This thesis studies quantifier elimination based …

We consider the complexity of deciding the truth of first-order existential sentences of linear
arithmetic with divisibility over both the integers and the p-adic numbers. We show that if an …

We consider the complexity of the satisfiability problems for the existential fragment of Büchi
arithmetic and for the existential fragment of linear arithmetic over p-adic fields. Our main …

Nous donnons un aperçu des développements de la théorie des modèles des nombres p-
adiques depuis les travaux de Denef sur la rationalité de séries de Poincaré, par une revue …

We describe a weak quantifier elimination procedure for the full linear theory of the integers.
This theory is a generalization of Presburger arithmetic, where the coefficients are arbitrary …

1.1 Overview redlog stands for reduce logic system. It provides an extension of the computer
algebra system reduce to a computer logic system implementing symbolic algorithms on rst …

We address various aspects of our computer algebra-based computer logic system redlog.
There are numerous examples in the literature for successful applications of redlog to …

This paper presents the Dr. Doodle system, an interactive theorem prover that uses
diagrammatic representations. The assumption underlying this project is that, for some …

We consider existential problems over the reals. Extended quantifier elimination generalizes
the concept of regular quantifier elimination by providing in addition answers, which are …