# HL Formulas and Clauses

function NEGATED? : (form)
Assuming FORM is a valid CycL formula, return T IFF it is negated.
FORM must satisfy EL-FORMULA-P.
Single value returned satisfies BOOLEANP.

function NEGATE : (form)
Assuming FORM is a valid CycL formula, return a negated version of it.
FORM must satisfy EL-FORMULA-P.
Single value returned satisfies EL-FORMULA-P.

function CLAUSE-P : (object)
Returns T iff OBJECT is either a CNF or DNF clause.
Single value returned satisfies BOOLEANP.

function SENSE-P : (object)
Return T iff OBJECT is a valid CycL literal sense
:neg or :pos.
Single value returned satisfies BOOLEANP.

function MAKE-CLAUSE : (neg-lits pos-lits)
Construct a clause from NEG-LITS and POS-LITS, each of which are lists of literals.
NEG-LITS must satisfy LISTP.
POS-LITS must satisfy LISTP.
Single value returned satisfies CLAUSE-P.

function NEG-LITS : (clause)
Return the neg-lits of CLAUSE.
CLAUSE must satisfy CLAUSE-P.
Single value returned satisfies LISTP.

function POS-LITS : (clause)
Return the pos-lits of CLAUSE.
CLAUSE must satisfy CLAUSE-P.
Single value returned satisfies LISTP.

function CLAUSE-EQUAL : (clause1 clause2)
Return T iff CLAUSE1 and CLAUSE2 are both equivalent clauses.
Single value returned satisfies BOOLEANP.

function EMPTY-CLAUSE : ()
Return the empty clause.
Single value returned satisfies CLAUSE-P.

function EMPTY-CLAUSE? : (clause)
Return T iff CLAUSE is empty.
CLAUSE must satisfy CLAUSE-P.
Single value returned satisfies BOOLEANP.

function CLAUSE-LITERAL : (clause sense num)
Return literal in CLAUSE specified by SENSE and NUM.
SENSE must be either :pos or :neg.
CLAUSE must satisfy CLAUSE-P.
SENSE must satisfy SENSE-P.
NUM must satisfy INTEGERP.

function CLAUSE-WITHOUT-LITERAL : (clause sense num)
Return a new clause which is CLAUSE without the literal specified by SENSE and NUM.
SENSE must be either :pos or :neg.
CLAUSE must satisfy CLAUSE-P.
SENSE must satisfy SENSE-P.
NUM must satisfy INTEGERP.
Single value returned satisfies CLAUSE-P.

function GROUND-CLAUSE-P : (clause)
Return T iff CLAUSE is a ground clause.
Single value returned satisfies BOOLEANP.

function CNF-P : (object)
Returns T iff OBJECT is a canonicalized CycL formula in conjunctive normal form.
Single value returned satisfies BOOLEANP.

function GAF-CNF? : (cnf)
Return T iff CNF is a cnf representation of a gaf formula.
Single value returned satisfies BOOLEANP.

function CNF-FORMULA : (cnf &optional truth)
Return a readable formula of CNF
TRUTH only gets looked at for ground, single pos lit cnfs
in which case TRUTH gives the truth of the gaf.
CNF must satisfy CNF-P.
TRUTH must satisfy TRUTH-P.
Single value returned satisfies EL-FORMULA-P.

function CNF-FORMULA-FROM-CLAUSES : (cnf-clauses)
Return a readable formula from a list of CNF-CLAUSES.
CNF-CLAUSES must satisfy LISTP.
Single value returned satisfies EL-FORMULA-P.

function DNF-FORMULA : (dnf)
Return a readable formula of DNF.
Single value returned satisfies EL-FORMULA-P.

function DNF-FORMULA-FROM-CLAUSES : (dnf-clauses)
Return a readable formula from a list of DNF-CLAUSES.
DNF-CLAUSES must satisfy LISTP.
Single value returned satisfies EL-FORMULA-P.

function ATOMIC-CLAUSE-P : (clause)
Return T iff CLAUSE is an atomic clause.
Single value returned satisfies BOOLEANP.

function HL-TERM-P : (obj)
Returns T if the OBJ is a valid CycL HL term.
Single value returned satisfies BOOLEANP.