Conjunctive Normal Form Converter

Imports

import cats.implicits._
import axle.logic.FirstOrderPredicateLogic._

Example CNF conversion

import axle.logic.example.SamplePredicates._

val z = Symbol("z")
// z: Symbol = Symbol(z)

val s = ∃(z  Z, (A(z)  G(z))  (B(z)  H(z)))
// s: ∃ = ∃(
//   symbolSet = ElementOf(symbol = Symbol(z), set = Set(7, 8, 9)),
//   statement = Iff(
//     left = And(
//       left = A(symbols = List(Symbol(z))),
//       right = G(symbols = List(Symbol(z)))
//     ),
//     right = Or(
//       left = B(symbols = List(Symbol(z))),
//       right = H(symbols = List(Symbol(z)))
//     )
//   )
// )

val (cnf, skolemMap) = conjunctiveNormalForm(s)
// cnf: Statement = And(
//   left = Or(
//     left = ¬(statement = <function1>),
//     right = Or(
//       left = ¬(statement = <function1>),
//       right = Or(left = <function1>, right = <function1>)
//     )
//   ),
//   right = And(
//     left = Or(
//       left = And(
//         left = ¬(statement = <function1>),
//         right = ¬(statement = <function1>)
//       ),
//       right = <function1>
//     ),
//     right = Or(
//       left = And(
//         left = ¬(statement = <function1>),
//         right = ¬(statement = <function1>)
//       ),
//       right = <function1>
//     )
//   )
// )
// skolemMap: Map[Symbol, Set[Symbol]] = HashMap(
//   Symbol(sk2) -> Set(),
//   Symbol(sk6) -> Set(),
//   Symbol(sk7) -> Set(),
//   Symbol(sk3) -> Set(),
//   Symbol(sk4) -> Set(),
//   Symbol(sk1) -> Set(),
//   Symbol(sk0) -> Set(),
//   Symbol(sk5) -> Set()
// )
cnf.show
// res0: String = "((\u00acA(Symbol(sk0)) \u2228 (\u00acG(Symbol(sk1)) \u2228 (B(Symbol(sk2)) \u2228 H(Symbol(sk3))))) \u2227 (((\u00acB(Symbol(sk4)) \u2227 \u00acH(Symbol(sk5))) \u2228 A(Symbol(sk6))) \u2227 ((\u00acB(Symbol(sk4)) \u2227 \u00acH(Symbol(sk5))) \u2228 G(Symbol(sk7)))))"

skolemMap
// res1: Map[Symbol, Set[Symbol]] = HashMap(
//   Symbol(sk2) -> Set(),
//   Symbol(sk6) -> Set(),
//   Symbol(sk7) -> Set(),
//   Symbol(sk3) -> Set(),
//   Symbol(sk4) -> Set(),
//   Symbol(sk1) -> Set(),
//   Symbol(sk0) -> Set(),
//   Symbol(sk5) -> Set()
// )