Conditional Logic as a Short-Circuit Logic

Three-valued conditional logic (CL), defined by Guzm ́an and Squier (1990) and based on McCarthy’s noncommutative connectives, axiomatises a short-circuit logic (SCL), that is, a logic that prescribes shortcircuit evaluation of conjunction and disjunction. CL defines more identities than three-valued MSCL (Memorising SCL, which also has a two-valued variant). This follows from the fact that the definable connective that prescribes full left-sequential conjunction is commutative in CL. We observe that CL also has a two-valued variant of which the full left-sequential connectives and negation define a commutative logic that is weaker than propositional logic because the absorption laws do not hold. Next, we show that the original, equational axiomatisation of CL is not independent and give several alternative, independent axiomatisations. Finally, we show that in CL, the full left-sequential connectives and negation define Bochvar’s three-valued logic. The paper ends with an appendix on the use of Prover9 and Mace4.

Authors

Institutions

Publication Details

Journal
Scientific Annals of Computer Science
Published
2025-09-29
DOI
https://doi.org/10.47743/sacs.2025.2.161
Citations
2
Primary Topic
Logic, programming, and type systems
Type
article
Field-Weighted Citation Impact
4.96
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Conditional Logic as a Short-Circuit Logic

J.A. Bergstra, Alban Ponse
2 citations
Scientific Annals of Computer Science
Logic, programming, and type systems
4.96
article

Conditional Logic as a Short-Circuit Logic

J.A. Bergstra, Alban Ponse
article en
2 citations

Abstract

Three-valued conditional logic (CL), defined by Guzm ́an and Squier (1990) and based on McCarthy’s noncommutative connectives, axiomatises a short-circuit logic (SCL), that is, a logic that prescribes shortcircuit evaluation of conjunction and disjunction. CL defines more identities than three-valued MSCL (Memorising SCL, which also has a two-valued variant). This follows from the fact that the definable connective that prescribes full left-sequential conjunction is commutative in CL. We observe that CL also has a two-valued variant of which the full left-sequential connectives and negation define a commutative logic that is weaker than propositional logic because the absorption laws do not hold. Next, we show that the original, equational axiomatisation of CL is not independent and give several alternative, independent axiomatisations. Finally, we show that in CL, the full left-sequential connectives and negation define Bochvar’s three-valued logic. The paper ends with an appendix on the use of Prover9 and Mace4.

Scientific Annals of Computer ScienceVol. 35(2)
University of Amsterdam (NL)
Openalex Percentile: Top 5%
Logic, programming, and type systems
4.96
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Conditional Logic as a Short-Circuit Logic — J.A. Bergstra, Alban Ponse · Scientific Annals of Computer Science (2025) | TGRS Research Map | TGRS