Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-25T04:07:33.827Z Has data issue: false hasContentIssue false
  • English
  • Français

Decomposable theories

Published online by Cambridge University Press:  01 September 2007

KHALIL DJELLOUL
KHALIL DJELLOUL*
Affiliation:
Parc scientifique et technologique de Luminy, Laboratoire d'Informatique Fondamentale de Marseille, 163 avenue de Luminy - Case 901, 13288 Marseille, cedex 9, France (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We present in this paper a general algorithm for solving first-order formulas in particular theories called decomposable theories. First of all, using special quantifiers, we give a formal characterization of decomposable theories and show some of their properties. Then, we present a general algorithm for solving first-order formulas in any decomposable theory T. The algorithm is given in the form of five rewriting rules. It transforms a first-order formula ϕ, which can possibly contain free variables, into a conjunction φ of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if ϕ has no free variables then φ is either the formula true or ¬true. The correctness of our algorithm proves the completeness of the decomposable theories. Finally, we show that the theory of finite or infinite trees is a decomposable theory and give some benchmarks realized by an implementation of our algorithm, solving formulas on two-partner games in with more than 160 nested alternated quantifiers.

Keywords

Logical first-order formulaComplete theoryRewriting rulesTheory of trees
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 7 , Issue 5 , September 2007 , pp. 583 - 632
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Benhamou, F., Colmerauer, A., Garetta, H., Pasero, R. and Van-caneghem, M. 1996. Le manuel de Prolog IV. PrologIA, Marseille, France.Google Scholar
Burckert, H. 1988. Solving disequations in equational theories. In Proceeding of the 9th Conference on Automated Deduction, LNCS 310, pp. 517–526, Springer-Verlag.CrossRefGoogle Scholar
Clark, K. L. 1978. Negation as failure. In Logic and Data bases. Ed Gallaire, H. and Minker, Plenum.Google Scholar
Colmerauer, A. 1982. Prolog and infinite trees. In: Clark, K. L. and Tarnlund, S.-A., editors, Logic Programming. Academic Press. pp. 231–251.Google Scholar
Colmerauer, A. 1984. Equations and inequations on finite and infinite trees. Proceeding of the International Conference on the Fifth Generation of Computer Systems, pp. 85–99.Google Scholar
Colmerauer, A. 1990. An introduction to Prolog III. Comm. ACM, 33 (7): 68–90.Google Scholar
Colmerauer, A. and Dao, T. 2003. Expressiveness of full first-order formulas in the algebra of finite or infinite trees, Constraints, 8 (3): 283–302.CrossRefGoogle Scholar
Comon, H. 1988. Unification et disunification: Theorie et applications. PhD thesis, Institut National Polytechnique de Grenoble.Google Scholar
Comon, H. and Lescanne, P. 1989. Equational problems and disunification. J. Symbolic Computation, 7: 371–425.CrossRefGoogle Scholar
Comon, H. 1991. Disunification: a survey. In: Lassez, J. L. and Plotkin, G., editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press.Google Scholar
Comon, H. 1991. Resolution de contraintes dans des algebres de termes. Rapport d'Habilitation, Universite de Paris Sud.Google Scholar
Courcelle, B. 1983. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 25 (2): 95–169.CrossRefGoogle Scholar
Courcelle, B. 1986. Equivalences and Transformations of Regular Systems applications to Program Schemes and Grammars. Theoretical Computer Science, 42: 100–122.CrossRefGoogle Scholar
Dao, T. 2000. Resolution de contraintes du premier ordre dans la theorie des arbres finis ou infinis. These d'informatique, Universite de la mediterranee, France.Google Scholar
Djelloul, K. 2005a. Complete first-order axiomatization of the construction of trees on an ordered set. Proceedings of the 2005 International Conference on Foundations of Computer Science (FCS'05), CSREA Press, pp. 87–93.Google Scholar
Djelloul, K. 2005b. About the combination of trees and rational numbers in a complete first-order theory. Proceeding of the 5th International conference on frontiers of combining systems FroCoS 2005, Springer Lecture Notes in Artificial Intelligence, vol 3717 pp. 106–122.Google Scholar
Djelloul, K. and Dao, T. 2006a. Solving First-Order formulas in the Theory of Finite or Infinite Trees: Introduction to the Decomposable Theories. Proceeding of the 21st ACM Symposium on Applied Computing (SAC). ACM press (to appear).Google Scholar
Djelloul, K. and Dao, T. 2006b. Complete first-order axiomatization of the M-extended trees. Proceeding of the 20th Workshop on (constraint) Logic Programming (WLP06). INFSYS Research Report 1843-06-02, pp. 111–119.Google Scholar
Fruehwirth, T. and Abdelnnadher, S. 2002. Essentials of Constraints Programming. Springer Cognitive technologies.Google Scholar
Huet, G. 1976. Resolution d'equations dans les langages d'ordre 1, 2,. . .ω. These d'Etat, Universite Paris 7. France.Google Scholar
Jaffar, J. 1984. Efficient unification over infinite terms. New Generation Computing, 2 (3): 207–219.CrossRefGoogle Scholar
John, E. and Ullman, D. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley.Google Scholar
Kunen, K. 1987. Negation in logic programming. J. Logic Program. 4: 289–308.CrossRefGoogle Scholar
Lyndon, R. C. 1964. Notes on Logic. Van Nostrand Mathematical studies.Google Scholar
Maher, M. 1988. Complete axiomatization of the algebra of finite, rational and infinite trees. Technical report, IBM T.J.Watson Research Center.Google Scholar
Malcev, A. 1971. Axiomatizable classes of locally free algebras of various types. In: Wells, B. III, editor, The Metamathematics of Algebraic Systems. Anatolii Ivanovic Malcev. Collected Papers: 1936–1967, volume 66, chapter 23, pp. 262–281.Google Scholar
Matelli, A. and Montanari, U. 1982. An efficient unification algorithm. ACM Trans. Lang. Syst. 4 (2): 258–282.CrossRefGoogle Scholar
Paterson, M. and Wegman, N. 1978. Linear unification. J. Computer and Systems Science, 16: 158–167.CrossRefGoogle Scholar
Ramachandran, V. and Van Hentenryck, P. 1993. Incremental algorithms for formula solving and entailment over rational trees. Proceeding of the 13th Conference Foundations of Software Technology and Theoretical Computer Science, LNCS volume 761, pp. 205–217.CrossRefGoogle Scholar
Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM, 12 (1): 23–41.CrossRefGoogle Scholar
Rybina, T. and Voronkov, A. 2001. A decision procedure for term algebras with queues. ACM Trans. Computational Logic, 2 (2): 155–181.Google Scholar
Smith, A. 1991. Constraint operations for CLP. Logic Programming: Proceedings of the 8th International Conference, Paris. pp. 760–774.Google Scholar
Vorobyov, S. 1996. An Improved Lower Bound for the Elementary Theories of Trees. Proceeding of the 13th International Conference on Automated Deduction (CADE'96). Springer Lecture Notes in Artificial Intelligence, vol 1104, pp. 275–287.CrossRefGoogle Scholar