Loading...
Please wait, while we are loading the content...
Similar Documents
Projective Quantifier Elimination for Equational Constraint Solving ?
| Content Provider | Semantic Scholar |
|---|---|
| Author | Álvez, Javier Hermo, Montserrat Lucio, Paqui |
| Copyright Year | 2014 |
| Abstract | We deal with (general) equational constraints, that is, firstorder formulas, with equality as its only predicate symbol, over a (finite or infinite) language L of function symbols. As semantic domain, we consider the algebra of finite terms over L. Solving one of such constraints means to find all the solutions for (i.e. assignments to) its free variables. We present the Projective Quantifier Elimination (PQE) technique for solving equational constraints (in particular, deciding their satisfiability) that performs an algebraic-style transformation of expressions instead of handling first-order formulas. PQE is formulated on the basis of three algebraic operations on expressions: complement, intersection and projection. We aim to contribute not only a new style of quantifier elimination for constraint solving, but also a more efficient method for equational constraint solving. PQE avoids unnecessary applications of the costly Explosion Rule (ER) that are performed by traditional solving methods. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.sc.ehu.es/jiwlucap/quantify14.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
