Taking the order dual of a boolean algebra gives a boolean algebra, but taking the order dual of a Heyting algebra does not give a Heyting algebra. To fix this, one can introduce an exclusion operator to be the order dual of the Implication. The extension given by introducing such an exclusion is called /quot;bi-intuitionistic logic/quot;.

Bi-intuitionistic logic was established by Cecylia Rauser in the 1970s, but her work has many issues. For example there have been many contradictory claims about the deduction theorem in her work. To fix these issues, Gore and Shillito split bi-intuitionistic logic into two distinct logics, called /quot;strong bi-intuitionistic logic/quot; and /quot;weak bi-intuitionistic logic/quot;.

This logic has gone on to be studied from a proof theoretic and Kripke semantics perspective, but no algebraic semantics has been established for these logics.

This presentation discusses how I established algebraic semantics for these logics, using the framework of Abstract Algebraic Logic to structure our results, as well as leveraging this framework to gain new results about these logics.