一句话：提出 LMSO 证明系统，从 ω-正则规范的线性构造性证明中提取有限状态流转换器。
本文提出 LMSO——一个受线性逻辑启发的证明系统，作为从 ω-正则规范的线性构造性证明中提取有限状态流转换器的证明论框架。Church 综合问题要求由规范自动构造满足该规范的有限状态流转换器；LMSO 借助 Curry-Howard 对应，将证明视为程序，并给出基于自动机的可实现性模型，把证明解释为有限状态流转换器。作者证明了系统的正确性：该模型为证明提供可靠语义；同时证明了完备性：每个可解的 Church 综合实例都对应规范公式的一个线性构造性证明。该工作旨在作为半自动方法的踏脚石，将计算机辅助证明与自动判定过程结合。
We propose LMSO, a proof system inspired from Linear Logic, as a proof-theoretical framework to extract finite-state stream transducers from linear-constructive proofs of omega-regular specifications. We advocate LMSO as a stepping stone toward semi-automatic approaches to Church's synthesis combining computer assisted proofs with automatic decisions procedures. LMSO is correct in the sense that it comes with an automata-based realizability model in which proofs are interpreted as finite-state stream transducers. It is moreover complete, in the sense that every solvable instance of Church's synthesis problem leads to a linear-constructive proof of the formula specifying the synthesis problem.
DOI 原文 ·
@inproceedings{paperbot4350,
title = {LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic},
author = {Cécilia Pradic and Colin Riba},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209195}
}