DEV Community
·
挑战基础逻辑：一个非常困难的自动推理挑战（开放参与）
💡
原文英文，约900词，阅读约需4分钟。
📝
内容提要
我设计了一个开放式逻辑难题，挑战自动推理，要求找到比现有数千步的最短证明更短的形式证明。欢迎有兴趣的开发者参与。
🎯
关键要点
- 我设计了一个开放式逻辑难题，挑战自动推理。
- 该难题涉及形式证明，与结构证明理论相关。
- 自今年三月以来，只有三人提出改进方案。
- 目标是找到比现有数千步的证明更短的形式证明。
- 每个证明只能使用一个经典命题逻辑的最小公理。
- 证明基于浓缩分离法，要求复杂的自动化。
- 所探讨的证明系统是希尔伯特系统，难以找到短证明。
- 目前已知的最短证明有数千步。
- 我展示了一个仅13步的短证明示例。
- 挑战在GitHub的讨论论坛进行，提供工具支持。
- 我正在测试新的公式合成证明压缩功能。
- 要在排行榜上占据首位，需要至少减少现有49个最短证明中的一个步骤。
- 欢迎有兴趣的开发者参与，提供帮助和建议。
➡️
