私は Java プログラムを作成して、基本的な離散数学 (つまり、ステートメントの真値のチェック) を行う人々を支援したいと考えています。これを行うには、ユーザーが入力する変数の数、そこにある演算子、および存在する場合はどの量指定子 (∃ と ∀) を検出できる必要があります。これらすべてを実行できる優れたアルゴリズムはありますか?
ご存知のように、私は結果だけが欲しいわけではありません。彼らの入力を完全に制御したいので、論理的な証拠を示すことができます。(そのため、JavaScript に渡すようなことはできません)。
私が使用した手法は、文脈自由文法を使用して入力文字列を解析することです。これを行うのに役立つフレームワークはたくさんあります。私は過去にANTLRを個人的に使用して、入力文字列を個別のロジックツリーに解析しました。ANTLRを使用すると、JavaタイプにマップできるCFGを定義できます。これにより、データ構造にマップして、式の真理値を格納および評価できます。もちろん、データ構造に含まれる変数を引き出すこともできます。
さて、あなたの質問は少し漠然としていますが、私はあなたが何をしたいのかを理解していると思います: 一次論理式を処理し、ユーザーにそのような式の操作方法を段階的に示す教育支援ですよね? このアイデアにはメリットがあると思います。一人のプロジェクトとしても完全に実行可能ですが、それほど簡単ではありません。多くの新しいことを学ばなければなりませんが、それらはすべて非常に興味深いものです。そこから何も生まれなくても、確かに貴重な知識を得ることができます。
小さく始めることをお勧めします。ゼロ次論理式を認識する再帰降下パーサーを構築することから始めます (式が有効かどうかを判断するマシン。つまり、"A ^ B" は受け入れますが、"^ A ^" は拒否します)。 . 次に、式を保存する方法を工夫する必要があります。そうすれば、実際に作業できるようになります。それからまた、小さく始めましょう: のような有効なゼロ次論理式を受け入れ、それを段階的に真に減らすことに成功する小さなマシンは、すでに人々が学ぶことができるものであり、書くのはそれほど難しくありません。冒険したい場合は、変数を追加して方程式を作成してください: -- 簡約と真理値表を使用すると、これらを簡単に解決できます。TRUE AND NOT (TRUE AND FALSE)A AND TRUE = TRUE
変数をバインドする量指定子の場合、事態はややこしくなります。自動化された定理の証明が機能する場所です。しかし、それはあなたが何をしたいかによって異なります.さまざまな正規形への変換を実装し、プロセスを段階的に学生に示すことは、かなり簡単で、むしろ便利です.
いずれにせよ、これはまともな個人的なプロジェクトだと思いますし、そこから多くのことを学ぶことができます. 大学に在籍している場合は、最終的に単位を取得することもできます。