通过程序变换结合逻辑程序与单子二阶逻辑
编程语言
2007-05-23 v1 计算机科学中的逻辑
摘要
我们提出了一种基于展开/折叠变换规则的程序综合方法，可用于从单后继弱单子二阶理论（WS1S）的公式推导出终止的定子逻辑程序。这种综合方法也可以用作一种证明方法，作为 WS1S 闭公式的判定过程。我们应用我们的综合方法将 CLP(WS1S) 程序翻译为逻辑程序，并将其用作验证无限状态系统安全属性的证明方法。
引用
@article{arxiv.cs/0311043,
title = {Combining Logic Programs and Monadic Second Order Logics by Program Transformation},
author = {F. Fioravanti and A. Pettorossi and M. Proietti},
journal= {arXiv preprint arXiv:cs/0311043},
year = {2007}
}
备注
25 pages. Full version of a paper that appears in: M. Leuschel (ed.) Proceedings of LOPSTR'02, Twelfth International Workshop on Logic-based Program Development and Transformation, Madrid, Spain, 17-20 Sept. 2002. Lecture Notes in Computer Science 2664. Springer-Verlag Berlin Heidelberg, 2003, pp. 160-181