Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
You can’t perform that action at this time.