Motivace

Predikátová logika je jedním z nejlépe prozkoumaných systémů pro reprezentaci a zpracování znalostí. Ačkoli původně navržená pro studium relace logického důsledku, stala se predikátová logika nebo v jiné terminologii teorie prvního řádu prototypem schémat pro reprezentaci znalostí. Původně byla predikátová logika zkoumána pro potřeby matematické, ale brzy se ukázalo zejména v souvislosti s rozvojem informatiky, že jde o velmi univerzální prostředek umožňující analyzovat jazykové výrazy nezbytné právě pro reprezentaci znalostí v mnoha, na první pohled odlišných, tematických oblastech. Navíc se tento prostředek reprezentace ukázal jako výhodný pro studium odvoditelnosti (inference) mezi tvrzeními, což je patrně ten nejvýznamnější příspěvek predikátové logiky pro porozumění výpočtovým problémům soudobé informatiky.

Rezoluční metoda v predikátové logice je obdobná stejnojmenné metodě ve výrokové logice. Ovšem vzhledem k bohatší vnitřní struktuře formulí predikátové logiky je složitější. Používá se v logickém programování a je základem programovacího jazyka Prolog.