Fórum Root.cz

Ostatní => Odkladiště => Téma založeno: Logician 03. 06. 2017, 22:27:18

Název: Automatické dokazování
Přispěvatel: Logician 03. 06. 2017, 22:27:18
V logice jsme dostali za úkol přečíst si "Machine Oriented Logic Based on the Resolution Principle", což jsem udělal a teď si říkám - proč se používá zrovna FOL? V jiných kontextech (třeba reprezentace jazyků jako angličtina nebo čeština) se používají často predikáty vyšších řádů, kde už rezoluce neplatí. Znamená to, že s FOL lze sice formálně dobře pracovat, ale nestačí k popisu výroků v běžných jazycích?
Název: Re:Automatické dokazování
Přispěvatel: zboj 04. 06. 2017, 13:36:07
V logice jsme dostali za úkol přečíst si "Machine Oriented Logic Based on the Resolution Principle", což jsem udělal a teď si říkám - proč se používá zrovna FOL? V jiných kontextech (třeba reprezentace jazyků jako angličtina nebo čeština) se používají často predikáty vyšších řádů, kde už rezoluce neplatí. Znamená to, že s FOL lze sice formálně dobře pracovat, ale nestačí k popisu výroků v běžných jazycích?
Stačí, když se použije konjunktivistická notace. V obecné sémantice je logika vyššího řádu úplná a převoditelná reifikací na FOL, čehož se využívá v reprezentaci.
Název: Re:Automatické dokazování
Přispěvatel: zboj 05. 06. 2017, 11:30:11
P.S. Stručný článek o tomto problému má v češtině Peregrin včetně letmé ukázky oné reifikace.
Název: Re:Automatické dokazování
Přispěvatel: zboj 12. 06. 2017, 14:26:30
P.S. Stručný článek o tomto problému má v češtině Peregrin včetně letmé ukázky oné reifikace.
P.P.S. Jinak je k tomu "výživné" čtení na Stanford Encyclopedia of Philosophy :)