Automated Theorem Proving II - NAIL067

• Title: Automatické dokazování vět II
• Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2013
• Semester: summer
• E-Credits: 3
• Hours per week, examination: summer s.:0/2, C [HT]
• Capacity: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: cancelled
• Language: Czech
• Teaching methods: full-time
• Guarantor: prof. RNDr. Petr Štěpánek, DrSc.
• Class: Informatika Mgr. - volitelný
• Classification: Informatics > Theoretical Computer Science
• Co-requisite : NAIL066

Annotation

English

Seminar is dedicated to study of machine methods of Theorem Proving. It starts with the classical Resolution method and its extensions and to a study of methods based on equality. Proof checking and theorem proving in mathematical systems using a language close to that of mathematics will be also discussed.Seminar will také attention to implementations of theorem proving systems and to environments consisting of several theorem provers which will can be compared, tested and the environment developed.

Last update: T_KTI (23.04.2004)

Czech

Naplní semináře je studium metod strojového dokazování vět, jednak klasickou rezoluční metodou a jejími rozšířeními, dále studiem metod používající rovnosti. Seminář se také bude zabývat metodami kontroly důkazů a dokazování v matematických systémech formulovaných v jazyce blízkém obvyklému jazyku matematiky.Seminář bude zabývat implementací systémů dokazování vět a celkového prostředí sestávající z více dokazovačů, které jsou testovány a srovnávány podle výkonnosti a dalších měr.

Last update: T_KTI (23.04.2004)

Aim of the course

Naučit metody používané při automatickém dokazování a popsat vybrané konkrétní systémy.

Last update: T_KTI (26.05.2008)

Literature

[1] Automated Reasoning, (A. Robinson, A. Voronkov , editors) The MIT Press 2001

[2] Stručný manuál Otteru

[3] MIZAR základní popis

Last update: T_KTI (23.04.2004)

Syllabus

English

I. Transformation of formulas , effective constructions of sets of clauses equivalent to a given formula. Normal forms of formulas.

II. Classical Resolution Metod, paramodulation, hyperresolution, negative hyperresolution and other extensions.

III. Otter

IV. Formal Systems close to the language of mathematics. Proof Checking.

V. MIZAR

VI. Theorem Proving based on Equality.

Last update: T_KTI (23.04.2004)

Czech

I. Úpravy formulí, efektivní vytváření množiny klauzulí z dané formule, normální tvary formulí

II. Klasická rezoluční metoda, paramodulace,hyperrezoluce, negativní hyperrezoluce jiná její rozšíření.

III. Otter

IV. Formální systémy blízké jazyku matematiky. Kontrola důkazů.

V. MIZAR

VI. Dokazování využívající rovnost.

Last update: T_KTI (23.04.2004)