Wednesday, December 16, 2015

Protégé - Example Ontology file

Please find the Example Ontology file, we created in the lab course for the exercise Modelling the Facts in Protégé from exercise sheet 7.

You can find the same in the material folder as well.

Atoms, Atomic Formulas, and Functions

 © 2015 by Sidney Harris
Thanks again for pointing out ambiguities and lacks of clarity in the lecture material!

In the lab course today, we were discussing atoms vs. atomic formulas in FOL.

Usually, atoms and atomic formulas are used equivalently in FOL to denote formulas that contain no logical connectives and quantifiers, or equivalently, formulas that do not contain any strict subformulas. Atoms (atomic formulas) are the simplest well-formed formulas in FOL.

For example, consider the following (composite) formula:
∀x. P (x) ∧ ∃y. Q (y, f (x)) ∨ ∃z. R (z)

where x,y,z denote variables, f denotes a function symbol, and P, Q, R denote predicates.

The atoms (atomic formulas) contained in this formula are:
  • P (x) 
  • Q (y, f (x))
  • R (z)
In the lecture slides, we only gave a brief summary for the definition of FOL based on examples. For an extensive definition of FOL, please refer to [1].

Thus, whenever we are talking about atoms, as e.g. when we were talking about rules, we refer to atomic formulas.

Then there was the question, whether a function like e.g. mother(x) is an atom/atomic formula?

The definition of an FOL formula says:
  1. If P is a predicate symbol of arity k, and if t1,...,tk, are terms, then P(t1,...,tk) is a formula.
  2. (Negation) For all formulas F, also ¬F is a formula
  3. (Binary Connectives) For all Formulas F,G, also F∧G,F∨G,F→ G,F↔G are formulas 
  4. (Quantifiers) If x is a variable and F is a formula, then also ∀x.F and ∃x.F are formulas
A function alone is only considered a term, following the definition of an FOL term:
  1. all variables are terms
  2. If f is a function symbol of arity k, and if t1,...,tk, are terms, then f(t1,...,tk) is also a term.
For a distinction, you may keep in mind that terms do not compute a truth value, a formula does.

References:
[1] Uwe Schöning: Logik für Informatiker. Spektrum Akademischer Verlag, 2000
or in english:
[2] Uwe Schöning: Logic for computer scientists, Birkhäuser, 2008, also online availabl

Tuesday, December 8, 2015

Final Exam

The final exam will take place on
Friday, February 12, 2016 – 10:00 AM to 12:00 PM

The location will be announced.

Monday, December 7, 2015

Sample solutions (Tableaux)

I compiled one sample solution for the FOL tableaux from exercise sheet 5, thanks to Jan for his template.

And I've found another extensive example for the Mad Cow DL tableaux from exercise sheet 6, it is in German but you hopefully don't mind.

You can find both in the material folder.