package logtk
-
logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
LogtkTransformations on LogtkFormulas and Terms
type term = LogtkFOTerm.ttype form = LogtkFormula.FO.tProvides some transformations on formulas, and sets of formulas. LogtkTransformations include definition expansion and term rewriting
type t = | RwTerm of LogtkRewriting.TRS.t| RwForm of LogtkRewriting.FormRW.t| Tr of string * form -> form list(*the function can return a conjunction of formulas. The string is a short name/description of the transformation
*)
type transformation = tval of_term_rules_seq : (term * term) Sequence.t -> tval of_form_rules_seq : (term * form) Sequence.t -> tval open_and : ttransformation that opens outermost "and" connectives
val remove_trivial : tTranformation that removes trivial formulas
val fmt : Format.formatter -> t -> unitLogtkTransformation DAG
Abstraction over formulas with additional information. A FORM.t contains a formula, and is built from parent formula wrappers upon a transformation.
module type FORM = sig ... endThis module provides an infrastructure to efficiently compute the fixpoint of a set of transformations on a set of formulas. LogtkFormulas form a DAG, whose edges go from a formula to the formulas it transforms into; result set is the set of leaves reachable from the initial formulas.
module type DAG = sig ... end