Foundations of Semantic Web Technologies

372 Foundations of Semantic Web Technologies

THEOREM C.3

If T = {F

1

, . . . , F

n

} is a theory and F a formula, then T |= F if and only if

(F

1

∧ · · · ∧ F

n

) ∧ ¬F is unsatisfiable.

First-order predicate logic is monotonic in the following formal sense.

THEOREM C.4

Let T and S be two theories over the same first-order language and let T ⊆ S.

Then {F | T |= F } ⊆ {F | S |= F }.

There exist alternative logics, i.e. logics stemming from logic programming,

or logics stemming from attempts to model “common sense” in artificial intel-

ligence, which are non-monotonic in the sense that statements like that from

Theorem C.4 do not hold for them.

Closely related to monotonicity is the n otion of Open World Assumption

(OWA). However, the OWA is an informal notion and