184.774 Automated Deduction Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_20",{id:"j_id_20",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_22",{id:"j_id_22",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});});

2019S, VU, 4.0h, 6.0EC

Merkmale

• Semesterwochenstunden: 4.0
• ECTS: 6.0
• Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

The reasoning power that computational logic offers brings new perspectives in the field of program verification. This course is about computational logic, with particular focus on algorithmic and automated methods for proving logical properties.

The course aims at teaching attendees algorithmic techniques and fundamental results in automated deduction. Student will also use state-of-the-art theorem provers for proving logical properties.

Inhalt der Lehrveranstaltung

The course focuses on specialised algorithms for reasoning in various fragments of first-order logics, such as propositional logic, combination of ground theories, and full first-order logic with equality. We will address both the theoretical and practical aspects for using and implementing (semi-)decisions procedures of various logics.

The tentative list of topics covered by the course is below:

• propositional and first-order logic;
• satisfiability checking in propositional logic (splitting, DPLL, randomized algorithms);
• satisfiability checking in the theory of arithmetic, uninterpreted functions and arrays;
• satisfiability checking the the combination of theories (SMT);
• validity proving in first-order logic (superposition theorem proving).

The course will address transformation to normal forms, DPLL, SAT-solving, SMT-solving, resolution, unification, superposition, redundancy checking, and  experiments with theorem provers.

Weitere Informationen

The course is held block, within 7 weeks, with 2 lectures a week

The first lecture is on March 7, 9:15--10:45, in EI 3 Sahulka HS.

LVA Termine

TagZeitDatumOrtBeschreibung
Di.10:00 - 12:0005.03.2019 - 14.05.2019EI 8 Pötzl HS LVA Automated Deduction
Do.09:00 - 11:0007.03.2019 - 27.06.2019EI 3 Sahulka HS LVA Automated Deduction
Do.10:00 - 10:4523.05.2019EI 8 Pötzl HS Automated Deduction 184.774 - Recap
Di.09:00 - 12:0011.06.2019EI 8 Pötzl HS Automated Deduction 184.774: Exam
Mi.09:00 - 12:0012.06.2019EI 10 Fritz Paschke HS - ETIT Automated Deduction 184.774 - Exam
Automated Deduction - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.05.03.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.07.03.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.12.03.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.14.03.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.19.03.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.21.03.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.26.03.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.28.03.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.02.04.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.04.04.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.09.04.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.11.04.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.30.04.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.02.05.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.07.05.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.09.05.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Di.14.05.201910:00 - 12:00EI 8 Pötzl HS LVA Automated Deduction
Do.16.05.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Do.23.05.201909:00 - 11:00EI 3 Sahulka HS LVA Automated Deduction
Do.23.05.201910:00 - 10:45EI 8 Pötzl HS Automated Deduction 184.774 - Recap

Leistungsnachweis

The course grade will be based on three written homework assignments and a written exam.

Homework assignments count for 40% of the course grade.

LVA-Anmeldung

Nicht erforderlich

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Englisch