package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Reduction to CNF and simplifications

package logtk

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Pos
  - Seq
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
- LogtkFormula
  - FO
    
    Base
    
    Seq
    
    TPTP
  - Make
    
    Base
    
    MyT
    
    Seq
    
    TPTP
    
    Seq
    
    TPTP
  - Map
    
    From
    
    Base
    
    Seq
    
    TPTP
    
    To
    
    Base
    
    Seq
    
    TPTP
  - S
    
    Base
    
    Seq
    
    TPTP
  - TERM
    
    Seq
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Pos
  - Seq
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    X
  - S
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Seq
  - TPTP
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Pos
  - Seq
  - Tbl
- LogtkSignature
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Seq
  - TPTP
    
    Arith
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Seq
  - TPTP
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Seq
  - Subst
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

Reduction to CNF and simplifications

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.

parameter 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.

DistributeExists if enabled, will distribute existential quantifiers over disjunctions. This can make skolem symbols smaller (smaller arity) but introduce more of them.
DisableRenaming disables formula renaming. Can re-introduce the worst-case exponential behavior of CNF.
InitialProcessing a simplification function that is called before CNF starts.
PostNNF transformation applied just after reduction to NNF. Its output must not break the NNF form (negation at root only).
PostSkolem transformation applied just after skolemization. It must not break skolemization nor NNF (no quantifier, no non-leaf negation).
DefLimit number of expected clauses above which a sub-formula is renamed (unless DisableRenaming is present).

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