完成したものは僕のGitHub Pagesで公開しています。 連言やカットなどの機能は省略したのでほぼ導出原理(の証明の探索)そのままになっています。 Prologの文法 Prologのプログラムはホーン節と呼ばれる述語論理の論理式の列から成ります。さらにホーン節は仮…

pdfを書きました．龍田「型理論」の9章を行間を埋めつつ，これ単体で完結するようにまとめたものです． drive.google.com