Verzia zo dňa a času 14:36, 1. november 2011

Course opens in winter semester 2011/2012. First lecture: Tue 20 September 2011 in lecture room F-109. See more details below.

Computational Logic 2-AIN-108

go to list of all courses...

Course name and code:	Computational Logic (2-AIN-108)
Prerequisite courses:	none
Available in/recommended study year:	Winter semester / 1
Form and # of hours/week:	L - lecture (2), P - practicals (2)
Credits:	5
Evaluation (semester/exam):	50/50
Course webpage:	you are reading it
Information sheet:	2-AIN-108 information sheet
Teacher(s):	Martin Homola, Martin Baláž (lectures), Alexander Šimko(labs)
E-mail:	teachingtbc.sk, balazii.fmph.uniba.sk
Homepage(s):	http://www.dai.fmph.uniba.sk/w/Computational_Logic

Basic Information

• lectures: Tue 13:10 2h F-109
• labs: Wed 9:50 2h II
• labs: Wed 8:10 2h H6
• midterm: Wed 2 Nov 2011 9:50 in room II

• Labs info: http://ii.fmph.uniba.sk/~simko/vl/
• Lecture notes: http://wiki.matfyz.sk/CL2011_Poznámky_k_predmetu_Výpočtová_logika

• Results (login required)
  • Wiki assignment

Evaluation and Conditions

There will be a midterm and a final exam. During the semester you can earn evaluation points at the practicals (possibly for homeworks) and by participating on the wiki-based collaborative lecture notes. You can earn up to 102 points:

• practicals: 3 pts every week (6 weeks)
• lecture notes: 3 pts every week (12 weeks)
• midterm: 15 pts
• exam: 30 pts

The following grading scale will be used:

• A = 80 pts and more
• B = 71 pts and more
• C = 62 pts and more
• D = 53 pts and more
• E = 44 pts and more
• Fx = less than 44 pts

Syllabus

1. Propositional Logic (PL) and First Order Logic (FOL)
   • The language of PL and FOL
   • Semantics: interpretation and model
   • Satisfiability and logical consequence
   • Proof theory: deduction, skolemization, unification, resolution
2. Modal Logic
   • Modal operators box and diamond
   • System K
   • Basic axioms of modal logic
   • Semantics: Kripke structures
   • Basic axioms of modal logic
   • Systems T, B, S4 and S5 (briefly)
3. Description Logics (DL) and Ontologies
   • Ontologies
   • Description logic ALC: syntax and semantics
   • Tableaux reasoning algorithm
   • More expressive DL (briefly)
   • Applications
4. Logic Programming (LP)
   • Horn clauses
   • SLD-resolution and Prolog
   • Definite LP
   • Normal LP
   • Stable model semantics and Answer Set Programming
   • Extensions: extended, disjunctive and nested LP (briefly)
5. Logic of Context
   • Problem of generality in AI, need of context
   • Context as a box
   • Context properties and operations
   • Local Model Semantics
   • Multi-context Systems
6. Dynamic Logic
7. Epistemic Logic
8. Temporal Logic (♠)
9. Multi-valued Logics (♠)

♠) The last two topics of the course may be left out due to time constraints

Lecture Notes

There is no coherent study-material for this course. You are advised to take notes. To facilitate this, we have created dedicated lecture-notes pages in the students' wiki where you are all asked to regularly contribute in a collaborative fashion. Your goal is to keep coherent, full-scope, up-to-date lecture notes, covering all material from the lectures. And at least briefly, also the practicals. For your activity you can earn up to 3 pts per week. Visit the lecture notes.

Lecture slides

1. Propositional Logic
2. First-Order Logic
3. Description Logic ALC
4. Reasoning with ALC
5. Logic Programming - Prolog

Exercises

1. Resolution