Logic (WS2015): Unterschied zwischen den Versionen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Tobias Philipp (Diskussion | Beiträge)
Keine Bearbeitungszusammenfassung
Markus Krötzsch (Diskussion | Beiträge)
K (Textersetzung - „ddll.inf.tu-dresden.de“ durch „iccl.inf.tu-dresden.de“)
 
(37 dazwischenliegende Versionen von einem anderen Benutzer werden nicht angezeigt)
Zeile 12: Zeile 12:
|Exam type=Klausur
|Exam type=Klausur
|Description=This course will introduce you to propositional logic and first-order predicate logic. After reviewing syntax and semantics, we will cover some basic concepts like normal forms, substitution, and unification. You will be introduced to proof procedures such as the resolution calculus and related concepts including soundness, completeness, and decidability.
|Description=This course will introduce you to propositional logic and first-order predicate logic. After reviewing syntax and semantics, we will cover some basic concepts like normal forms, substitution, and unification. You will be introduced to proof procedures such as the resolution calculus and related concepts including soundness, completeness, and decidability.
The lecture ends on November 25, and we continue with [https://iccl.inf.tu-dresden.de/web/Science_of_Computational_Logic_(WS2015)/en Science of Computational Logic]
'''Exercise Book'''
Please pay attention to our [https://iccl.inf.tu-dresden.de/web/Datei:CL-PS-Guidelines-2014.pdf guidelines].


'''Test Exams'''
'''Test Exams'''


We plan to run one test exam where participation is compulsory and results will count for 5% of the final grade.
We plan to run two test exam where participation is compulsory and results will count for 10% of the final grade.
The other 95% are determined by the score of the written exam.
<!---
The other 90% are determined by the score of the written exam
However, this only holds if you pass the exam on the first attempt.
However, this only holds if you pass the exam on the first attempt.
If you fail, your grade will solely be determined by the score of your second attempt.
If you fail, your grade will solely be determined by the score of your second attempt.
-->
Test Exam 1: Monday 2th November
Test Exam 2: Wednesday, 9th December
'''Final Exam''': 19th December, 10am in Room ZEU/255/Z (Zeunerbau, Georg-Bährstrasse 3c).


'''Written Exam'''
'''Written Exam'''
Zeile 25: Zeile 39:
The Foundation exam consists of two separate exams:
The Foundation exam consists of two separate exams:
a written examination for the course Logic and an oral examination for the course
a written examination for the course Logic and an oral examination for the course
[https://ddll.inf.tu-dresden.de/web/Science_of_Computational_Logic_(WS2015) Science of Computational Logic].
[https://iccl.inf.tu-dresden.de/web/Science_of_Computational_Logic_(WS2015) Science of Computational Logic].
The written exam is scheduled shortly before Christmas.
The written exam is scheduled shortly before Christmas.


Zeile 36: Zeile 50:
{{Vorlesung Zeiten
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture - History of Logic and Propositional Logic
|Title=Lecture - History of Logic and Propositional Logic, till slide 'recursion'
|Room=APB E005
|Room=APB E005
|Date=2015/10/12
|Date=2015/10/12
|DS=DS6
|DS=DS6
|Download=History2015.pdf, Propositional2015.pdf,  
|Download=History2015.pdf, Propositional2015.pdf,
}}
}}
{{Vorlesung Zeiten
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture - Propositional Logic
|Title=Lecture - Propositional Logic, till 'Replacement Theorem' (slide 27)
|Room=APB E005
|Room=APB E005
|Date=2015/10/14
|Date=2015/10/14
|DS=DS2
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial: Training on Induction, Recursive Functions
|Room=APB E005
|Date=2015/10/15
|DS=DS4
|Download=Sheet-1.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial: The set L(R)
|Room=APB E005
|Date=2015/10/16
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture
|Room=APB E005
|Date=2015/10/19
|DS=DS6
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture, till slide 62
|Room=APB E005
|Date=2015/10/21
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial: Training on entailment, proof structure (iff, implication), counter examples
|Room=APB E005
|Date=2015/10/22
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial: Entailment and unsatisfiability, proof structure
|Room=APB E005
|Date=2015/10/23
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture
|Room=APB E005
|Date=2015/10/26
|DS=DS6
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture - finished propositional logic
|Room=APB E005
|Date=2015/10/28
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial: Replacement Theorem and Normal Forms
|Room=APB E005
|Date=2015/10/29
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial: Resolution
|Room=APB E005
|Date=2015/10/30
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Test Exam I
|Room=APB E005
|Date=2015/11/02
|DS=DS6
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Introduction into Predicate Logic
|Room=APB E005
|Date=2015/11/04
|DS=DS2
|Download=Fol2015.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Test Exam Inspection
|Room=APB E005
|Date=2015/11/05
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Compactness Theorem
|Room=APB E005
|Date=2015/11/06
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture -  till Lemma 4.25
|Room=APB E005
|Date=2015/11/09
|DS=DS6
|Download=fol2015-complete.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture - till slide 55
|Room=APB E005
|Date=2015/11/11
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Natural Deduction
|Room=APB E005
|Date=2015/11/12
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Completeness of Resolution, Pure Literals
|Room=APB E005
|Date=2015/11/13
|DS=DS5
|Download=CompletenessTheorem.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture - till slide 61
|Room=APB E005
|Date=2015/11/16
|DS=DS6
|Download=Fol2015-update.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Syntax and Semantics of FOL
|Room=APB E005
|Date=2015/11/19
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial
|Room=APB E005
|Date=2015/11/20
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture - till Lemma 4.64
|Room=APB E005
|Date=2015/11/23
|DS=DS6
|Download=Fol2015-update2.pdf,
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Vorlesung
|Title=Lecture
|Room=APB E005
|Date=2015/11/25
|DS=DS2
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Presentation of the European Partner Universities
|Room=APB E005
|Date=2015/11/26
|DS=DS4
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Herbrand Interpretation and Infinite Models
|Room=APB E005
|Date=2015/11/27
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Application of Prenex Normalform, Skolemization, Unification, Resolution and Factorization
|Room=APB E005
|Date=2015/12/03
|DS=DS4
}}
}}
{{Vorlesung Zeiten
{{Vorlesung Zeiten
Zeile 53: Zeile 255:
|Title=Tutorial
|Title=Tutorial
|Room=APB E005
|Room=APB E005
|Date=2015/10/15
|Date=2015/12/04
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial
|Room=APB E005
|Date=2015/12/10
|DS=DS4
|DS=DS4
|Download=Sheet-1.pdf,
}}
}}
{{Vorlesung Zeiten
{{Vorlesung Zeiten
Zeile 61: Zeile 269:
|Title=Tutorial
|Title=Tutorial
|Room=APB E005
|Room=APB E005
|Date=2015/10/16
|Date=2015/12/11
|DS=DS5
|DS=DS5
}}
{{Vorlesung Zeiten
|Lehrveranstaltungstype=Übung
|Title=Tutorial - Corresponding Herbrand Interpretations and General Q&A session
|Room=APB E005
|Date=2015/12/17
|DS=DS4
}}
}}

Aktuelle Version vom 2. März 2017, 15:23 Uhr

Logic

Lehrveranstaltung mit SWS 2/2/0 (Vorlesung/Übung/Praktikum) in WS 2015

Dozent

  • Steffen Hölldobler

Tutor

Umfang (SWS)

  • 2/2/0

Module

Leistungskontrolle

  • Klausur


This course will introduce you to propositional logic and first-order predicate logic. After reviewing syntax and semantics, we will cover some basic concepts like normal forms, substitution, and unification. You will be introduced to proof procedures such as the resolution calculus and related concepts including soundness, completeness, and decidability.

The lecture ends on November 25, and we continue with Science of Computational Logic

Exercise Book

Please pay attention to our guidelines.

Test Exams

We plan to run two test exam where participation is compulsory and results will count for 10% of the final grade.

Test Exam 1: Monday 2th November

Test Exam 2: Wednesday, 9th December

Final Exam: 19th December, 10am in Room ZEU/255/Z (Zeunerbau, Georg-Bährstrasse 3c).

Written Exam

This course will be examined as a part of the Foundations exam. The Foundation exam consists of two separate exams: a written examination for the course Logic and an oral examination for the course Science of Computational Logic. The written exam is scheduled shortly before Christmas.

Some remarks on the style of the written exam in logic

  • no exam aids or support materials will be allowed. In other words, only writing materials are allowed.
  • The emphasis of the exam will be on the proofs of theorems, propositions and lemmata from the lectures and the proofs occurring with the problems from the tutorials.
  • In addition, in the first problem of the exam we will usually ask for some definition or algorithm presented on the lectures, e.g. define concepts like substitution, resolvent, interpretation, Skolemization, ... or algorithms like unification, transformation to clause form, ...
  • Maybe, one or two exam problems will be the application of some of the presented calculi (e.g. resolution, natural deduction, normalform transformation, etc).

Veranstaltungskalender abonnieren (icalendar)

Vorlesung Lecture - History of Logic and Propositional Logic, till slide 'recursion' DS6, 12. Oktober 2015 in APB E005 Datei 1 Datei 2
Vorlesung Lecture - Propositional Logic, till 'Replacement Theorem' (slide 27) DS2, 14. Oktober 2015 in APB E005
Übung Tutorial: Training on Induction, Recursive Functions DS4, 15. Oktober 2015 in APB E005 Datei
Übung Tutorial: The set L(R) DS5, 16. Oktober 2015 in APB E005
Vorlesung Lecture DS6, 19. Oktober 2015 in APB E005
Vorlesung Lecture, till slide 62 DS2, 21. Oktober 2015 in APB E005
Übung Tutorial: Training on entailment, proof structure (iff, implication), counter examples DS4, 22. Oktober 2015 in APB E005
Übung Tutorial: Entailment and unsatisfiability, proof structure DS5, 23. Oktober 2015 in APB E005
Vorlesung Lecture DS6, 26. Oktober 2015 in APB E005
Vorlesung Lecture - finished propositional logic DS2, 28. Oktober 2015 in APB E005
Übung Tutorial: Replacement Theorem and Normal Forms DS4, 29. Oktober 2015 in APB E005
Übung Tutorial: Resolution DS5, 30. Oktober 2015 in APB E005
Vorlesung Test Exam I DS6, 2. November 2015 in APB E005
Vorlesung Introduction into Predicate Logic DS2, 4. November 2015 in APB E005 Datei
Übung Test Exam Inspection DS4, 5. November 2015 in APB E005
Übung Tutorial - Compactness Theorem DS5, 6. November 2015 in APB E005
Vorlesung Lecture - till Lemma 4.25 DS6, 9. November 2015 in APB E005 Datei
Vorlesung Lecture - till slide 55 DS2, 11. November 2015 in APB E005
Übung Tutorial - Natural Deduction DS4, 12. November 2015 in APB E005
Übung Tutorial - Completeness of Resolution, Pure Literals DS5, 13. November 2015 in APB E005 Datei
Vorlesung Lecture - till slide 61 DS6, 16. November 2015 in APB E005 Datei
Übung Tutorial - Syntax and Semantics of FOL DS4, 19. November 2015 in APB E005
Übung Tutorial DS5, 20. November 2015 in APB E005
Vorlesung Lecture - till Lemma 4.64 DS6, 23. November 2015 in APB E005 Datei
Vorlesung Lecture DS2, 25. November 2015 in APB E005
Übung Presentation of the European Partner Universities DS4, 26. November 2015 in APB E005
Übung Tutorial - Herbrand Interpretation and Infinite Models DS5, 27. November 2015 in APB E005
Übung Tutorial - Application of Prenex Normalform, Skolemization, Unification, Resolution and Factorization DS4, 3. Dezember 2015 in APB E005
Übung Tutorial DS5, 4. Dezember 2015 in APB E005
Übung Tutorial DS4, 10. Dezember 2015 in APB E005
Übung Tutorial DS5, 11. Dezember 2015 in APB E005
Übung Tutorial - Corresponding Herbrand Interpretations and General Q&A session DS4, 17. Dezember 2015 in APB E005


Kalender

Mai 2025

MoDiMiDoFrSaSo
2829301234
567891011
12131415161718
19202122232425
2627282930311
2345678