0

基于我在 mathoverflow 社区中的问题，我想再次在这里提问，以达到更大的社区：

我正在寻找一些软件或开源项目，它们能够以自然演绎的方式证明一阶谓词逻辑的命题，例如在 Lemmon （开始逻辑）一书中介绍的，并且可以将结果放入 LaTeX 代码中。

（你可以在这里找到一个简短的介绍。）

4

0 回答 0