2024/05/25 命題論理における推論の妥当性を論理式から自動的に計算する

論理学入門を履修中t6o_o6t.icon

現在は命題論理に関するトピックを学習している

前提を表す論理式と、それを元にした推論を表す論理式が与えられるので、推論の妥当性を判定せよ、という課題が出ている

問題が27問近くあり、手で解くのは苦労する

自動的に判断したいt6o_o6t.icon

論理式のパーサを書いた

Identifier：英大文字（P, Q, A, Bなど）

記号：∧、∨、→、￢

Pratt Parserは演算子が明確な優先順位を持つときは有効だが、今回は優先順位がカッコ以外差を持たない

Group := (Expression InfixOperator Expression)

各括弧が2つの式と中置演算子だけを持てるように実装した

パーサの上に、推論を判定するEvaluatorを書いた

前提を表す論理式は、ASTを生成しつつ、And演算子のASTのleftとrightとして繋ぎこむ

前提と推論を表す条件式は、Implication（→）演算子のASTのleftとrightとして繋ぎこむ

類似しているため、同一の関数でコアロジックを実装した

現在の問題点

main関数内に、標準入力 / 出力とEvaluator呼び出しを全て書いてしまった

ロジックの入力を標準入力から分離する

外部から入力用関数を注入できるようにする

type InputFn = () => string

ロジックの出力を標準出力から分離する

ロジックを関数 validate(presupposition: string[], inference: string): ValidateResultに分割する

前提（string[]）と推論（string）から検証結果（ValidateResult）を返す

code:ValidateResult.ts

type ValidateResult = {

isValid: boolean,

evaluations: {

identifierValues: {

value: number

}

分離したt6o_o6t.icon

これで自由にプログラムで制御できる

ファイルから入力できるようにする

練習問題は.docxで配布されている

先頭行に(1)　というようなものがあり、これは正規表現/^(1)　/で削除できるのではないか

s.replace(/^$\d+$　/, "")

あとは全角文字を削除する

出来たt6o_o6t.icon