机器证明？

[bihai]

十年前我对机器证明有些兴趣。我的关注点不在计算机自动证明这个方面，而是能描述证明的过程即可，就是说，得有一套体系来描述几何证明的过程。

假设，有一个app，里面有一个题目。然后中学生利用UI，把定理，公里和条件一起使用，来制造新的信息，即新的条件，最终到达目标。就是这个app可以验证学生的证明是正确的。

我尝试了一个方法，用Java的什么Generic。搞了一些函数，类。但是问题是我的方法需要在编译期间能通过，这些定理需要在编译引入，而不是运行期。这挺麻烦的，就是说学生证明的新的定理不能动态使用。

最近想重新了解一下这个领域。看吴文俊的书。第一步就看不懂


定理机器证明

https://www.ecsponline.com/yz/B1FBFE973 ... 4BD000.pdf
14页

I3 一直线上至少有两点，至少有三个点不在同一条直线上。

这是写错字了吗？看不懂人话

[hci]

就是字面意思吧：一条直线上至少有两点。要想不在同一直线上，至少需要三个点。也就是说，只有两点的话，二者必然在一条直线上。

看书不要想太多了。

十年前我对机器证明有些兴趣。我的关注点不在计算机自动证明这个方面，而是能描述证明的过程即可，就是说，得有一套体系来描述几何证明的过程。

假设，有一个app，里面有一个题目。然后中学生利用UI，把定理，公里和条件一起使用，来制造新的信息，即新的条件，最终到达目标。就是这个app可以验证学生的证明是正确的。

我尝试了一个方法，用Java的什么Generic。搞了一些函数，类。但是问题是我的方法需要在编译期间能通过，这些定理需要在编译引入，而不是运行期。这挺麻烦的，就是说学生证明的新的定理不能动态使用。

最近想重新了解一下这个领域。看吴文俊的书。第一步就看不懂


定理机器证明

https://www.ecsponline.com/yz/B1FBFE973 ... 4BD000.pdf
14页

I3 一直线上至少有两点，至少有三个点不在同一条直线上。

这是写错字了吗？看不懂人话