Automatické dokazování v Lukasiewiczově vícehodnotové logice
Obor: Informatika, Matematika
Typ: počítačový
Supervizor: doc. Mgr. Michal Botur, Ph.D.
archivovaný projekt (projekt byl dořešen a uzavřen)
Lukasiewiczova vícehodnotová logika je (asi) nejpoužívanější nestandardní logika. Její hlavní myšlenkou je rozšíření škály pravdivostních hodnot z množiny {0,1} (nepravda, pravda) na celý interval [0,1] reálných čísel. Desetinná místa mezi jedničkou a nulou vyjadřují "míru pravdivosti" od úplné nepravdy přes "celkem pravdivé" výroky až k absolutně pravdivému výroku. V současnosti je známa teorie, která umožňuje ověřování pravdivosti výroků automatizovat. Tedy je znám vhodný algoritmus. Našim cílem bude vytvořit program, který tohoto algoritmu využívá a dále jej rozvíjet. Nutnou podmínkou k tématu je alespoň mírně pokročilá znalost některého programovacího jazyka.