我不确定这是否更适合 TeX.SE 或 Stackoverflow，但考虑到它主要是以 TeX 为中心的，我认为这里的 TeX 集体思维是最合适的。
我想要一个 GUI 文档处理器，用于编写 fitch 风格的逻辑证明，就像使用LPLFitch 软件包。我希望它完全是所见即所得的，不需要用户直接与 TeX 代码交互，而是在后端使用 LaTeX。此外，我希望它完全独立，不需要在用户的机器上安装 LaTeX。它将用于帮助没有 TeX 经验的学生制作此类证明。
我的问题是，目前有哪些开源资源？我唯一熟悉的是莱克斯但是其目的是全面实现 LaTeX，而不是我所设想的最小处理器，后者只会使用极少数的软件包和 LaTeX 全部功能的最小子集。
目标：
- 完全所见即所得的文档处理器。
- 会有几个按钮来插入必要的符号，并会立即呈现这些符号（通过将它们作为unicode符号插入，或快速编译运行）。
- 不需要用户具备 LaTeX 知识，也不需要在用户的机器上安装完整的 LaTeX。
- 将产生 Fitch 风格的自然演绎证明，类似于 LPLFitch 包中的证明。
问题：
- 有哪些现有的开源资源可供我利用？
- 对于从头开始实现这样的功能，您有什么建议（例如，使用 LuaTeX 或者一些更具程序性的 TeX）？
- 这是一个好主意吗，还是我只是因为熟悉 LaTeX 而看不到更好的解决方案？
我意识到这是一个相当开放和不成熟的问题。这是我刚刚开始的一个想法，我对此没有大量的经验，但这是一个我想进行的项目。如果这个问题不适合目前的网站形式，我完全理解。
答案1
两个基于 Web 的服务所做的工作与问题中要求的大致相同。在这两种情况下，服务都支持某种 TeX 导出；但是，它们都没有使用lplfitch原始问题中引用的包。
- 惠誉（也可以看看直播版本) 使用 Johan Klüwer 的软件包导出为某种格式
fitch.sty。（可在逻辑问题以及该fitchjs项目的 Git 仓库。） - 证明情绪输出自己的自定义格式；但尚不清楚其代码是否开源。（与英文版相比，韩文版的开发似乎更为活跃。）
完全可以分叉FitchJS并使用它lplfitch：处理 LaTeX 生成的代码位于两个文件中：
其中
parsing.js有一部分是将unicode符号与其LaTeX等效符号相互转换。lplfitch使用不同的微控制器来连接词；这部分应该很容易修复。稍微复杂一点的是中的导出例程
userio.js；包的语法fitch与在包中添加证明行的语法有很大不同lplfitch，需要投入更多的时间来重写。（看来证明是内部存储在堆栈上的（如果我的粗略查看是正确的），在这种情况下，最好转储现有的导出例程并编写一些新内容，这基于首先将证明转换为行，然后将各个行（包括正确数量的垂直条）转换为输出中的一行，完全忽略逻辑结构。这与想要的完全相反
lplfitch。）