val name : (_, _) t -> stringval find : Logic.DB.t -> ('a, 'b) t -> ('a * 'b) listval subset : Logic.DB.t -> ('a, 'b) t -> ('a, 'b) t -> unitsubset db r1 r2 adds to db the axiom that r2(X,Y) :- r1(X,Y); in other words, r1 is a subset of r2 as a relation
val transitive : Logic.DB.t -> ('a, 'a) t -> unitAxioms for transitivity are added to the DB
val tc_of : Logic.DB.t -> tc:('a, 'a) t -> ('a, 'a) t -> unittc_of db ~tc r adds to db axioms that make the relation tc the transitive closure of the relation r.
val reflexive : Logic.DB.t -> ('a, 'a) t -> unitreflexive db r makes r reflexive in db, ie for all X, r(X,X) holds in db.
val symmetry : Logic.DB.t -> ('a, 'a) t -> unitAxiom for symmetry (ie "r(X,Y) <=> r(Y,X)") added to the DB
val from_fun : Logic.DB.t -> ('a, 'b) t -> ('a -> 'b -> bool) -> unitThe given function decides of the given relation (if it returns true for a couple of constants, then the relation holds for those constants)
val add_list : Logic.DB.t -> ('a, 'b) t -> ('a * 'b) list -> unitAdd given list of axioms
val to_string : (_, _) t -> stringval fmt : Format.formatter -> (_, _) t -> unit