论文标题
抽象运营商对功能完整性的一般验证
A General Verification for Functional Completeness by Abstract Operators
论文作者
论文摘要
如果操作员无法代表完整集$ \ lbrace \ neg，\ vee，\ wedge，\ rightarrow，\ leftrightArrow \ rbrace $，则在功能上是不完整的。功能不完整的验证高度依赖于建设性的证据。通过大型未经测试的操作员组合的判断效率低。在各种逻辑系统中提出的大量潜在运算符给出，需要一种用于其功能完整性的一般验证方法。本文为功能完整性提供了普遍的验证。首先，我们提出了两个抽象运营商$ \ wideHat {r} $和$ \ breve {r} $，两者均没有固定的形式，仅由几个弱约束来定义。特别是，$ \ wideHat {r} _ {\ geq} $和$ \ breve {r} _ {\ geq} $是定义的抽象运营商，该操作员定义了总订单关系$ \ geq $。然后，我们证明任何操作员设置$ \ mathfrak {r} $在功能上是在功能上完成的，并且仅当它可以表示复合操作员$ \ wideHat {r} _ {\ geq} \ circ \ circ \ breve {r} _ {\ geq} $ {\ geq} $或$ \ breve {r} _ {\ geq} \ circ \ wideHat {r} _ {\ geq} $。否则，确定$ \ mathfrak {r} $在功能上是不完整的。该理论通常可以应用于任何未经测试的操作员设置，以确定其功能是否完整。
An operator set is functionally incomplete if it can not represent the full set $\lbrace \neg,\vee,\wedge,\rightarrow,\leftrightarrow\rbrace$. The verification for the functional incompleteness highly relies on constructive proofs. The judgement with a large untested operator set can be inefficient. Given with a mass of potential operators proposed in various logic systems, a general verification method for their functional completeness is demanded. This paper offers an universal verification for the functional completeness. Firstly, we propose two abstract operators $\widehat{R}$ and $\breve{R}$, both of which have no fixed form and are only defined by several weak constraints. Specially, $\widehat{R}_{\geq}$ and $\breve{R}_{\geq}$ are the abstract operators defined with the total order relation $\geq$. Then, we prove that any operator set $\mathfrak{R}$ is functionally complete if and only if it can represent the composite operator $\widehat{R}_{\geq}\circ\breve{R}_{\geq}$ or $\breve{R}_{\geq}\circ\widehat{R}_{\geq}$. Otherwise $\mathfrak{R}$ is determined to be functionally incomplete. This theory can be generally applied to any untested operator set to determine whether it is functionally complete.
