Pith. sign in

REVIEW 4 major objections 5 minor 40 references

Paraconsistent Relations as a Variant of Kleene Algebras

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper introduces paraconsistent Kleene algebras with tests (PKAT), obtained by dropping the Boolean laws of non-contradiction and excluded middle from KAT, and proves that two parametric algebras of paraconsistent sets and relations…

desk verdict The PKAT concept is natural and the SetP proof holds, but the main relation theorem fails because the test carrier is not closed under the given negation. read the letter →

arxiv 2506.05840 v1 pith:SXPIAB3Z submitted 2025-06-06 cs.LO

Juliana Cunha , Alexandre Madeira , Luís S. Barbosa This is my paper
classification cs.LO MSC 03B5303G25
keywords paraconsistentKleenealgebrawithtestsrelationssetstwistedstructuresHeytingalgebrastransitionsystemsweightedprograms
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that Kleene algebra with tests can be weakened so that programs and assertions may yield vague or contradictory outcomes while keeping the algebraic core intact. The new structure, a paraconsistent Kleene algebra with tests (PKAT), keeps the Kleene algebra axioms and the test laws that make tests a distributive idempotent algebra, but deliberately rejects the law of non-contradiction and the law of excluded middle. The paper's main results are that two parametric models built from twisted structures over complete Heyting algebras (truth-value lattices in which meet distributes over arbitrary joins) satisfy the PKAT axioms: the algebra of paraconsistent sets $\mathrm{SetP}(\mathcal{T})$ and the algebra of paraconsistent relations $\mathrm{RelP}(\mathcal{K},\mathcal{T})$ with $\mathcal{T}\subseteq\mathcal{K}$. A sympathetic reader would care because this gives an equational, relation-based semantics for computations whose tests carry paired positive and negative evidence, with room for both inconsistency and vagueness.

What carries the argument

The load-bearing object is the twisted structure of a complete Heyting algebra $\mathcal{A}$: the product lattice $A\times A$ ordered by $(a,a')\preccurlyeq (b,b')$ iff $a\le b$ and $a'\ge b'$, with the two componentwise lattice operations flipped in the second component and an involution that swaps the two entries. Every paraconsistent set or relation assigns each state, or each pair of states, a pair $(a,b)$ of evidence weights, and the pointwise operations combine the two components in opposite directions, so contradictory pairs sit above the consistency line and vague pairs below it. The star operation is an arbitrary join of powers, and the proofs that it satisfies the Kleene unfolding and induction axioms use the infinite distributivity of meet over arbitrary joins (Properties (25)--(26)) together with the finite distributivity properties (22)--(24), all of which hold in complete Heyting algebras.

What would settle it

Take the three-element complete Heyting algebra $\mathbf{3}$ and a two-element state set $W$, enumerate all finitely many functions in $\mathrm{RelP}(\mathbf{3},\mathbf{3})$, and mechanically check axioms (10)--(13) using the paper's definitions of composition and star; a single violated axiom would refute Theorem 3, while a clean pass confirms the construction on the simplest non-Boolean case.

Watch

Extended reading notes

Core claim

The central discovery is that the step from KAT to a paraconsistent setting can be made by weakening only the test-level Boolean structure, not the Kleene algebra itself. The paper defines a PKAT as a Kleene algebra equipped with a subalgebra of tests satisfying axioms (14)--(19), namely commutativity, idempotence, double negation, and the two distributivity laws, while dropping axioms (20) and (21) (non-contradiction and excluded middle). It then proves Theorem 2 for paraconsistent sets over any complete Heyting algebra and Theorem 3 for paraconsistent relations over complete Heyting algebras $\mathcal{K}$ and $\mathcal{T}$ with $\mathcal{T}\subseteq\mathcal{K}$. In both models every program or test is a function to pairs $(a,b)$ in a twisted structure, where the first component is evidence for and the second evidence against, and the operations combine the two components in opposite directions, so the models represent inconsistent evidence without collapsing.

Load-bearing premise

The load-bearing premise is that the truth-value lattices are complete Heyting algebras, so that meet distributes over arbitrary joins; if that distributivity fails, the star-related axioms and the test distributivity proofs in Theorems 2 and 3 may stop going through.

Editorial extensions

If this is right

  • Since any KAT is a PKAT (Theorem 1), every ordinary KAT equation remains valid in the paraconsistent setting; the weakening is conservative.
  • Theorem 2 makes the pointwise algebra of paraconsistent sets over any complete Heyting algebra a PKAT, so vague and inconsistent membership can be reasoned about with the regular operations.
  • Theorem 3 makes paraconsistent relations a PKAT: composition is weighted relational composition with a join over intermediate states, and the star is the reflexive-transitive closure in the paired-evidence sense, so conditionals and while loops keep their standard algebraic definitions.
  • The parametricity over arbitrary complete Heyting algebras means the same PKAT axioms cover Boolean, three-valued, and real-interval truth spaces, while tests remain a subalgebra of programs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The authors leave implicit that the order $(a,b)\preccurlyeq (c,d)$ is the interval order on evidence weights: reading the pair as the interval $[b,a]$, PKAT is an interval-valued semantics for programs, not merely a labelled two-valued one.
  • A concrete testable extension is to instantiate the parameters with finite Heyting chains such as the three-element algebra and use the finite carrier of $\mathrm{RelP}(\mathcal{K},\mathcal{T})$ as a decidable model-checking domain for weighted programs with contradictory evidence.
  • If the authors' proposed Hoare-style encoding $b\cdot p\preccurlyeq b\cdot p\cdot c$ is adopted, PKAT will yield a graded correctness notion: not just whether a program is correct, but how much positive and negative evidence its execution leaves for the postcondition.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper proposes a paraconsistent variant of Kleene algebras with tests, called PKAT, obtained from KAT by dropping the Boolean laws of non-contradiction (20) and excluded middle (21). It defines two parametric families of algebras over twisted structures built from complete Heyting algebras: paraconsistent sets SetP(T) and paraconsistent relations RelP(K,T), and claims in Theorems 2 and 3 that each satisfies the PKAT axioms (1)-(19). The paper is motivated by applications to vague or inconsistent program behaviour, following earlier work on paraconsistent transition systems.

Significance. If the main theorems were correct, the paper would provide a clean algebraic semantics for paraconsistent tests and programs, extending a line of work on PLTS and opening the way to Hoare-style reasoning for paraconsistent and vague computations. The PKAT definition itself is a natural and potentially useful weakening of KAT. The paper is generally readable and the algebraic intuition is well explained. However, the two main existence theorems contain substantial technical gaps: the test carrier of RelP(K,T) is not closed under the displayed negation, the star proofs rely on an infinite distributivity law that is not guaranteed by the stated hypotheses, and the inclusion of tests into relations is not shown to be algebraically compatible. These issues are not merely cosmetic; they affect the central claim that SetP(T) and RelP(K,T) form PKATs as stated.

major comments (4)
  1. [Definition 7 and Theorem 3] The negation operation is not well defined on the test carrier of RelP(K,T). Tests are defined as functions t: W×W -> T×T with t(u,v) = (0,1) whenever u ≠ v, and negation is defined pointwise by (-t)(u,v) = /sslash(t(u,v)). For u ≠ v, (-t)(u,v) = /sslash(0,1) = (1,0), which violates the defining test condition. In particular, -Λ has off-diagonal value (1,0) and is not a test. Hence the two-sorted signature is ill-formed and Theorem 3 fails as written. This problem is independent of the T ⊆ K assumption; it already occurs when T = K. A repair, such as defining negation on the diagonal only and re-verifying the test axioms, would be a substantial revision rather than a local correction.
  2. [Theorems 2 and 3, proofs of Axioms (10)-(13)] The proofs of the star axioms move an infinite join across the twisted meet operation ^. For example, in the proof of Axiom (10) in Theorem 3, the step labelled "using Property (40)" transforms ⋁_u (R(w,u) ^ ⋁_n R^n(u,v)) into ⋁_n ⋁_u (R(w,u) ^ R^n(u,v)). In the twisted structure this equality requires, for the second coordinate, the dual infinite distributive law a' ⊔ (⋂_i b'_i) = ⋂_i (a' ⊔ b'_i). This law is not a consequence of completeness or of the Heyting algebra axioms; complete Heyting algebras that are locales need not satisfy it. Lemma 1 only lists the meet-over-join laws (25)-(26), and Lemma 2 only states finite distributivity. The same gap appears in Theorem 2. Thus the proofs do not establish Axioms (10)-(13) for arbitrary complete Heyting algebras as stated.
  3. [Definition 7 and Theorem 3] The hypothesis "T ⊆ K" is stated as containment of carrier sets, but for RelP(K,T) to be a two-sorted algebra with the test set included in the relation set, the operations +, ·, and - on tests must coincide with the restrictions of the corresponding operations on relations. This requires the twisted structure T to be a subalgebra of the twisted structure K, i.e. T should be a sub-Heyting-algebra of K (or at least closed under the operations of the twisted structures). The paper neither states nor proves such compatibility, and without it the inclusion of test functions into relation functions is not an algebraic embedding.
  4. [Theorem 3, proof of Axiom (14), steps (⋆) and (⋆⋆)] The proof asserts the biconditional "A ^ B ≠ (0,1) iff A ≠ (0,1) and B ≠ (0,1)" for elements of the twisted structure. This is false in general: in a Boolean lattice, two non-bottom elements can meet to bottom. While the particular conclusion that only the diagonal term contributes may be recoverable from the off-diagonal condition on tests, the argument as written contains an invalid step. The proof should be repaired by using the specific form of tests rather than the stated biconditional.
minor comments (5)
  1. [Definition 5] The definition states "B ⊆ T" but the intended inclusion is that the test carrier T is contained in the program carrier K; the symbol B is not otherwise introduced. This should be corrected, e.g. to "T ⊆ K".
  2. [Definition 7 and text before it] The paragraph before Definition 7 says the constants ⊘ and Λ are "the least and the greatest elements of T × T". Λ is not the greatest element of the full product T×T; it is the greatest element of the test set (the functions supported on the diagonal). The wording should be clarified.
  3. [Theorem 3, proof of Axiom (15)] The proof says "By Property (30) it is possible to show Axiom (15)", but Property (30) is idempotence of _, which does not obviously imply the distributivity law in Axiom (15). This likely refers to Property (41) or a combination of properties; the reference should be corrected.
  4. [Theorem 3, proof of Axiom (16)] There is a typo in the displayed line: "(t · t′)(u, v), = t(u, v) ^ t′(u, v)" contains an extra comma after the left-hand expression.
  5. [Lemma 1 and references] Properties (25)-(26) are cited to [18] and [8], but [18] is described as "submitted to a journal" and may not be publicly accessible. Since these properties are used in crucial infinitary steps, the paper would be stronger if the relevant proofs were included or if a more accessible reference were provided.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: PKAT is an explicit weakening of KAT and the examples are direct axiom verifications; the only self-citation supplies standard distributivity facts, not the target result.

full rationale

The paper's central derivations are direct verifications of axioms (1)-(19) for the two constructed algebras, not fitted predictions or results that assume their own conclusion. PKAT is introduced as an explicit weakening of KAT by dropping axioms (20) and (21), and Theorems 2 and 3 check the remaining axioms against pointwise definitions over twisted structures. No parameter is fitted to the target identities, and no axiom is used to prove itself. The main self-citation occurs in Lemma 1, where properties (22)-(24) are attributed to the authors' submitted work [18] and properties (25)-(26) to the external reference [8]. These are standard complete-Heyting-algebra distributivity facts used in star-axiom manipulations; they do not assume the PKAT axioms or the theorems being proved, so the self-citation is not load-bearing in a circular sense. A separate, non-circular correctness concern should be flagged: in Definition 7, the test carrier is not closed under the pointwise negation t(u,v) = /sslash t(u,v), because /sslash(0,1) = (1,0), so the negated test violates the defining condition t(u,v) = (0,1) for u != v. The proof of Theorem 3 states that Axiom (18) is 'similar to Theorem 2' without verifying this closure. This is a mathematical defect in the example, not a circular derivation, and therefore it does not raise the circularity score beyond the minor self-citation concern.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The PKAT construction adds no fitted free parameters. The central theorems rest on the standard theory of complete Heyting algebras and Kalman twist structures, plus the new PKAT definition itself. The main domain assumption is that truth values form a complete Heyting algebra (a frame), which is inherited from the authors' PLTS program.

assumptions (4)
  • domain assumption Complete Heyting algebras are used as the source of truth values (Definition 3); their meet distributes over arbitrary joins (Lemma 1, Properties (25)-(26)).
    The proofs of Theorems 2 and 3 rely on this infinite distributivity to verify the star axioms (10)-(13). If the lattice were only complete, the star might not behave as required.
  • standard math The twisted structure A × A with operations ^ and _ is a distributive lattice with a De Morgan involution (Lemma 2).
    This is a known result from Kalman (1958) and Kracht (1998); the paper proves the properties explicitly.
  • ad hoc to paper PKAT is defined as a KAT whose tests satisfy axioms (14)-(19) but not necessarily (20)-(21) (Definition 5).
    This is the new definition introduced by the paper; the theorems verify that the example algebras satisfy it.
  • domain assumption For RelP(K,T), the test truth-value lattice T is a subset of the program truth-value lattice K (Theorem 3).
    This inclusion is needed so that tests (T × T-valued) are also a subset of programs (K × K-valued).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Paraconsistent Relations as a Variant of Kleene Algebras." pith.science (2026). https://pith.science/paper/SXPIAB3Z

@misc{pith2026250605840,
  author       = {Pith},
  title        = {Pith review of: Paraconsistent Relations as a Variant of Kleene Algebras},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SXPIAB3Z}},
  note         = {Machine review of arXiv:2506.05840}
}
read the original abstract

Kleene algebras (KA) and Kleene algebras with tests (KAT) provide an algebraic framework to capture the behavior of conventional programming constructs. This paper explores a broader understanding of these structures, in order to enable the expression of programs and tests yielding vague or inconsistent outcomes. Within this context, we introduce the concept of a paraconsistent Kleene Algebra with tests (PKAT), capable of capturing vague and contradictory computations. Finally, to establish the semantics of such a structure, we introduce two algebras parametric on a class of twisted structures. We believe this sort of structures, for their huge flexibility, have an interesting application potential.

Figures

Figures reproduced from arXiv: 2506.05840 by the authors.

Figure 1
Figure 1. The vagueness-inconsistency square These pairs of weights express different behaviors: • inconsistency, when the positive and negative weights are contradictory,i.e., they sum to a value greater than 1, this corresponds to the upper triangle in [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

40 extracted references · 33 canonical work pages

  1. [18]

    Barbosa (Ava ilable here): Paraconsistent transition structures: compositional principles and a modal logic

    Juliana Cunha, Alexandre Madeira & Luis S. Barbosa (Ava ilable here): Paraconsistent transition structures: compositional principles and a modal logic . (submitted to a journal)

    work page

  2. [1]

    Jair Minoro Abe, Cl´ audio Rodrigo Torres, Germano Lambe rt-Torres, Jo˜ ao In´ acio da Silva Filho & Helga Gonzaga Martins (2007): Paraconsistent Autonomous Mobile Robot Emmy III . In Germano Lambert- Torres, Jair Minoro Abe, Jo˜ ao In´ acio da Silva Filho & HelgaGonzaga Martins, editors: Advances in Techno- logical Applications of Logical and Intelligent...

    work page 2007

  3. [2]

    Juan Carlos Agudelo & Walter Alexandre Carnielli (2010) : Paraconsistent Machines and their Relation to Quantum Computing . J. Log. Comput. 20(2), pp. 573–595. Available at https://doi.org/10.48550/ arXiv.0802.0150

    work page Pith review arXiv doi:10.48550/arxiv.0802.0150 2010

  4. [3]

    Intelligent Systems Reference Library 110, Springer, doi:10.1007/978-3-319-40418-9

    Seiki Akama, editor (2016): T owards Paraconsistent Engineering. Intelligent Systems Reference Library 110, Springer, doi:10.1007/978-3-319-40418-9

    work page doi:10.1007/978-3-319-40418-9 2016

  5. [4]

    Backhouse, Dexter Kozen & Bernhard M¨ oller (20 02): Applications of Kleene Algebra (Dagstuhl Seminar 01081)

    Roland C. Backhouse, Dexter Kozen & Bernhard M¨ oller (20 02): Applications of Kleene Algebra (Dagstuhl Seminar 01081) . Dagstuhl Seminar Report 298, Schloss Dagstuhl – Leibniz-Z entrum f¨ ur Informatik, Dagstuhl, Germany, doi:10.4230/DagSemRep.298

    work page doi:10.4230/dagsemrep.298

  6. [5]

    Lu´ ıs Soares Barbosa & Alexandre Madeira (2023): Capturing Qubit Decoherence through Paraconsistent Transition Systems. In Shigeru Chiba, Y ouyou Cong & Elisa Gonzalez Boix, editors: Companion Proceedings of the 7th International Conference on the Art, Science, and Engineering of Programming, Programming 2023, Tokyo, Japan, March 13-17, 2023 , ACM, pp. 1...

    arXiv 2023

  7. [6]

    ESSLLI course notes

    Nick Bezhanishvili & Dick de Jongh (2005): Intuitionistic Logic . ESSLLI course notes . Available at https://www.math.uni-hamburg.de/en/personen/khomskii/intuitionistic/PP-2006-25. text.pdf

    work page 2005

  8. [7]

    Francis Borceux (1994): Locales, p. 1–86. Encyclopedia of Mathematics and its Appli- cations, Cambridge University Press. Available at https://www.cambridge.org/core/books/ handbook-of-categorical-algebra/A0B8285BBA900AFE85E ED8C971E0DE14

    work page 1994

Show all 40 references
  1. [8]

    Journal of Logic and Computation 21(5), pp

    F´ elix Bou, Francesc Esteva, Llu´ ıs Godo & Ricardo OscarRodr´ ıguez (2009):On the Minimum Many-V alued Modal Logic over a Finite Residuated Lattice. Journal of Logic and Computation 21(5), pp. 739–790, doi: 10. 1093/logcom/exp062

    2009

  2. [9]

    algebra universalis 71, doi:10.1007/s00012-014-0265-4

    Manuela Busaniche & Roberto Cignoli (2014): The subvariety of commutative residuated lattices represented by twist-products. algebra universalis 71, doi:10.1007/s00012-014-0265-4

    2014 doi

  3. [10]

    Stud Logica 110(4), pp

    Manuela Busaniche, Nikolaos Galatos & Miguel Andr´ es M arcos (2022): Twist Structures and Nelson Conu- clei. Stud Logica 110(4), pp. 949–987, doi: 10.1007/S11225-022-09988-Z

    2022 doi

  4. [11]

    Menni & Marta Sagastume (2008): On Some Categories of Involutive Centered Residu- ated Lattices

    Jose Castiglioni, M. Menni & Marta Sagastume (2008): On Some Categories of Involutive Centered Residu- ated Lattices. Studia Logica 90, pp. 93–124, doi: 10.1007/s11225-008-9145-2

    2008 doi

  5. [12]

    Maria Luisa Dalla Chiara & Roberto Giuntini (2000): Paraconsistent ideas in quantum logic . Synth. 125(1- 2), pp. 55–68. Available at https://doi.org/10.1023/A:1005296018904

    2000 doi

  6. [13]

    Conway (1971): Regular Algebra and Finite Machines

    J.H. Conway (1971): Regular Algebra and Finite Machines. Chapman and Hall mathematics series, Chapman and Hall. Available at https://books.google.pt/books?id=xBXvAAAAMAAJ

    1971

  7. [14]

    Newton C. A. Costa & Walter A. Carnielli (1986): On Paraconsistent Deontic Logic . Philosophia 16(3-4), pp. 293–305, doi: 10.1007/bf02379748

    1986 doi

  8. [15]

    Newton C. A. Da Costa & E. H. Alves (1977): A Semantical Analysis of the Calculi C N. Notre Dame Journal of Formal Logic 18(4), pp. 621–630, doi: 10.1305/ndjfl/1093888132. 146 Paraconsistent Relations as a V ariant of Kleene Algebras

    1977

  9. [16]

    In Andrzej Indrzejczak & Michal Zawidzki, editors: 10th International Conference on Non-Classical Logics

    Ana Cruz, Alexandre Madeira & Lu´ ıs Soares Barbosa (2022): A Logic for Paraconsistent Transition Systems. In Andrzej Indrzejczak & Michal Zawidzki, editors: 10th International Conference on Non-Classical Logics. Theory and Applications , EPTCS 358, pp. 270–284. Available at h...

    2022 doi

  10. [17]

    Ana Cruz, Alexandre Madeira & Lu´ ıs Soares Barbosa (202 2): Paraconsistent Transition Systems. In Daniele Nantes-Sobrinho & Pascal Fontaine, editors: Proceedings 17th International Workshop on Logical and Se- mantic Frameworks with Applications, LSFA 2022, Belo Horiz onte, Br...

    2022 doi

  11. [19]

    Juliana Cunha, Alexandre Madeira & Lu´ ıs Soares Barbos a (2023): Stepwise Development of Paraconsistent Processes. In Cristina David & Meng Sun, editors: Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Bristol, UK, July 4-6, 2023, Procee...

    2023 doi

  12. [20]

    Juliana Cunha, Alexandre Madeira & Lu´ ıs Soares Barbos a (2023): Structured Specification of Paraconsis- tent Transition Systems. In Hossein Hojjat & Erika ´Abrah´ am, editors:Fundamentals of Software Engineering - 10th International Conference, FSEN 2023, Tehran, Iran, M ay 4...

    2023

  13. [21]

    Expert Systems with Applications 187, p

    Hyghor Miranda Cˆ ortes, Paulo Eduardo Santos & Jo˜ ao In ´ acio da Silva Filho (2022): Monitoring electrical systems data-network equipment by means of Fuzzy and Paraco nsistent Annotated Logic . Expert Systems with Applications 187, p. 115865. Available at https://doi.org/10...

    2022

  14. [22]

    Michael Dunn & Greg Restall (2002): Relevance Logic. In D. Gabbay & F. Guenthner, editors: Handbook of Philosophical Logic, Kluwer Academic Publishers, pp. 1–128. Available at https://doi.org/10.1007/ 978-94-017-0452-6

    2002

  15. [23]

    Leandro Gomes, Alexandre Madeira & Lu´ ıs Soares Barbos a (2019): Generalising KAT to V erify W eighted Computations. Sci. Ann. Comput. Sci. 29(2), pp. 141–184, doi: 10.7561/SACS.2019.2.141

    2019 doi

  16. [24]

    MIT Press, Cambridge, MA, USA, doi:10.7551/mitpress/2516.001.0001

    David Harel, Jerzy Tiuryn & Dexter Kozen (2000): Dynamic Logic . MIT Press, Cambridge, MA, USA, doi:10.7551/mitpress/2516.001.0001

    2000 doi

  17. [25]

    Kalman (1958): Lattices with involution

    John A. Kalman (1958): Lattices with involution. Transactions of the American Mathematical Society 87, pp. 485–491, doi: 10.1090/S0002-9947-1958-0095135-X . Available at https://api.semanticscholar. org/CorpusID:53394259

    1958 doi

  18. [26]

    S. C. Kleene (1956): Representation of Events in Nerve Nets and Finite Automata , pp. 3–42. Princeton University Press, Princeton. Available at https://doi.org/10.1515/9781400882618-002

    1956 doi

  19. [27]

    Kozen (1992): The Design and Analysis of Algorithms

    D. Kozen (1992): The Design and Analysis of Algorithms . Monographs in Computer Science, Springer New Y ork, NY . Available athttps://doi.org/10.1007/978-1-4612-4400-4

    1992 doi

  20. [28]

    Kozen (1994): A Completeness Theorem for Kleene Algebras and the Algebra o f Regular Events

    D. Kozen (1994): A Completeness Theorem for Kleene Algebras and the Algebra o f Regular Events . In- formation and Computation 110(2), pp. 366–390, doi: 10.1006/inco.1994.1037. Available at https:// www.sciencedirect.com/science/article/pii/S0890540184710376

    1994

  21. [29]

    ACM Trans

    Dexter Kozen (1997): Kleene Algebra with T ests. ACM Trans. Program. Lang. Syst. 19(3), pp. 427–443, doi:10.1145/256167.256195

    1997

  22. [30]

    In John Lloyd, V eronica Dahl, Ulrich Furbach, Manfred Kerb er, Kung-Kiu Lau, Catuscia Palamidessi, Lu´ ıs Moniz Pereira, Y ehoshua Sagiv & Peter J

    Dexter Kozen & Maria-Cristina Patron (2000): Certification of Compiler Optimizations Using Kleene Alge- bra with T ests. In John Lloyd, V eronica Dahl, Ulrich Furbach, Manfred Kerb er, Kung-Kiu Lau, Catuscia Palamidessi, Lu´ ıs Moniz Pereira, Y ehoshua Sagiv & Peter J. Stuckey,...

    2000

  23. [31]

    Journal of Philosophical Logic 27(1), pp

    Marcus Kracht (1998): On Extensions of Intermediate Logics by Strong Negation . Journal of Philosophical Logic 27(1), pp. 49–73, doi: 10.1023/A:1004222213212

    1998 doi

  24. [32]

    Kuich & A

    W . Kuich & A. Salomaa (1986): Semirings, Automata, Languages . EA TCS monographs on theoretical computer science, Springer-V erlag. Available at https://doi.org/10.1007/978-3-642-69959-7

    1986 doi

  25. [33]

    In Clifford H

    V aughan Pratt (1990): Dynamic algebras as a well-behaved fragment of relation alg ebras. In Clifford H. Bergman, Roger D. Maddux & Don L. Pigozzi, editors: Algebraic Logic and Universal Algebra in Com- puter Science, Springer New Y ork, New Y ork, NY , pp. 77–110. Available a...

    1990

  26. [34]

    Quantum 2, p

    John Preskill (2018): Quantum Computing in the NISQ era and beyond . Quantum 2, p. 79, doi: 10.22331/ q-2018-08-06-79

    2018

  27. [35]

    In Dov M

    Graham Priest (2007): Paraconsistency and dialetheism . In Dov M. Gabbay & John Woods, editors: The Many V alued and Nonmonotonic Turn in Logic, Handbook of the History of Logic 8, Elsevier, pp. 129–204. Available at https://doi.org/10.1016/S1874-5857(07)80006-9

    2007 doi

  28. [36]

    Rasiowa & R

    H. Rasiowa & R. Sikorski (1970): The Mathematics of Metamathematics . Monografie matematyczne, PWN- Polish Scientific Publishers. Available at https://books.google.pt/books?id=vtRGtQEACAAJ

    1970

  29. [37]

    Ukrainskii Matematicheskii Zhurnal 16(1)

    V alentin N Redko (1964): On defining relations for the algebra of regular events . Ukrainskii Matematicheskii Zhurnal 16(1)

    1964

  30. [38]

    Arto Salomaa (1966): Two Complete Axiom Systems for the Algebra of Regular Events . J. ACM 13(1), pp. 158–169, doi: 10.1145/321312.321326

    1966

  31. [39]

    The Journal of Symbolic Logic 6(3), pp

    Alfred Tarski (1941): On the Calculus of Relations . The Journal of Symbolic Logic 6(3), pp. 73–89, doi: 10. 2307/2268577. Available at http://www.jstor.org/stable/2268577

    1941

  32. [40]

    Wille (2006): Minimal V arieties of Involutive Residuated Lattices

    Constantine Tsinakis & Annika M. Wille (2006): Minimal V arieties of Involutive Residuated Lattices. Studia Logica 83(1), pp. 407–423, doi: 10.1007/s11225-006-8311-7

    2006 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.