minimal-logic
Part of this programme is a proof assistant. This lets you construct proofs of statements in minimal logic composably. It also keeps track of assumptions for you.
The Curry-Howard correspondence can be interpreted as an equivalence between types and deductions where for example the composition of functions corresponds to the composition of implications.
import Minimal
compose :: Deduction -> Deduction -> Proof
compose dAB dBC = do
-- get the antecedent of the conclusion of dAB
let (Implication a _) = conclusion dAB
dA <- assume a
dB <- implElim dA dAB
dC <- implElim dB dBC
dAC <- implIntro a dC
return dAC
pAB, pBC :: Proof
pAC = do
dAB <- pAB
dBC <- pBC
compose dAB dBC
The other half is the model checker. This lets you construct models and then check whether formulae are or are not forced by those models.
A model with only a single world is a model of classical logic.
import Model
exampleWorld :: World
exampleWorld = World
{ forcedProps = Set.singleton (Proposition "P")
, childWorlds = Set.empty
, name = "W"
}
example :: Model
example = Model
{ abnormalWorlds = Set.empty
, rootWorld = exampleWorld
}
Please contact about this project at miles@rout.nz.
minimal-logic
—The repository for this project