JSYML
2010
12 years 11 months ago
2010
We consider valued fields with a distinguished isometry or contractive derivation as valued modules over the Ore ring of difference operators. Under certain assumptions on the resi...
LPAR
2010
Springer
13 years 2 months ago
2010
Springer
Craig interpolation has become a key ingredient in many symbolic model checkers, serving as an approximative replacement for expensive quantifier elimination. In this paper, we foc...
JSYML
2000
13 years 4 months ago
2000
The notion of a D-ring, generalizing that of a differential or a difference ring, is introduced. Quantifier elimination and a version of the AxKochen-Ershov principle is proven for...
JAR
2008
13 years 4 months ago
2008
This article presents detailed implementations of quantifier elimination for both integer and real linear arithmetic for theorem provers. The underlying algorithms are those by Coo...
ENTCS
2008
13 years 4 months ago
2008
Most well-known algorithms for equational solving are based on quantifier elimination. This technique iteratively eliminates the innermost block of existential/universal quantifie...
CASC
2009
Springer
13 years 5 months ago
2009
Springer
We consider Presburger arithmetic extended by infinity. For this we give an effective quantifier elimination and decision procedure which implies also the completeness of our exten...
IJCAI
2001
13 years 6 months ago
2001
A technique is proposed for computing the weakest sufficient (wsc) and strongest necessary (snc) conditions for formulas in an expressive fragment of first-order logic using quant...
AISC
2010
Springer
13 years 7 months ago
2010
Springer
We prove formally that the first order theory of algebraically closed fields enjoy quantifier elimination, and hence is decidable. This proof is organized in two modular parts. We ...
CASC
2006
Springer
13 years 8 months ago
2006
Springer
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 practi...
AISC
2004
Springer
13 years 8 months ago
2004
Springer
We present a new method for generic quantifier elimination that uses an extension of Hermitian quantifier elimination. By means of sample computations we show that this generic Her...