from 計算モデル

プログラムとは論理式だ！

論理式の証明とは計算だ！

計算の答えは真か偽の2値になるのか？

論理式自体は値ではない

名前の通り、式だ

式の意味の解釈の仕方を定めて初めて値が定まる

解釈の仕方は無限にある

が、論理モデルではHerbrand解釈というのを使うらしい

関数モデルでは、関数自体が値を表現してた

そもそも現実世界の問題を、証明するために、計算に落とし込むのがそもそもムズイ

証明のスタート地点に立つのがムズイという意味

無限の可能性を論理式で扱うために、扱う論理式を制限する

なんでこれが効果があるんだ？

Horn節という論理式を使う

公理の下で命題が成り立つことを証明する過程が計算に当たる

公理とはHorn節のことで、プログラムのこと

命題とは、データのこと