This paper is about the integration in a unique formalism of knowledge representation languages such as those provided by description logic languages and rule-based reasoning paradigms such as those provided by logic programming languages. We aim at creating an hybrid formalism where description logics constructs are used for defining concepts that are given as arguments to the predicates of the logic programs.
Examining role-based access control and organization-based access control, we present a case study motivating the combination of logic programming with description logics that we are seeking for. Access of subjects to objects in a computer system are permitted in accordance with a security policy embodied in an access control database. Many computer systems use the access control matrix model to represent security policies [31]. Formally, an access control matrix is a structure consisting of a set of subjects (users, processes, etc), a set of objects (files, tables, etc) and binary relations ()∈ between objects and subjects giving to subjects permissions to access objects. In this setting, asserting that subject possesses permission on object comes down to asserting that holds for and .
Access control with a lot of subjects is space-consuming. To reduce the cost of
security, within the context of role-based access control (RBAC), it has been proposed that
access control administrators treat sets of subjects as instances of a concept called role1 [38].
Formally, an RBAC-structure consists of a set of subjects, a set of objects, a set of roles,
a binary relation between subjects and roles defining the roles of subjects and binary
relations ()∈ between objects and roles giving to roles permissions to access objects. In
this setting, asserting that subject has role comes down to asserting that holds for
and , whereas asserting that role possesses permission on object comes down to
asserting that holds for and . It is possible to refine the RBAC model by including
the concept of role hierarchy which allows permissions to be inherited through it. This
hierarchy is specified by means of assertions of the form ′⊑′′ where ′ and ′′ are roles.
To put it simply, the idea behind RBAC is the following: in a computer system, subject
possesses a permission on object if and only if there are roles 0, . . . , such that holds
for and 0, for all positive integers ≤ , − 1⊑ has been asserted and holds for and .
RBAC with a lot of objects is space-consuming. To reduce the cost of security, within
the context of organization-based access control (OrBAC), it has been proposed that RBAC
administrators treat sets of objects as instances of a concept called view [
Finally, it is also a great pity that neither RBAC, nor OrBAC allow conditional
assertions of the form (, )← (′, ′). By using conditional assertions of that form, one
may more succinctly define more precise access control policies. For instance, to say that
subjects having the role possess a permission on objects having the view if subjects
having the role ′ possess a permission on objects having the view ′, one can simply
say that (, )← (′, ′). This is particularly interesting when does not denote
a permission, but an obligation corresponding to the permission denoted by 2. In that
case, a conditional assertion like (, )← (, ) expresses the deontic rule saying
that subjects having the role possess the permission on objects having the view if
subjects having the role possess the corresponding obligation on objects having the view .
Knowledge representation languages such as those provided by description logic
languages [
Let VAR be a countable set of variable concepts (with typical members denoted , , etc). Let CON be a countable set of constant concepts (with typical members denoted , , etc) and 2We are assuming the deontic principle saying that permissions are implied by their corresponding obligations [37]. ROL be a countable set of constant roles (with typical members denoted , , etc). The set of complex concepts (with typical members denoted , , etc) is defined by the rule 3 • ::= | | ⊤ | (⊓) | ∃., where ranges over VAR, ranges over CON and ranges over ROL. We adopt standard rules for omission of the parentheses. A complex concept is VAR-free if contains no occurrence of a variable concept. A complex concept is ROL-free if contains no occurrence of a constant role. For all ∈N, the concept construct (∃.) is inductively defined as follows for each ∈ROL: • if =0 then (∃.)::=, • otherwise, (∃.)::=∃.(∃.)− 1.
A substitution is a function from VAR to the set of all complex concepts equal to the identity
function on a cofinite subset of VAR [
Concept inclusions are expressions of the form ⊑ (read “ is contained in ”) for all complex concepts , . Concept equations are expressions of the form = (read “ is equal to ”) for all complex concepts , .
Let PRE be a countable set of predicate symbols (with typical members denoted , , etc). For all ∈PRE, let ar() be the arity of . An atom is an expression of the form (1, . . . , ar()) (read “ holds for 1, . . ., ar()”) where is a predicate symbol and 1, . . ., ar() are complex concepts. Clauses are expressions of the form 1, . . . , ← 1, . . . , (read “if 1, . . ., then either 1, . . ., or ”) where 1, . . ., , 1, . . ., are atoms. Definite clauses are clauses of the form ← 1, . . . , , unit clauses are clauses of the form ← and definite goals are clauses of the form ← 1, . . . , .
Let IND be a countable set of individual constants (with typical members denoted , , etc).
A concept assertion is an expression of the form : (read “ belongs to ”) where is a
VAR-free complex concept and is an individual constant. A role assertion is an expression
of the form :(, ) (read “ is -related to ”) where ∈ROL and and are individual
constants.
3The set of complex concepts we define here is the one of description logic ℰℒ [
A T-box is a finite set of concept inclusions and concept equations. A program is a finite set of clauses. An A-box is a finite set of concept assertions and role assertions. A deductive ontology is a triple ( , Π , ) consisting of a T-box , a program Π and an A-box .
We introduce the semantics of our hybrid formalism4.
The semantics is defined in terms of frames, i.e. structures (, , ) where is a nonempty set, : CON →− ( ) and : ROL →− ( × ). In a frame (, , ), for all ∈ROL, • the -image of a subset of is the set of all ∈ such that there exists ∈ such that ()(, ), • the -pre-image of a subset of is the set of all ∈ such that there exists ∈ such that ()(, ), • the domain of is the set of all ∈ such that there exists ∈ such that ()(, ), • the range of is the set of all ∈ such that there exists ∈ such that ()(, ). Obviously, in a frame (, , ), for all ∈ROL, the domain of is the -pre-image of and the range of is the -image of . A var-interpretation on a frame (, , ) is a function : VAR →− ( ). For all frames (, , ), the value of the complex concept with respect to a var-interpretation on (, , ) is the subset ‖‖ of defined by • ‖‖ = (), • ‖‖ =(), • ‖⊤‖ = , • ‖⊓‖ =‖‖ ∩ ‖‖ , • ‖∃.‖ ={ ∈ : there exists ∈ such that ()(, ) and ∈‖‖ }. Obviously, ‖‖ does not depend on when is VAR-free. In that case, ‖‖ will be denoted ‖‖.
A pre-interpretation on a frame (, , ) is a function : PRE →− (( )⋆) such that for all ∈PRE, ()⊆ ( )ar(). For all frames (, , ) and for all pre-interpretations on (, , ), the value of an atom (1, . . . , ar()) with respect to a var-interpretation on (, , ) is the element |(1, . . . , ar())| in {0, 1} such that • if () contains (‖1‖ , . . . , ‖ar()‖ ) then |(1, . . . , ar())| =1, • otherwise, |(1, . . . , ar())| =0. 4In this paper, for all sets , () denotes the set of all subsets of , ⋆ denotes the set of all tuples of elements of and for all ∈N, denotes the set of all -tuples of elements of .
An ind-interpretation on a frame (, , ) is a function : IND →− . For all frames (, , ) and for all ind-interpretations on (, , ), the value of a concept assertion : is the element |:| in {0, 1} such that • if ‖‖ contains () then |:|=1, • otherwise, |:|=0, • if () contains ((), ()) then |:(, )|=1, • otherwise, |:(, )|=0. and the value of a role assertion :(, ) is the element |:(, )| in {0, 1} such that
For all T-boxes , a -model (or a model of ) is a frame (, , ) such that for all varinterpretations on (, , ), • for all concept inclusions ⊑ in , ‖‖ ⊆‖ ‖ , • for all concept equations = in , ‖‖ =‖‖ .
| 1| =1, . . ., or | | =1, • for all concept assertions : in , |:|=1, • for all role assertions :(, ) in , |:(, )|=1.
For all deductive ontologies ( , Π , ), a ( , Π , )-model (or a model of ( , Π , )) is a structure (, , , , ) consisting of a -model (, , ), a pre-interpretation on (, , ) and an ind-interpretation on (, , ) such that for all var-interpretations on (, , ),
• for all clauses 1, . . . , ← 1, . . . , in Π , if | 1| =1, . . ., | | =1 then either Notice that in a model (, , , , ) of a deductive ontology ( , Π , ), for all varinterpretations on (, , ), • for all definite clauses ← 1, . . . , in Π , if | 1| =1, . . ., | | =1 then | | =1, • for all unit clauses ← in Π , | | =1, • for all definite goals ← 1, . . . , in Π , either | 1| =0, . . ., or | | =0.
Although of limited expressive power, concept constructs can be used for
characterizing classes of frames. As observed by [
Within our setting, elementary conditions — like “() is serial”, “() is empty”, etc — are ifrst-order conditions that can be expressed as sentences in a function-free first-order language with equality based on a set of unary predicate symbols in one-to-one correspondence with CON and a set of binary predicate symbols in one-to-one correspondence with ROL. As a result, the following decision problems are of interest: — deciding elementary definability (DED): given a T-box , determine whether there exists an elementary condition such that for all frames (, , ), holds in (, , ) if and only if (, , ) is a model of , — deciding concept definability (DCD): given an elementary condition , determine whether there exists a T-box such that for all frames (, , ), (, , ) is a model of if and only if holds in (, , ), — deciding elementary equivalence (DEE): given a T-box and an elementary condition , determine whether for all frames (, , ), (, , ) is a model of if and only if holds in (, , ).
DED, DCD and DEE stem from the corresponding definability problems in modal logics [
We present decision problems about concept inclusions and concept equations. Let be a T-box.
A concept inclusion ⊑ is a logical consequence of (denoted |=⊑) if for all -models (, , ) and for all var-interpretations on (, , ), ‖‖ ⊆‖ ‖ . A concept equation = is a logical consequence of (denoted |==) if for all -models (, , ) and for all var-interpretations on (, , ), ‖‖ =‖‖ . As a result, the following decision problems are of interest: — deciding concept inclusions (DCI): given a concept inclusion ⊑, determine whether |=⊑, — deciding concept equations (DCE): given a concept equation =, determine whether |==.
If is VAR-free then DCI and DCE are in P [
We present decision problems about logical consequences and correct answers. Let ( , Π , ) be a deductive ontology.
A clause 1, . . . , ← 1, . . . , is a logical consequence of ( , Π , ) (denoted ( , Π , )|= 1, . . . , ← 1, . . . , ) if for all ( , Π , )-models (, , , , ) and for all var-interpretations on (, , ), if | 1| =1, . . ., | | =1 then either | 1| =1, . . ., or | | =1. Notice that a definite clause ← 1, . . . , is a logical consequence of ( , Π , ) if and only if for all ( , Π , )-models (, , , , ) and for all var-interpretations on (, , ), if | 1| =1, . . ., | | =1 then | | =1, a unit clause ← is a logical consequence of ( , Π , ) if and only if for all ( , Π , )-models (, , , , ) and for all var-interpretations on (, , ), | | =1 and a definite goal ← 1, . . . , is a logical consequence of ( , Π , ) if and only if for all ( , Π , )-models (, , , , ) and for all var-interpretations on (, , ), either | 1| =0, . . ., or | | =0. As a result, the following decision problems are of interest: — deciding definite clauses (DDC): given a definite clause ← 1, . . . , , determine whether ( , Π , )|= ← 1, . . . , , — deciding unit clauses (DUC): given
( , Π , )|= ← ,
10See [
a unit clause ← , determine whether — deciding definite goals (DDG): given a definite goal ← 1, . . . , , determine whether ( , Π , )|=← 1, . . . , .
A substitution is a correct answer for the definite goal ← 1, . . . , with respect to ( , Π , ) if for all ( , Π , )-models (, , , , ) and for all var-interpretations on (, , ), | ( 1)| =1, . . ., | ( )| =1. As a result, the following decision problem is of interest: — deciding correct answers (DCA): given a definite goal ← 1, . . . , , determine whether there exists a correct answer for ← 1, . . . , with respect to ( , Π , ).
DDC, DUC, DDG and DCA stem from the corresponding derivability problems in logic programming [26, 34]. It is not known whether DDC, DUC, DDG and DCA are decidable11.
We present a research program. As can be seen from its presentation, this research program
covers diferent aspects of description logics and logic programming: recursion theory with
(RP1), computational complexity with (RP2), model theory and fixpoint theory with (RP3),
automated deduction with (RP4) and non-monotonic reasoning with (RP5). Needless to say,
to carry out it, one must neither work in isolation, nor lose sight of the possible applications of
the hybrid formalism developed in this paper. In other respect, with respect to expressivity, one
must also compare this formalism to the main approaches proposed so far. These approaches
include the above-mentioned hybrid knowledge bases [
Our hybrid formalism can be seen as a programming language. It is not known whether it is Turing-complete. When description logic ℒ is considered instead of description logic ℰ ℒ, the Turing-completeness of our hybrid formalism can be easily proved by means of a reduction from the Turing-completeness of Minsky machines. Hence, the following item in our research program: (RP1) separate the description logics that do give rise to a Turing-complete hybrid formalism from the description logics that do not. In particular, find simple and natural conditions on concept inclusions, concept equations and clauses such that deductive ontologies satisfying them give rise to a Turing-complete hybrid formalism.
The success of the logic programming languages comes from the fact that it is relatively easy to
define Turing-incomplete restrictions of clauses that can be used as a domain-specific language
taking advantage of eficient algorithms developed for them [
In logic programming, the declarative semantics of programs is given by the usual semantics of first-order logic. It is defined in terms of Herbrand interpretations [ 26, 34]. In this setting, given a program, the main result is the standard characterization of its Herbrand models as the pre-fixpoints of some continuous mapping associated to it. Consequently, the following item in our research program: (RP3) develop the declarative and fixpoint semantics of our hybrid formalism. In particular, given a deductive ontology, characterize its Herbrand models as the pre-fixpoints of some continuous mapping associated to it.
In logic programming, the refutation procedure of interest is called SLD-resolution where an
inference step is based on the unifiability between the selected atom in a given definite goal
and the left side of a variant of a definite clause in a given program. Hence, the following item
in our research program: (RP4) develop the procedural semantics of our hybrid formalism. In
particular, considering the unification problem in description logics with empty T-boxes [
By using conditional assertions of the form 1, . . . , ← 1, . . . , , not( 1), . . . , not( ) where 1, . . ., , 1, . . ., , 1, . . ., are atoms, one may write more expressive deductive ontologies. For instance, in our example about security policies, the deontic principle saying that every non-prohibited access is permitted and the deontic principle saying that every non-compulsory access is optional can be expressed by the following conditional assertions: • perm(, )← not(proh(, )), • opti(, )← not(comp(, )).
In logic programming, the declarative semantics of a program containing, possibly, negation in
the right side of clauses is given by the so-called answer set semantics. It is defined in terms
of stable models [
Our idea of an hybrid formalism where description logics constructs are used for defining
concepts that are given as arguments to the predicates of the logic programs has only one
ancestor: the formalism developed in [
Special acknowledgement is heartily granted to Stéphane Demri, Esra Erdem, Luis Fariñas del Cerro, Andreas Herzig, Rosalie Iemhof, George Metcalfe, Mojtaba Mojtahedi, Linh Anh Nguyen, Christophe Ringeissen, Maryam Rostamigiv, Renate Schmidt and Tinko Tinchev for their feedback. We also make a point of strongly thanking the referees for their useful suggestions. programming with description logics for the semantic web’. Artificial Intelligence 172 (2011) 1495–1539. [24] Eiter, T., Ianni, G., Lukasiewicz, T., Schindlauer, R. ‘Well-founded semantics for description logic programs in the semantic web’. ACM Transactions on Computational Logic 12 (2011) article 11. [25] Erdem, E. Theory and Applications of Answer Set Programming. Doctoral thesis of the
University of Texas at Austin (2002). [26] Gabbay, D., Hogger, C., Robinson, J. Handbook of Logic in Artificial Intelligence and Logic
Programming. Volume 5: Logic Programming. Oxford University Press (1998). [27] Gencer, Ç. ‘Description of modal logics inheriting admissible rules for K4’. Logic Journal of the IGPL 10 (2002) 401–411. [28] Gencer, Ç., de Jongh, D. ‘Unification in extensions of K4’. Logic Journal of the IGPL 17 (2009) 159–172. [29] Gottlob, G., Papadimitriou, C. ‘On the complexity of single-rules datalog queries’. Information and Computation 183 (2003) 104–122. [30] Grosof, B., Horrocks, I., Volz, R., Decker, S. ‘Description logic programs: combining logic programs with description logic’. In: Proceedings of the 12th International Conference on World Wide Web. ACM (2003) 48–57. [31] Lampson, B. ‘Protection’. Operating Systems Review 8 (1974) 18–24. [32] Levy, A., Rousset, M.-C. ‘Combining Horn rules and description logics in CARIN’. Artificial
Intelligence 104 (1998) 165–209. [33] Lifschitz, V. ‘What is answer set programming’. In: Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence. Association for the Advancement of Artificial Intelligence (2008) 1594–1597. [34] Lloyd, J. Foundations of Logic Programming. Springer (1987). [35] Motik, B., Rosati, R. ‘Reconciling description logics and rules’. Journal of the ACM 57 (2010) article 30. [36] Mugnier, M.-L., Thomazo, M. ‘An introduction to ontology-based query answering with existential rules’. In: Reasoning Web. Springer (2014) 245–278. [37] Parent, X., van der Torre, L. Introduction to Deontic Logic and Normative Systems. College
Publications (2018). [38] Sandhu, R., Coyne, E., Feinstein, H., Youman, C. ‘Role-based access control models’. IEEE
Computer 29 (1996) 38–47. [39] Schild, K. ‘A correspondence theory for terminological logics: preliminary report’. In: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence. Morgan Kaufmann (1991) 466–471. [40] Sofronie-Stokkermans, V. ‘On unification for bounded distributive lattices’. ACM Transactions on Computational Logic 8 (2007) article 12.