DEV Community
·
挑战基础逻辑：一个非常困难的自动推理挑战（开放参与）
原文英文，约900词，阅读约需4分钟。
📝
内容提要
我设计了一个开放式逻辑难题，挑战自动推理，要求找到比现有数千步的最短证明更短的形式证明。欢迎有兴趣的开发者参与。
🎯
关键要点
-
我设计了一个开放式逻辑难题，挑战自动推理。
-
该难题涉及形式证明，与结构证明理论相关。
-
自今年三月以来，只有三人提出改进方案。
-
目标是找到比现有数千步的证明更短的形式证明。
-
每个证明只能使用一个经典命题逻辑的最小公理。
-
证明基于浓缩分离法，要求复杂的自动化。
-
所探讨的证明系统是希尔伯特系统，难以找到短证明。
-
目前已知的最短证明有数千步。
-
我展示了一个仅13步的短证明示例。
-
挑战在GitHub的讨论论坛进行，提供工具支持。
-
我正在测试新的公式合成证明压缩功能。
-
要在排行榜上占据首位，需要至少减少现有49个最短证明中的一个步骤。
-
欢迎有兴趣的开发者参与，提供帮助和建议。
🔎
延伸解读
挑战的复杂性
该逻辑难题的复杂性源于使用希尔伯特系统，这种系统虽然定义简单，但寻找短证明却极为困难。参与者需要掌握浓缩分离法，并具备较强的编程能力，以便有效地进行自动推理。
参与者的机会
尽管目前只有少数人提出改进方案，但这也意味着参与者有机会在排行榜上脱颖而出。只需在现有49个最短证明中减少一步，就能获得认可，激励更多开发者参与挑战。
工具的支持
挑战提供了GitHub上的工具支持，参与者可以利用这些工具简化证明生成过程。掌握这些工具的使用将大大提高参与者的效率，尤其是在处理复杂的逻辑证明时。
❓
延伸问答
这个逻辑难题的主要目标是什么？
主要目标是找到比现有数千步的证明更短的形式证明。
参与这个挑战需要哪些技能？
参与者需要具备创造力和高级编程技能。
这个挑战使用了什么样的证明系统？
挑战使用的是希尔伯特系统，这是一种经典的命题逻辑证明系统。
目前已知的最短证明有多少步？
目前已知的最短证明有数千步。
如何在排行榜上获得高分？
要在排行榜上占据首位，需要至少减少现有49个最短证明中的一个步骤。
这个挑战在哪里进行讨论？
挑战在GitHub的讨论论坛进行，提供工具支持。
🏷️
