如何将经典的自然演绎证明翻译成计算机程序？

如何解决如何将经典的自然演绎证明翻译成计算机程序？

我一直在学习命题逻辑的自然演绎（特别是 Chiswell 和 Hodges 的数学逻辑教科书第 2 章中描述的系统），并且一直在探索 Curry-霍华德信件。这展示了如何进行自然推导，并将其相当直接地转换为 Scala 或 Haskell 等语言的类型化程序。或者至少，对于不使用“Reductio ad absurdum”(RAA) 规则的直觉证明，我可以。通过一些阅读，我发现也有一些方法可以探索经典证明的计算解释，也许使用像 call/cc 这样的控制运算符。是否可以在真正的编程语言中使用这些想法？希望有人可以提供一些有关如何工作的指示/示例。