柯里-霍华德方法对乔治·查奇综合的研究
摘要：Church的综合问题要求是否存在一个满足给定输入输出规范的有限状态流转换器。对于在无限序列上使用单调二阶逻辑（MSO）编写的规范，Church的综合可以理论上使用自动机和博弈算法解决。通过引入SMSO，即基于直觉的MSO的一个变体，在Curry-Howard对应关系下重新审视Church的综合问题，我们证明了SMSO在合成方面是完备和准确的，这得益于基于自动机的实现模型。
作者：C''ecilia Pradic and Colin Riba
论文ID：1803.08958
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22