2022/03/17 by Dalia Papuc, Papuc, Dalia, Alban Ponse +1
Computer Science · #03C90 #F.3.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2203.09321
openalex publication_date 2022/03/17 · openalex created_date 2022/04/03 · openalex updated_date 2026/07/28
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.