SWSL includes two fundamentally distinct knowledge representation languages:
In this section, we discuss how -- and also why -- to combine knowledge expressed in SWSL-Rules with knowledge expressed in SWSL-FOL.
First, it is worthwhile to review the motivations for having the two distinct knowledge representation languages.
SWSL-Rules is especially well suited to represent available knowledge and desired patterns of reasoning for several tasks in semantic Web services:
In particular, the capabilities of SWSL-Rules for logical nonmonotonicity (negation-as-failure and/or Courteous prioritized conflict handling) is used heavily in many use case scenarios for each of the above tasks and the associated kinds of knowledge.
SWSL-FOL is especially well suited to represent available knowledge and desired patterns of reasoning for several other tasks in semantic Web services, especially revolving around the process model:
In particular, the capabilities of SWSL-FOL for disjunction, reasoning by cases, contrapositive reasoning, and/or existentials are used heavily in many use case scenarios for each of the above tasks and its associated kinds of knowledge.
SWSL-Rules and SWSL-FOL overlap largely in syntax, and SWSL-Rules includes almost all of the connectives of SWSL-FOL. The deeper issue, however, is the semantic relationship between SWSL-Rules and SWSL-FOL.
For several purposes it is desirable to combine knowledge expressed in the SWSL-Rules form with knowledge expressed in the SWSL-FOL form. One important such purpose is:
For example, the predicates might be classes or properties defined via OWL-DL axioms, i.e., expressed in the Description Logic fragment of FOL.
In terms of semantics, it is desirable to have reasoning in SWSL-Rules respect as much as possible the information contained in such background FOL ontologies. In particular, it is desirable to enable sufficient completeness in the semantic combination to ensure that the conclusions drawn in SWSL-Rules will be (classically) not inconsistent with the SWSL-FOL ontologies.
Ideally, there would be one well-understood overall knowledge representation formalism that subsumes both SWSL-Rules and SWSL-FOL. This would provide the general theoretical basis for combining arbitrary SWSL-Rules knowledge with arbitrary SWSL-FOL knowledge. Unfortunately, finding such an umbrella formalism is still an open issue for basic research. Instead, the current scientific understanding provides only a limited theoretical basis for combining SWSL-Rules knowledge with SWSL-FOL knowledge. On the bright side, there are limited expressive cases for which it is well-understood theoretically how to do such combination.
The Venn diagram of relationships between the different formalisms, given in Figure 2.1 illustrates the most salient aspects of the current scientific understanding.
Figure 2.1: The relationships among different formalisms
The shield shape represents first-order logic-based formalisms. The (diagonally-rotated) bread-slice shape shows the expressivity of the logic programming based paradigms. These overlap partially -- in the Horn rules subset. FOL includes expressiveness beyond the overlap, notably: positive disjunctions; existentials; and entailment of non-ground and non-atomic conclusions. Likewise, LP includes expressiveness beyond the overlap, such as negation-as-failure, which is logically nonmonotonic. Description Logic (cf. OWL-DL), depicted as an oval shape, is a fragment of FOL.
Horn FOL is another fragment of FOL. Horn LP is a slight weakening of Horn FOL. "Weakening" here means that the conclusions from a given set of Horn premises that are entailed according to the Horn LP formalism are a subset of the conclusions entailed (from that same set of premises) according to the Horn FOL formalism. However, the set of ground atomic conclusions is the same in the Horn LP as in the Horn FOL. For most practical purposes (e.g., relational database query answering), Horn LP is thus essentially similar in its power to the Horn FOL.
Horn LP is a fragment of both FOL and nonmonotonic LP -- i.e., of both SWSL-Rules and SWSL-FOL. Horn LP is thus a limited "bridge" that provides a way to pass information -- either premises, or ground-atomic conclusions -- from FOL to LP, or vice versa. Knowledge from FOL that is in the Horn LP subset of expressiveness can be easily combined with general LP knowledge. Vice versa, knowledge from LP that is in the Horn LP subset of expressiveness can be easily combined with general FOL knowledge. Description Logic Programs (DLP) [Grosof2003a] represent a fragment of Horn LP. It likewise acts as a "bridge" between Description Logic (i.e., OWL-DL) and LP.
Note that, technically, LP uses a different logical connective for implication (":-" in SWSL syntax) than FOL uses. When we speak of Horn LP as a fragment of FOL, we are viewing this LP implication connective as mapped into the FOL implication connective (also known as material implication).
Horn LP as "bridge". To summarize, there is some initial good news about semantic combination:
Builtin predicates. Another case of well behaved semantic combination is for builtin predicates that are purely informational, e.g., that represent arithmetic comparisons or operations such as less-than or multiplication. Technically, in LP these can be viewed as procedural attachments. But alternatively, they can be viewed as predicates that have fixed extensions. Their semantics in both FOL and LP can thus be viewed essentially as virtual knowledge base consisting of a set of ground facts. This thus falls into the Horn LP fragment.
Hypermonotonic reasoning as "bridge". Recently, a new theoretical approach called hypermonotonic reasoning [Grosof2004c] has been developed to enable a case of "bridging" between (nonmon) LP and FOL that is considerably more expressive than Horn LP.
We will now describe in more detail some preliminary results about this hypermonotonic reasoning approach that bear upon the relationship of LP to FOL and thus upon how to combine LP knowledge with FOL knowledge.
Courteous LP (including its fragment: LP with negation-as-failure) can be viewed as a weakening of FOL, under a simple mapping of Courteous LP rules/conclusions into FOL. "Weakening" here means that for a given set of premises, the set of conclusions entailed in the Courteous LP formalism is in general a subset of the set of conclusions entailed by the FOL formalism. In other words:
This fundamental relationship between the formalisms provides an augmentation to the theoretical basis for combining knowledge in LP (i.e., SWSL-Rules) with knowledge in FOL.
Consider a set of rules S in LP and a set of formulas B in FOL. Let T be a translation mapping from the language of S to the language of B. S is said to be hypermonotonic with respect to B and T when S is sound but incomplete relative to B, under the mapping T. That is, when the conclusions entailed in S from a given set of premises P are in general always a subset of the conclusions entailed in B from the translated premises of S.
Define CLP2 to be the fragment of the Courteous LP formalism in which explicit negation-as-failure is omitted (i.e., prohibited). Each rule and mutex in CLP2 can be mapped quite straightforwardly and intuitively to a clause in FOL: simply replace the LP implication connective (":-" in SWSL-Rules syntax) by the FOL implication connective. Observe that this is the same mapping/translation that was considered in relating the Horn LP to FOL. Each ground-literal conclusion in CLP2 can also be mapped, in the same fashion, into a ground-literal in FOL.
The restriction on Courteous LP to avoid explicit negation-as-failure is not very onerous essentially, since the great majority of use cases in which explicit negation-as-failure is employed can be reformulated during manual authoring of rules so as to avoid it as a construct. More generally, the mapping can be extended, by complicating it a bit, to permit explicit negation-as-failure.
Going in the reverse direction, every clause in FOL can also be mapped into CLP2, in such a way that the resulting CLP information is a weakening of the FOL clause that nevertheless preserves much of the strength of the FOL clause. This reverse-translation mapping from FOL to CLP is complicated somewhat by the directional nature of the LP implication connective. "Directional" here means having a direction from body towards head. Each LP rule can be viewed as a directed clause. Consider a FOL clause C that consists of a disjunction of m literals:
Here, each Li is an atom or a classically-negated atom. When mapping c to CLP2, there are m possible choices of one for each possible choice of which literal is to be made head of the LP rule. Each possible choice corresponds to a different rule -- the LP rule in which literal Li is chosen as head has the form:
Li :- neg L1, ..., neg Li-1, neg Li+1, ..., neg Lm .
Altogether, the FOL clause C is mapped into a set of m LP rules:
L1 :- neg L2, neg L3, ..., neg Lm .
L2 :- neg L1, neg L3, ..., neg Lm .
Lm :- neg L1, neg L2, ..., neg Lm-1 .
where neg (neg A) is replaced equivalently by A. This set of rules is called the "omni-directional" set of rules for that clause -- or, more briefly, the "omni rules" for that clause.
In general, FOL axioms need not be clausal since they may include existential quantifiers. However, often skolemization can be performed to represent such existentials in a manner that preserves soundness (as is usual for skolemization). A refinement of the reverse translation mapping above is to exploit such skolemization in order to relax the requirement of clausal form. We use such skolemization particularly for head existentials.
Automatic weakened translation of FOL ontologies into SWSL-Rules. In the ontologies aspect of SWSL, it is desirable to have a "bridging" technique to automatically translate FOL ontologies into SWSL-Rules in such a manner as to preserve soundness (from an FOL viewpoint) but to be nevertheless fairly strong (i.e., capture much of the strength/content of the original FOL axioms). We have adopted, as an experimental "bridging" approach, the reverse translation mapping technique described above in order to map FOL ontologies into SWSL-Rules (heavily using the Courteous feature). In particular, we have applied this technique to map the axioms of PSL Core and Outer Core into SWSL-Rules so as to create a weakened version of that ontology that can be utilized within SWSL-Rules. Because some of these PSL axioms include existentials, we utilize the skolemization refinement described above, particularly for head existentials. The mapping from the PSL axioms to SWSL-Rules is given in appendix PSL in SWSL-FOL and SWSL-Rules.
The precise algorithm used to obtain the SWSL-Rules translation for a given axiom in SWSL-FOL is as follows:
Input: a formula F in SWSL-FOL. Output: a set of rules R, expressed in SWSL-Rules. 1) Translate F into formula F1 in Prenex Normal Form. 2) Skolemize F1 to get F2, which is in Skolem Normal Form. 3) Write F2 as a set S of clauses. 4) For each clause C in S, produce the omnidirectional set of rules for C (as defined above). R then is the union of all the omnidirectional sets of rules produced by (4).