论文标题
具有短路的双条件和NAND的非承诺命题逻辑
Non-commutative propositional logic with short-circuited biconditional and NAND
论文作者
论文摘要
短路评估表示命题连接的语义，其中仅当第一个参数不足以确定表达式值时，才能评估第二个参数。在编程中，短路评估被广泛使用，左序连词和脱节是原始的连接剂。我们考虑左序，非交互性命题逻辑，也称为MSCL（记忆的短路逻辑），并从先前发表的方程式公理化开始。首先，我们使用双条纹结缔组织的左序版本扩展了此逻辑，该版本允许MSCL的优雅的公理化。接下来，我们考虑NAND运算符（Sheffer Stroke）的左序版本，并再次对MSCL的相应变体提供了完整的，方便的公理化。最后，我们将这些逻辑系统在三个值的设置中以“未定义”为常量，并再次提供完整性结果。
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with left-sequential conjunction and disjunction as primitive connectives. We consider left-sequential, non-commutative propositional logic, also known as MSCL (memorising short-circuit logic), and start from a previously published, equational axiomatisation. First, we extend this logic with a left-sequential version of the biconditional connective, which allows for an elegant axiomatisation of MSCL. Next, we consider a left-sequential version of the NAND operator (the Sheffer stroke) and again give a complete, equational axiomatisation of the corresponding variant of MSCL. Finally, we consider these logical systems in a three-valued setting with a constant for `undefined', and again provide completeness results.
