Sciweavers

Share
CSCLP
2008
Springer

An Efficient Decision Procedure for Functional Decomposable Theories Based on Dual Constraints

9 years 11 months ago
An Efficient Decision Procedure for Functional Decomposable Theories Based on Dual Constraints
Abstract. Over the last decade, first-order constraints have been efficiently used in the artificial intelligence world to model many kinds of complex problems such as: scheduling, resource allocation, computer graphics and bio-informatics. Recently, a new property called decomposability has been introduced and many first-order theories have been proved to be decomposable: finite or infinite trees, rational and real numbers, linear dense order,...etc. A decision procedure in the form of 5 rewriting rules has also been developed. It decides if a first-order formula without free variables (proposition) is true or not in any decomposable theory. Unfortunately, this later needs to normalize the initial proposition before starting the solving process. This transformation generates many nested negations and quantifications which greatly slow the performances of this decision procedure. We present in this paper an efficient decision procedure for functional decomposable theories, i.e. theorie...
Khalil Djelloul
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSCLP
Authors Khalil Djelloul
Comments (0)
books