Propositional Logic as Set Description Language

Used for the Semantic Web.

Let $PL_{DL}^0$ be given by the following grammar for concepts:

So we have:

• atomics
• Concept intersection (and)
• concept complement (negation)
• concept union (or)
• concept subsumption (implication)
• concept equality (equivalence)

We can use all of our propositional identities that we already proved for Propositional Logic:

So we can actually compute with these.

And we are able to translate back to Propositional Logic and then over to First-Order Predicate Logic:

→ Translation into First-Order Predicate Logic

Examples for this