LaTeX バックエンドを使用した Fitch スタイルの証明のための最小限の WYSIWYG プロセッサ

Question

これが TeX.SE に適しているのか、それとも Stackoverflow に適しているのかはわかりませんが、ほとんどが TeX 中心であることを考えると、ここの TeX 集合知が最も適していると考えました。

私は、フィッチスタイルの論理証明を書くためのGUIドキュメントプロセッサが欲しいです。LPLFitch パッケージ. 完全に WYSIWYG (見たままが得られる) にしたいです。ユーザーが TeX コードを直接操作する必要はなく、バックエンドで LaTeX を使用します。さらに、ユーザーのマシンに LaTeX をインストールする必要のない、完全に自己完結型のものにしたいです。これは、TeX の経験がない学生がこのような証明を作成するのに役立つでしょう。

私が疑問に思うのは、既存のオープンソースのリソースは何かということです。私が知っている唯一のものはリックスしかし、これは私が考えている非常に小さなプロセッサとは対照的に、LaTeX の完全な実装を目的としています。このプロセッサでは、非常に少数のパッケージと LaTeX の全機能の最小限のサブセットのみが使用されます。

目標：

1. 完全に WYSIWYG なドキュメント プロセッサ。
2. 必要な記号を挿入するためのボタンがいくつかあり、それらの記号がすぐにレンダリングされます (Unicode 記号として挿入するか、クイックコンパイルを実行するかのいずれか)。
3. ユーザー側で LaTeX の知識を必要とせず、ユーザーのマシンに LaTeX を完全にインストールする必要もありません。
4. LPLFitch パッケージにあるような、Fitch スタイルの自然演繹証明を生成します。

質問：

1. 構築の基盤として利用できる既存のオープンソース リソースにはどのようなものがありますか?
2. このようなものをゼロから実装する場合のアドバイスはありますか (たとえば、LuaTeX を使用するか、よりプログラム的な TeX を使用するなど)?
3. これは良いアイデアなのでしょうか、それとも私が LaTeX に慣れすぎていて、より良い解決策を見逃しているだけなのでしょうか?

これはかなりオープンエンドで、未完成な質問だと認識しています。これは私が始めたばかりのアイデアであり、十分な経験があるわけではありませんが、私が追求したいプロジェクトです。現在の形式の質問がサイトに適していない場合は、完全に理解しています。

Answer 1

2 つの Web ベースのサービスが、質問で尋ねられていることとほぼ同様のことを行います。どちらの場合も、サービスは何らかの TeX エクスポートをサポートしていますが、どちらもlplfitch元の質問で参照されているパッケージを使用しません。

• フィッチJS（参照ライブバージョン) は、Johan Klüwer のパッケージを使用して形式にエクスポートしますfitch.sty。(コピーはロジックマターズプロジェクトの Git リポジトリにも同様に適用されますfitchjs。
• プルーフムード独自の出力カスタムフォーマット; ただし、コードがオープンソースであるかどうかは不明です。(開発は英語版に比べて韓国語版の方が活発であるようにも思われます。)

FitchJSフォークして使用することは可能ですlplfitch。LaTeX 生成を処理するコードは 2 つのファイルにあります。

1. には、parsing.jsUnicode シンボルが LaTeX の同等のシンボルに、または LaTeX の同等のシンボルから変換される部分があります。lplfitch接続語には異なるマイクロコードが使用されていますが、この部分は簡単に修正できるはずです。

2. のエクスポート ルーチンは少し複雑ですuserio.js。パッケージの構文は、パッケージfitchに証明行を追加するための構文とは大幅に異なるためlplfitch、書き直すのにもう少し時間がかかります。

   (証明は内部的にスタックに格納されているようです (ざっと見た限りでは)。その場合、既存のエクスポート ルーチンをダンプして、最初に証明を行に変換し、次に個々の行 (正しい数の縦棒を含む) を出力の 1 行に変換するという新しいルーチンを記述した方がよいかもしれません。論理構造は完全に無視されます。これは、望んでいることとはまったく逆ですlplfitch。)