Semantics by Translation

Bijan Parsia

COMP60462

Semantics?

• Two sorts:
  • Direct model theory (We've done this!)
  • By translation into something with a clear semantics
    • In our case, First Order Logic (FOL)
    • Other standard targets:
      • 2 variable fragment of FOL (L2)
      • propositional model logic
• How to pick?
  • Ease/familiarity
  • To target existing tools
  • To illustrate different properties
    • FOL is not decidable; L2 is

Translation Semantics

• Why translate?
  • Resuse tools and understanding
  • Transfer metalogical properties
  • Clarify! (Think frames2logic)
• Why we are translating ALC to FOL?
  • To get familiar with the technique.

FOL

• We can translate to binary FOL easily:
• In what follows: var, and var' indicate distinct variables, and var^{new} , etc. indicates a fresh version of the variable.

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

L2

• If we are careful, we can translate into 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
  Tr(A, var)	A(var)
  Tr(\neg C)	\neg (Tr(C, var))
  Tr(C \sqcap D, var)	Tr(C, var) \land Tr(D, var)
  Tr(C \sqcup D, var)	Tr(C, var) \lor Tr(D, var)
  Tr(P, var, var')	P(var, var')
  Tr(\forall P.C, var)	\forall(var')(Tr(P(var, var') \rightarrow Tr(C, var'))
  Tr(\exists P.C, var)	\exists(var')(Tr(P(var, var') \land Tr(C, var'))
  Tr(a:C), Tr(<a, b>:P)	C(a), P(a,b)
  Tr(A \equiv C, x)	\forall(x)(Tr(A, x) \leftrightarrow Tr(C, x))

We inherit

• Reasoning services
  • entailment, satisfiability, query answering
• Reasoning procedures
• Complexity results
  • Since L2 is deciable, ALC is decidable.
• Some insight
  • Models will be tree like!

Repetitive interlude

• Because I forgot we didn't get to this last time

Decidability

• For every question, can we answer YES or NO in a finite number of steps
• Correctly!
• That is, is the problem mechanically solvable
• Propositional logic is decidable
• As are many KR logics
• First order logic is semi-decidable
• Will terminate on all YES answers
• Programming languages are like this
• Why/when does this matter?

Complexity

• How much time (or space)?
• Complexity of problem vs. of algorithm
• How hard is the problem?
• How efficient is the algorithm?
• "Worst case" complexity (WCC)
• How much time will we use if everything goes wrong.
• WWC_{problem} \leq WWC_{algorithm}
• WWC doesn't tell you everything
• I.e., behavior in most cases, best case, "typical" cases, "realisitc" cases, your case!

Complexity 2

Complexity 3

Basic Considerations

• Representational adequacy
• expressiveness
• Weak Cognitive adequacy
• usability
• Computationally sensible
• implementabilty
• Useful services!
• We are focusing on deductive reasoning for now
• A measure of a formalism is whether we get new, useful serivces over time.

Other Applications of Translation

• We can add convenience syntax to our language
  • I.e., macros...e.g., onlySome
• We can analyze other formalisms (Policy...next time)
  • http://www.mindswap.org/papers/2005/Policy-ISWC05.pdf
  • http://www.mindswap.org/~kolovski/xacml.pdf
• We can analyze (and implement) extensions (Quantities...next time)
  • http://www.webont.org/owled/2008/papers/owled2008eu_submission_34.pdf