Conjunctive Normal Form Converter

Imports

import axle.string
import axle.logic._
import FirstOrderPredicateLogic._

Example CNF conversion

import SamplePredicates._
// import SamplePredicates._

val s = ∃('z  Z, (A('z)  G('z))  (B('z)  H('z)))
// s: axle.logic.FirstOrderPredicateLogic.∃ = ∃(ElementOf('z,Set(7, 8, 9)),Iff(And(<function1>,<function1>),Or(<function1>,<function1>)))

val (cnf, skolemMap) = conjunctiveNormalForm(s)
// cnf: axle.logic.FirstOrderPredicateLogic.Statement = And(Or(¬(<function1>),Or(¬(<function1>),Or(<function1>,<function1>))),And(Or(And(¬(<function1>),¬(<function1>)),<function1>),Or(And(¬(<function1>),¬(<function1>)),<function1>)))
// skolemMap: Map[Symbol,Set[Symbol]] = Map('sk2 -> Set(), 'sk6 -> Set(), 'sk7 -> Set(), 'sk3 -> Set(), 'sk4 -> Set(), 'sk1 -> Set(), 'sk0 -> Set(), 'sk5 -> Set())
string(cnf)
// res0: String = ((¬A('sk0) ∨ (¬G('sk1) ∨ (B('sk2) ∨ H('sk3)))) ∧ (((¬B('sk4) ∧ ¬H('sk5)) ∨ A('sk6)) ∧ ((¬B('sk4) ∧ ¬H('sk5)) ∨ G('sk7))))

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