Revising basic theorem proving algorithms to cope with the logic of partial functions
Revising basic theorem proving algorithms to cope with the logic of partial functions
复制标题
修改基本定理证明算法以应对部分函数的逻辑
DOI：
10.1016/j.scico.2013.09.007
复制
发表时间：
2014
影响因子：
1.3
通讯作者：
Jones C
中科院分区：
文献类型：
--
作者：
Jones C
部分术语是那些不能表示值的术语；这种术语经常出现在程序的规范和开发中。早期的论文描述并论证了非经典的“部分函数逻辑”(LPF)的使用，以便于对这些术语进行合理和方便的推理。本文回顾了基本定理证明算法--例如归结算法--并指出了它们需要修改以处理LPF的地方。在“反驳”程序中需要特别小心。相对于语义模型，改进的算法是合理的。提供了进一步工作的迹象，这些工作可能导致对法律援助框架的有效支持。
Partial terms are those that can fail to denote a value; such terms arise frequently in the specification and development of programs. Earlier papers describe and argue for the use of the non-classical “Logic of Partial Functions” (LPF) to facilitate sound and convenient reasoning about such terms. This paper reviews the fundamental theorem proving algorithms — such as resolution — and identifies where they need revision to cope with LPF. Particular care is needed with “refutation” procedures. The modified algorithms are justified with respect to a semantic model. Indications are provided of further work which could lead to efficient support for LPF.
登录
查看更多内容
偏函数的强Kleene逻辑的机械化
DOI：
--
发表时间：
1994
期刊：
CADE
影响因子：
--
作者：
Manfred Kerber;M. Kohlhase
通讯作者：
M. Kohlhase
经典重构的部分函数的类型化逻辑
影响因子：
0.6
作者：
Cliff B. Jones;K. Middelburg
通讯作者：
K. Middelburg
VDM 中的证明：从业者指南
DOI：
10.1007/978-1-4471-2033-9
发表时间：
1993
期刊：
Int. J. Softw. Informatics
影响因子：
--
作者：
J. Bicarregui;J. Fitzgerald;P. Lindsay;Richard C. Moore;B. Ritchie
通讯作者：
B. Ritchie
DOI：
--
发表时间：
2011
期刊：
International Journal of Software and Informatics
影响因子：
--
作者：
Cliff B. Jones
通讯作者：
Cliff B. Jones
DOI：
--
发表时间：
2006
期刊：
影响因子：
--
作者：
J. Fitzgerald
通讯作者：
J. Fitzgerald