Logic

WARNING: This stuff is quite old and needs an overhaul

Conjunctive Normal Form Converter

Imports

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

Example CNF conversion

import axle.logic.example.SamplePredicates._

val z = Symbol("z")

val s = ∃(z ∈ Z, (A(z) ∧ G(z)) ⇔ (B(z) ∨ H(z)))

val (cnf, skolemMap) = conjunctiveNormalForm(s)

cnf.show
// res1: String = "((¬A(Symbol(sk0)) ∨ (¬G(Symbol(sk1)) ∨ (B(Symbol(sk2)) ∨ H(Symbol(sk3))))) ∧ (((¬B(Symbol(sk4)) ∧ ¬H(Symbol(sk5))) ∨ A(Symbol(sk6))) ∧ ((¬B(Symbol(sk4)) ∧ ¬H(Symbol(sk5))) ∨ G(Symbol(sk7)))))"

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

Future Work

Redo all of this in terms of Abstract Algebra