A small propositional logic proof tree generator and prover.

Trees.swift

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))