known to be married is to be assumed to be non-married, that those **who are known** to be high-risk should have a surcharge, and that those that have **a known spouse**
should have a discount:

## K Nonm Arried(X) ← K Person(X), Not **Married**(X).

K surcharge(X) ← K highRisk(X), K **person**(X).

K discount(X) ← K spouse(X, Y ), K person(X), K **person**(Y ).

Note that *married* and *nonMarried* **are defined both by axioms in the ontology**
and by rules. Within the rule bodies, literals with the K or not **operators (e.g.**
K highRisk(X**)) may require information both from the ontology and from other**
rules; other literals are proven directly by the other rules (e.g. *person(X)*). Intuitively, Kϕ stands for "ϕ is known to be true", whereas not ϕ stands for "ϕ **is not**
known to be true".

Suppose *person(john)* **were added as a fact (in the rule base). Under closedworld negation, the first rule would derive** *nonMarried(john)***. By the first ontology**
axiom, ¬*married(john)* **would hold, and by the second axiom** *highRisk(john)* **would**
also hold. By the last rule, surcharge(john**) would hold as well. Thus the proof**
of surcharge(john**) involves interdependencies between the rules with closed-world** negation, and the ontology with open-world negation. At the same time the proof of surcharge(john**) is** *relevant* **in the sense that properties of other individuals, not** related to john **either through rules nor axioms in the ontology, do not need to be**
considered.

Now suppose that one learns that a person named Bill has a spouse, **and that**
Bob is the spouse of Ann. This can be formalized by adding the corresponding facts for the predicate person, the fact spouse(bob, ann) and the DL assertion **bill** : ∃Spouse.⊤**. In this case one would expect that neither Bill nor Bob are considered**
high risk, and so should not have a surcharge; and that since Bob (contrary to Bill) has a known spouse, he should have a discount. This is in fact the result of MKNFW F S**. Note that, it is only possible to represent the difference between the**
situations of Bill and Bob by using the existential quantification of DL, something that is not possible in logic programming alone.

In the original definition of *MKNF*W F S**, the inter-dependencies of the ontology**
and rules were captured by a bottom-up fixed-point operator with **multiple levels** of iterations. Recently, a query-based approach to hybrid MKNF knowledge bases, called SLG(O**), has been developed using tabled resolution (Alferes et al. 2012).**
SLG(O) is sound and complete, as well as terminating for various classes of programs (e.g. datalog). In addition SLG(O**) is relevant in the sense of Example 2,**
i.e. in general one does not need to compute the whole model (for every object in the knowledge base) to answer a specific query. This relevancy is a critical requirement for scalability in numerous practical applications (e.g. in the area of Semantic Web): without relevance a query about a particular individual I **may need to derive**
information about other individuals even if those individuals were not connected to I through rules or axioms. This is also clear e.g. in the above mentioned case study