Concept Logics with Function Symbols

Hans-Jürgen Bürckert; Bernhard Hollunder; Armin Laux

In: Anthony G. Cohn (Hrsg.). Proceedings of the 11th European Conference on Artificial Intelligence. European Conference on Artificial Intelligence (ECAI-94), 11th, August 8-12, Amsterdam, Netherlands, Pages 406-410, J. Wiley, 1994.


Recently, concept logics have been proposed which allow one to incorporate algorithms for domain specific problem solving into the classical resolution principle. The domain specific knowledge can be expressed by using the (KL-ONE like) knowledge representation language ALC, and problems are encoded by sets of so-called constrained clauses. Testing satisfiability and validity of the thereby used ALC-constraints are decidable. In this paper we will show that things become much more complex if problems are given as sets of formulas with restricted quantifiers. The reason for this is due to the fact that in general Skolem function symbols are introduced when translating formulas with restricted quantifiers into constrained clauses. While satisfiability of ALC-constraints with function symbols is decidable, validity of such constraints turns out to be undecidable.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence