Sciweavers

JSYML
2010
74views more  JSYML 2010»
13 years 5 months ago
Quantifier elimination in valued Ore modules
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...
Luc Bélair, Françoise Point
LPAR
2010
Springer
13 years 8 months ago
Interpolating Quantifier-Free Presburger Arithmetic
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...
Daniel Kroening, Jérôme Leroux, Phili...
JSYML
2000
103views more  JSYML 2000»
13 years 10 months ago
A Model Complete Theory of Valued D-Fields
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...
Thomas Scanlon
JAR
2008
105views more  JAR 2008»
13 years 10 months ago
Proof Synthesis and Reflection for Linear Arithmetic
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...
Amine Chaieb, Tobias Nipkow
ENTCS
2008
110views more  ENTCS 2008»
13 years 10 months ago
A New Proposal Of Quasi-Solved Form For Equality Constraint Solving
Most well-known algorithms for equational solving are based on quantifier elimination. This technique iteratively eliminates the innermost block of existential/universal quantifie...
Javier Álvez, Paqui Lucio
CASC
2009
Springer
180views Mathematics» more  CASC 2009»
13 years 11 months ago
Effective Quantifier Elimination for Presburger Arithmetic with Infinity
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...
Aless Lasaruk, Thomas Sturm
IJCAI
2001
14 years 2 days ago
Computing Strongest Necessary and Weakest Sufficient Conditions of First-Order Formulas
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...
Patrick Doherty, Witold Lukaszewicz, Andrzej Szala...
AISC
2010
Springer
14 years 2 months ago
A Formal Quantifier Elimination for Algebraically Closed Fields
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 ...
Cyril Cohen, Assia Mahboubi
CASC
2006
Springer
128views Mathematics» more  CASC 2006»
14 years 2 months ago
New Domains for Applied Quantifier Elimination
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...
Thomas Sturm
AISC
2004
Springer
14 years 2 months ago
Generic Hermitian Quantifier Elimination
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...
Andreas Dolzmann, Lorenz A. Gilch