system-lk

system-lk is a propositional theorem prover in Swift, based on Wang's Algorithm. I wrote system-lk to better understand the inference rules in sequent calculus after reading @joom's WangsAlgorithm.

Author

Mert Dumenci mert@dumenci.me

Usage

// Construct a `Sequent`.
let lawOfTheExcludedMiddle = Sequent(
    antecedents: [],
    consequents: [
        .Disjunction(
            .Atomic("x"),
            .Negation(.Atomic("x"))
        )
    ]
)

// Prove it using `prove`.
let proof = prove(sequent: lawOfTheExcludedMiddle)

Notes

Check out WangsAlgorithm for a much more complete version of this project. system-lk is heavily inspired by WangsAlgorithm, and doesn't implement half of its features: LaTeX proof output, parser for sequents, etc.