Over a year ago, I worked out a classical-Kleene combination logic that worked to preserve intuitionistic tautologies over the intuitionistic fragment with operators $\{ \neg, \vee, \wedge \}$, which works as follows:
I use $\{ 0, 1, 2 \}$ to correspond to false, unsure, and true, respectively. Kleene logic has no tautologies, so the move to grant it only intuitionistic tautologies was to do a move I called a "Gilvenko switch" (for the lemma in the theorem that bears his name). Propositional variables receive a unique truth-value column per the normal decision procedure for truth-table semantics for classical logic. When the proposition yields a classical contradiction, $1$ can switch to $0$.
It's a bottom-up procedure, with a structure containing a head Kleene value and a tail truth-table column for each unique atom. I'll give a relevant intuitionistic example below:
Procedure for $\neg \neg (A \vee \neg A)$:
- $\neg \neg ([1,10] \vee \neg [1,10])$, Assignment
- $\neg \neg ([1,10] \vee [1,01])$
- $\neg \neg [1,11]$, preserving that the LEM is not an intuitionistic tautology.
- $\neg \neg [1,1]$, Halving
- $\neg [1,0]$
- $\neg [0,0]$, Switch
- $[2,1]$, maintainting, true to Gilvenko's theorem, that the double-negated LEM is an intuitionistic tautology.
The problem is that this method can't prove $P \rightarrow P$ unless it's interpreted as $\neg (P \wedge \neg P)$. But, that translation allows the DNE -- $(\neg \neg P \rightarrow P)$, translated $\neg (\neg \neg P \wedge \neg P)$.
That's all to be expected, since $\rightarrow$ is independent of the other operators in intuitionistic logic, except $\neg A$ if $\bot$ is also operable, which it is in the above formulation (it's just $[0,0]$).
Most every intuitionistic decision procedure I've found is top-down (propositions-to-atomics), rather than bottom-up (atomics-to-propositions): Beth, Gödel–McKinsey–Tarski translation to S4, lax logic, HA, G4ip. Also, half of them are full-on theorem provers, which are massive overkill for my use case -- building a (barely started) programming language with an unsure value that adheres to intuitionistic constraints.
So, is there some means of amending another algorithm that would perform the inverse of the aforementioned "Gilvenko switch", meaning set criteria that would perform an analogous reduction and move $[1,1]$ to $[2,1]$? Is there any literature on things resembling such a proposal?
The most efficient decision procedure I've found is an $O(n \log{} n)$ here. The closest bottom-up approach I've seen is here.