Module Logtk.Cnf (.ml)

module Cnf: LogtkCnf

type form = LogtkFormula.FO.t 
type symbol = LogtkSymbol.t 

See "computing small normal forms", in the handbook of automated reasoning. All transformations are made on curried terms and formulas.
val is_cnf : form -> bool
Is the formula in CNF?
val is_lit : form -> bool
Literal?
val is_clause : form list -> bool
Is it a clause, ie a list of literals?
val miniscope : ?distribute_exists:bool -> form -> form
Apply miniscoping transformation to the term.
distribute_exists : see whether ?X:(p(X)|q(X)) should be transformed into (?X: p(X) | ?X: q(X)). Default: false
type clause = form list 
Basic clause representation, as list of literals
type options = 
| DistributeExists
| DisableRenaming
| InitialProcessing of (form -> form) (*
any processing, at the beginning
*)
| PostNNF of (form -> form) (*
any processing that keeps negation at leaves
*)
| PostSkolem of (form -> form) (*
must not introduce variables nor negations
*)

Options are used to tune the behavior of the CNF conversion.


val cnf_of : ?opts:options list ->
?ctx:LogtkSkolem.ctx -> form -> clause list
LogtkTransform the clause into proper CNF; returns a list of clauses. Options are used to tune the behavior.
val cnf_of_list : ?opts:options list ->
?ctx:LogtkSkolem.ctx -> form list -> clause list