Automatické dokazování

Logician

Automatické dokazování
« kdy: 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?


zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Automatické dokazování
« Odpověď #1 kdy: 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.

zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Automatické dokazování
« Odpověď #2 kdy: 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.

zboj

  • *****
  • 1 507
    • Zobrazit profil
    • E-mail
Re:Automatické dokazování
« Odpověď #3 kdy: 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 :)