A small propositional logic proof tree generator and prover.

Trees.swift

//: Playground - noun: a place where people can play
//: Prop 'til you Drop

indirect enum Formula : CustomStringConvertible {
    case Var(String)
    case Or(Formula, Formula)
    case And(Formula, Formula)
    case Imply(Formula, Formula)
    case BiImply(Formula, Formula)
    case Negate(Formula)
	
	var description : String {
		switch self {
		case .Var(let p):
			return p
		case .And(let p, let q):
			return "(\(p) /\\ \(q))"
		case .Or(let p, let q):
			return "(\(p) \\/ \(q))"
		case .Imply(let p, let q):
			return "(\(p) -> \(q))"
		case .BiImply(let p, let q):
			return "(\(p) <-> \(q))"
		case .Negate(let p):
			return "¬\(p)"
		}
	}
}

indirect enum Tree : CustomStringConvertible {
    case Invalid
    case Proved
    case Derive([Formula], Tree)
    case Split(left : ([Formula], Tree), right : ([Formula], Tree))
	
	var description : String {
		switch self {
		case .Invalid:
			return "🚫"
		case .Proved:
			return "✅"
		default:
			return "..."
		}
	}
}

enum Prop {
    case True(String)
    case False(String)
}

extension Array {
    public func find(f : Element -> Bool) -> Element? {
        for x in self {
            if f(x) {
                return .Some(x)
            }
        }
        return .None
    }
}

func prove(flst : [Formula], r : Formula) -> Tree {
    let sig = [.Negate(r)] + flst
    return .Derive(sig, deriveTree(sig, props: []))
}

func contradictionExists(p : Prop, props : [Prop]) -> Bool {
    return props.find({ q in
        switch (p, q) {
        case let (.True(a), .False(b)):
            return a == b
        case let (.False(a), .True(b)):
            return a == b
        default:
            return false
        }
    }) != nil
}

func deriveTree(s : [Formula], props : [Prop]) -> Tree {
    if s.isEmpty {
        return .Proved
    } else if let t = s.first {
        let rest = Array(s[1..<s.endIndex])
        switch t {
        case let .And(p, q):
            return .Derive([p, q], deriveTree([p, q] + rest, props: props))
        case let .Or(p, q):
            return .Split(left: ([p], deriveTree([p] + rest, props: props)), right: ([q], deriveTree([q] + rest, props: props)))
        case let .Imply(p, q):
            return .Split(left: ([.Negate(p)], deriveTree([.Negate(p)] + rest, props: props)), right: ([q], deriveTree([q] + rest, props: props)))
        case let .BiImply(p, q):
            return .Split(left: ([p, q], deriveTree([p, q] + rest, props: props)), right: ([.Negate(p), .Negate(q)], deriveTree([.Negate(p), .Negate(q)] + rest, props: props)))
        case .Negate(.And(let p, let q)):
            return .Split(left: ([.Negate(p)], deriveTree([.Negate(p)] + rest, props: props)), right: ([.Negate(q)], deriveTree([.Negate(q)] + rest, props: props)))
        case .Negate(.Or(let p, let q)):
            return .Derive([.Negate(p), .Negate(q)], deriveTree([.Negate(p), .Negate(q)] + rest, props: props))
        case .Negate(.Imply(let p, let q)):
            return .Derive([p, .Negate(q)], deriveTree([p, .Negate(q)] + rest, props: props))
        case .Negate(.BiImply(let p, let q)):
            return .Split(left: ([p, .Negate(q)], deriveTree([p, .Negate(q)] + rest, props: props)), right: ([.Negate(p), q], deriveTree([.Negate(p), q] + rest, props: props)))
        case .Negate(.Negate(let p)):
            return .Derive([p], deriveTree([p] + rest, props: props))
        case let .Var(p):
            if contradictionExists(.True(p), props: props) {
                return .Invalid
            } else {
                return deriveTree(rest, props: [.True(p)] + props)
            }
        case .Negate(.Var(let p)):
            if contradictionExists(.False(p), props: props) {
                return .Invalid
            } else {
                return deriveTree(rest, props: [.False(p)] + props)
            }
        }
    }
    fatalError("Non-empty list was unable to produce a first element")
}

let or : Formula = .Or(.Var("P"), .Negate(.Var("Q")))
print(prove([], r: or))