185.A46 Automated Deduction Automatisches Beweisen
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2013S, VU, 4.0h, 6.0EC, wird geblockt abgehalten

Merkmale

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

Ziele der Lehrveranstaltung

Der Student/ die Studentin soll die Grundlagen und Grundtechniken des Automatischen Beweisens erlernen, sowie den Gebrauch automatischer Beweisprogramme

Inhalt der Lehrveranstaltung


Transformation in Normalform, Semantische Baeume, Unifikation, Resolution, Verfeinerungen der Resolution, Paramodulation, Experimente mit Automatischen Beweisern. Didaktisches Vorgehen: waehrend der Lehrveranstaltung werden 2 Gruppen von Aufgaben verteilt welche mit Hilfe des Beweisers prover9 zu loesen sind. Muendliche Abschlusspruefung.

Weitere Informationen

Aufwandsabschaetzung

54h: 18 Vorlesungseinheiten a 2std + 1Std Vorbeitung

8h: Loesen erstes Uebungsblatt

2h: tippen der Loesungen in LaTeX

8h: downloaden und Testen von prover9

34h: Loesen 2. Uebungsblatt (mit Hilfe von prover9)

3h: tippen der Loesungen in LaTeX

40h: Vorbereitung auf abschl. Pruefung

1h: abschliessende Pruefung

-----------------------------------------------------------

150 h = 6 ECTS

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Do.16:00 - 20:0025.04.2013 - 27.06.2013Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Automated Deduction Automatisches Beweisen - Einzeltermine
TagDatumZeitOrtBeschreibung
Do.25.04.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.02.05.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.16.05.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.23.05.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.06.06.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.13.06.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.20.06.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
Do.27.06.201316:00 - 20:00Seminarraum FAV EG C (Seminarraum Gödel) Automatisches Beweisen
LVA wird geblockt abgehalten

LVA-Anmeldung

Nicht erforderlich

Curricula

StudienkennzahlVerbindlichkeitSemesterAnm.Bed.Info
066 011 DDP Computational Logic (Erasmus-Mundus) Keine Angabe
066 931 Computational Intelligence Gebundenes Wahlfach
066 937 Software Engineering & Internet Computing Gebundenes Wahlfach

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Sprache

Englisch