Logic Engineering (3)

Bijan Parsia

Beyond Propositional

• Propositional isn't very expressive
• No sub-sentential structure sensitivity
• Can't (sensibly) describe relations
• or relational structure
• Predicate logic adds
• N-ary predicates with variables
• Quantifers
• (Function terms)
• But is only semi-decidable
• And hard to reason with
• And "too expressive" (hard to work with)

Two Motivations

• Databasey
• Relational database
• Reduce the connectives
• Add n-ary predications (relations)
• Either ground or universally quantified
• (Fairly) tractable
• Extend to Horn clauses
• Datalog!
• Conceptual Modeling
• ER diagrams
• Unary and Binary predicates
• Allow for incomplete knowledge
• Ontology languages!

Description Logics

• Emphasis on tractability
• Goes back to the foundation
• Largely abandoned in the mid-90s
• Big resurgence in the past few years
• Must be sub-boolean (i.e., not contain propositional logic)
• Emphasis on expressiveness
• Decidable and "practible"
• All include propositional logic over unary predicates
• Base logic: ALC
• "Attribute logic with complement"

ALC

• Unary and Binary predicates
• Can be ground! (ABox statements)\[mary:Person, <sarah, mary>:loves\]
• Concept expression language
• With constructors:\[\sqcup, \sqcap, \neg, \exists, \forall\]
• (Man. Syntax: or, and/that, not, some, only.)
• Note that this includes propositional logic!
• These constructors can be combined aribtrarily, but always have just one variable free
• Axioms
• Facts (ground concept expressions and binary predicates)
• Universally quantified conditionals (and biconditionals)

Grammar

• For <Con, Roles, Ind>, let A \in Con, P \in Roles, a,b \in Ind, and C, D be arbitrary concept expressions:
• A | \neg C |
• C \sqcup D | C \sqcap D |
• \forall P.C | \exists P.C
• Facts (ABox statements):
• a:C
• <a, b>:P
• Axioms (TBox)
• A \equiv C
• (But A appears only once on the LHS and does appear directly or indirectly on the RHS of its definition)
• Such TBoxes are definitorial (rather a subset of the definitorial ones)
• Notice the variable free syntax!

Correspondances

• We can translate to binary FOL with at most two distinct variables:
• In what follows: var = x or y; var' = x if var=y and y if var=x

• DL	FOL
  A	A(var)
  \neg C	\neg (Tr(C, var))
  C \sqcap D	Tr(C, var) \land Tr(D, var)
  C \sqcup D	Tr(C, var) \lor Tr(D, var)
  P	Tr(P, var, var)
  \forall P.C	\forall(var')(Tr(P(var, var') \rightarrow Tr(C, var'))
  \exists P.C	\exists(var')(Tr(P(var, var') \land Tr(C, var'))
  a:C, <a, b>:P	C(a), P(a,b)
  A \equiv C	\forall(\textbf{x})(Tr(A, \textbf{x}) \leftrightarrow Tr(C, \textbf{x}))

Simplifed Problem

• We will consider
• Concept satisfiability
• With no facts (i.e., an "empty" ABox)
• With no axoims (i.e., an "empty" TBox)
• Instead of formulae, we will work with a completion graph
• Nodes correspond to individuals
• They have labels (e.g., \mathcal{L}(x))
• Edges to properties
• Labels correspond to property names
• (Could also work with ABoxes)
• To test satisfiability of C
• Create an initial node x
• \mathcal{L}(x) = \{nnf(C)\}
• Apply rules until termination
  

Tableau rules (for con sat)

• Take propos rules, apply them to nodes, and add two new ones:
• "And" rule: 
• Condition: C \sqcap D\in\mathcal{L}(x)  
• Action: add the conjunct(s) to the label
• "Or" rule:
• Condition:  C \sqcup D \in \mathcal{L}(x)
• Action: Spawn graphs with C\in\mathcal{L}(x) and with D\in\mathcal{L}(x)  
• Clash rule:
• If A, \neg A appear in a label, that graph is closed
• Exists rule:
• Condition: \exists P.C
• Action: Create a P edge to a new node, y s.t. \mathcal{L}(y) = \{C\}
• Forall rule:
• Condition:  \forall P.C\in\mathcal{L}(x), there is a P succ, y, s.t., C\not\in\mathcal{L}(y)
• Action: \mathcal{L}(y) = \mathcal{L}(y) \cup \{C\}

Work some examples!

\[\exists R. A \sqcap \exists R.\neg A\]

\[\exists R. (A \sqcap \neg A)\]

\[\exists R. A \sqcap \forall R.\neg A\]

\[\exists R. (A \sqcup \neg A)\]