Module Lfp

module Lfp: sig .. end

Learning LFP formulas.

val abstract_learn : ((string * Formula.formula) list -> Structure.structure option) ->
       Formula.formula -> Formula.formula option

Abstract learning: teacher takes a tuple of relation names and formulas and gives a counter-example structure with these relations where the given formulas are supposed to hold (but differ from the given).

val find_lfp_iter : int ->
       Formula.formula ->
       Formula.formula ->
       Formula.formula option -> Formula.formula option -> Formula.formula option

Find lfp formula iterating on counter-exaples.

val basic_outline : ?free_id:int ->
       ?neg:bool ->
       ?eq:bool ->
       ?only_pos:bool ->
       ?prefix:string ->
       k:int ->
       c:int ->
       asyms:Formula.formula list Pervasives.ref ->
       (string * int) list -> (string * int) list -> string list -> Formula.formula

Basic outline of the form "ex x_1 .. x_k (cl_1 and ... and cl_c)", clauses from all atoms and vars. Negated if set, takes and returns free guard id.*

val lfp_outline : ?free_id:int ->
       ?recursive:bool ->
       ?positive:bool ->
       ?eq:bool ->
       fp:string list ->
       k:int ->
       c:int ->
       asyms:Formula.formula list Pervasives.ref ->
       (string * int) list ->
       (string * int) list ->
       string list -> (int * int * int * int) list -> Formula.formula

Outline with definitions of the form "U_i(x)=+/-basic_outline k_i c_i", given a_i, k_i, c_i, and combined to lfp U(x_a) = +/- basic neg k c. *