A small propositional logic proof tree generator and prover.
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 let .Imply(.Imply(ss, sr), t2): | |
return "(\(ss) -> \(sr)) -> \(t2)" | |
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) | |
} | |
func prove(_ flst : [Formula], r : Formula) -> Tree { | |
let sig = [.Negate(r)] + flst | |
var props = [Prop]() | |
return .Derive(sig, deriveTree(sig, props: &props)) | |
} | |
func contradictionExists(_ p : Prop, props : [Prop]) -> Bool { | |
return props.first { 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(_ assumptions : [Formula], props : inout [Prop]) -> Tree { | |
guard let t = assumptions.first else { | |
return .Proved | |
} | |
let rest = Array(assumptions.dropFirst()) | |
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): | |
guard !contradictionExists(.True(p), props: props) else { | |
return .Invalid | |
} | |
props.append(.True(p)) | |
return deriveTree(rest, props: &props) | |
case .Negate(.Var(let p)): | |
guard !contradictionExists(.False(p), props: props) else { | |
return .Invalid | |
} | |
props.append(.False(p)) | |
return deriveTree(rest, props: &props) | |
} | |
} | |
let or : Formula = .Or(.Var("P"), .Negate(.Var("P"))) | |
let contra : Formula = .And(.Var("P"), .Negate(.Var("P"))) | |
dump(prove([], r: or)) | |
dump(prove([], r: contra)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment