UNITY逻辑中关于unless的若干结果

Some Results on Unless Properties in UNITY Logic

本文的工作主要分为两部分．首先，我们把验证ｐｕｎｌｅｓｓｑ是否是ＵＮＩＴＹ逻辑的定理转化为一阶定理的验证．其次，设ｐ１ｕｎｌｅｓｓｑ１，…，ｐｎｕｎｌｅｓｓｑｎ在一ＵＮＩＴＹ程序Ｆ中成立．我们把验证ｐｕｎｌｅｓｑ在Ｆ中成立是否可由以上ｎ个性质得出转化为强推出的验证，其中强推出是本文引进的新概念．

The first goal of this paper is to reduce the provability problem of “unless” formulas in UNITY logic to the propositional provability problem. The Second is to reduce the problem determining if satisfiability of a “unless” property in a UNITY program can be derived from that of othe “unless” properties to the strong provability problem in propositional logic. Where the notion of strong provability is a mew notion introduced in this paper.