Proof assistant

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

Model checker

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

Contact me

You can contact me about this project at