Skip to content

Instantly share code, notes, and snippets.

@alemar11
Forked from CodaFi/Trees.swift
Created October 27, 2015 22:08
Show Gist options
  • Save alemar11/ecc76bcc80962fdd8605 to your computer and use it in GitHub Desktop.
Save alemar11/ecc76bcc80962fdd8605 to your computer and use it in GitHub Desktop.
A small propositional logic proof tree generator and prover.
//: 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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment