述語論理をやろうず - Qiita

概要 プログラミング言語上で 1階述語論理の言語を実装したい。具体的には「論理式を 冠頭標準形 に変形し スコーレム標準形 を求め、節形式にする手順を実装に落とし込みたい」。そのために必要な 各種検討項目をまとめた。要するに 本稿は 論理プログラミング一歩手前までの数理論理学をプログラムに落とし込むための設計ドキュメントだといってよい。コードは未記載(分量が多いのでQiitaじゃないところに公開するかも)。 想定動作環境: Node上でのJavaScript で動作。依存パッケージは moo(字句解析), nearley (構文解析) のみ。npm i --save moo nearley で環境構築完了。 0. 表記 ～言語の記号～ 変数は以下が使える: x, y, z, w, x1, x2, ...x99 定数は以下が使える: a, b, c, a1, a2, ... a99 関数は以