package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
Detect some specific formulas
type form = LogtkFormula.FO.t
type term = LogtkFOTerm.t
val is_definition : form -> (term * term) option

Check whether the clause defines a symbol, e.g. subset(X,Y) = \forall Z(Z in X -> Z in Y). It means the LHS is a flat symbol with variables, and all variables in RHS are also in LHS

val is_pred_definition : form -> (term * form) option

Check whether the formula is a predicate definition

val is_rewrite_rule : form -> (term * term) list

More general than definition. It means the clause is an equality where all variables in RHS are also in LHS. It can return two rewrite rules if the clause can be oriented in both ways, e.g. associativity axiom.

val is_pred_rewrite_rule : form -> (term * form) option

LogtkRewriting rule for predicates

val is_const_definition : form -> (LogtkSymbol.t * term) option

Checks whether the clause is "const = ground composite term", e.g. a clause "aIbUc = inter(a, union(b, c))". In this case it returns Some(constant, definition of constant)

val is_const_pred_definition : form -> (LogtkSymbol.t * form) option

Definition of constant predicate

Interface to LogtkTransform

See module LogtkTransform. By detecting some shapes in the input, for instance rewrite rules or term definitions, one can obtain interesting transformations

val detect : form Sequence.t -> LogtkTransform.t list

Detect shapes in the given sequence, and convert them into transformations over formulas

val detect_list : form list -> LogtkTransform.t list
val detect_def : ?only:[ `Pred | `Term ] -> ?arity:[ `Zero | `Nonzero ] -> form Sequence.t -> LogtkTransform.t list

Detect definitions.

  • parameter only

    if present, restrict detection to predicates or terms

  • parameter arity

    if present, restrict to constant or non-constant symbols