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...

• Type: Conference
• Year: 2008
• Where: CSCLP
• Authors: Khalil Djelloul
• Keywords: Artificial Intelligence, CSCLP 2008, Decision Procedure, Decomposable Theories, Functional Decomposable Theories