用於帶有 LaTeX 後端的 Fitch 式校樣的最小所見即所得處理器

Question

我不確定這是否更適合 TeX.SE 還是 Stackoverflow，但考慮到它主要以 TeX 為中心，我認為這裡的 TeX hive 思維將是最適合的。

我想要一個 GUI 文件處理器來編寫 fitch 風格的邏輯證明，就像用LPL匹配包。我希望它完全是所見即所得（所見即所得），不需要用戶直接與 TeX 程式碼交互，而是在後端使用 LaTeX。此外，我希望它是完全獨立的，不需要在使用者的電腦上安裝 LaTeX。它將用於幫助沒有 TeX 經驗的學生產生此類證明。

我的問題是現有的開源資源有哪些？我唯一熟悉的就是萊克斯，但這旨在全面實現 LaTeX，而不是我心目中的最小處理器，後者僅利用極少量的軟體包和 LaTeX 全部功能的最小子集。

目標：

1. 完全所見即所得的文件處理器。
2. 將有幾個按鈕來插入必要的符號，並立即渲染這些符號（透過將它們作為 unicode 符號插入，或快速編譯運行）。
3. 不需要用戶端了解 LaTeX，也不需要在用戶電腦上安裝完整的 LaTeX。
4. 將產生 Fitch 風格的自然演繹證明，如 LPLFitch 包中的證明。

問題：

1. 我可以利用哪些現有的開源資源來建置？
2. 對於從頭開始實現這樣的事情，您有什麼建議（例如，使用 LuaTeX 或一些更具程式風格的 TeX）？
3. 這是個好主意嗎？

我意識到這是一個非常開放且不發達的問題。這是我剛開始的一個想法，我沒有很多經驗，但我想追求一個專案。如果該問題不適合當前形式的網站，我完全理解。

Answer 1

兩個基於網路的服務所做的事情與問題中提出的問題大致相似。在這兩種情況下，服務都支援某種 TeX 導出；但是都不使用lplfitch原始問題中引用的套件。

• 惠譽JS（也可以看看現場版fitch.sty) 使用 Johan Klüwer 的套件匯出為某種格式。 （副本可在邏輯問題以及該fitchjs專案的 Git 儲存庫中。
• 證明心情自己的輸出自訂格式;但尚不清楚他們的程式碼是否開源。 （與英文版本相比，韓文版本的開發似乎也更加活躍。）

很有可能分叉FitchJS並使用它lplfitch：處理 LaTeX 生成的程式碼位於兩個檔案中：

1. 其中parsing.js有一部分將 unicode 符號與 LaTeX 等效項進行相互轉換。lplfitch使用不同的微詞作為連接詞；這部分應該很容易修復。

2. 稍微複雜一點的是 中的導出例程userio.js；該套件的語法fitch與在套件中添加證明行的語法有很大不同lplfitch，並且需要更多的時間投入來重新編寫。

   （看來證明儲存在內部堆疊上（如果我的粗略檢視是正確的），在這種情況下，最好轉儲現有的導出例程並編寫新的內容，這基於首先將證明轉換為行和然後將各行（包括正確數量的垂直條）轉換為輸出中的一行，完全忽略邏輯結構，這與想要的完全相反lplfitch。