ΛProlog: Logic programming in higher-order logic
4 days ago
- #theorem proving
- #logic programming
- #higher-order logic
- λProlog是一种基于高阶直觉主义逻辑的逻辑编程语言。
- 它支持模块化编程、抽象数据类型、高阶编程以及λ树语法。
- 首个直接支持高阶抽象语法（HOAS）的编程语言。
- 最初设计于20世纪80年代末，至今仍有新实现和应用的研究兴趣。
- Dale Miller的著作《证明理论与逻辑编程》详细阐述了λProlog背后的证明理论。
- Abella是一个适用于带绑定规约推理的交互式定理证明器。
- λProlog代码示例可见于Teyjus发行版、书籍摘录及在线实现中。