PLPとPrologの違いについて説明していきます。Prologのプログラムは論理式として見ることもできるのですが、実行する順序が決まっていて、プログラムとして実行することができるようになっています。これを説明するためPrologの単一化(unification)について…

逆に という形の列(各 は という形の論理式)を証明する証明図(*)が存在するとします。 という論理式を とおきます。 を 個並べた列を と書くことにします。 「シークエント計算」についてはほとんど説明していないし、詳しく知っているわけでもないので以下…