It is known that the first-order theory of p-adic fields is decidable, and that the p-adics admit elimination of quantifiers. What is the state of the art in algorithmic aspects of quantifier elimination over p-adic fields? Are there implementations of such algorithms?
$\begingroup$
$\endgroup$
Add a comment
|