-
-
Save alemar11/ecc76bcc80962fdd8605 to your computer and use it in GitHub Desktop.
A small propositional logic proof tree generator and prover.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
//: 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