Automatické dokazování vět I - NAIL066

• Anglický název: Automated Theorem Proving I
• Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2013
• Semestr: zimní
• E-Kredity: 3
• Rozsah, examinace: zimní s.:0/2, Z [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: zrušen
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Garant: prof. RNDr. Petr Štěpánek, DrSc.
• Třída: Informatika Mgr. - volitelný
• Kategorizace předmětu: Informatika > Teoretická informatika
• Je korekvizitou pro: NAIL067

Anotace

čeština

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.

Poslední úprava: T_KTI (23.04.2004)

angličtina

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.

Poslední úprava: T_KTI (23.04.2004)

Cíl předmětu

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

Poslední úprava: T_KTI (26.05.2008)

Literatura

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

[2] A concise manual to Otter

[3] MIZAR the basic description

Poslední úprava: T_KTI (23.04.2004)

Sylabus

čeština

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.

Poslední úprava: T_KTI (12.05.2004)

angličtina

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.

Poslední úprava: T_KTI (23.04.2004)