Skolems (Calculemus)

Skolems Module

Namespace: Calculemus
Assembly: Calculemus.dll

Skolemizing a set of

Functions and values

Function or value	Description
`rename_form fm` Full Usage: `rename_form fm` Parameters: fm : `formula<fol>` - The input formula. Returns: `formula<fol>` The formula with an `old_` prefix added to each function symbols.	Renames all the function symbols in a formula. fm : `formula<fol>` The input formula. Returns: `formula<fol>` The formula with an `old_` prefix added to each function symbols. Example `!!!"f(g(x),z)" \|> rename_form` Evaluates to `P(old_f(old_g(x),z))`.
`rename_term tm` Full Usage: `rename_term tm` Parameters: tm : `term` - The input term. Returns: `term` The term with an `old_` prefix added to each function symbols.	Renames all the function symbols in a term. tm : `term` The input term. Returns: `term` The term with an `old_` prefix added to each function symbols. Example `!!!"f(g(x),z)" \|> rename_term` Evaluates to ``old_f(old_g(x),z)``.
`skolemizes fms` Full Usage: `skolemizes fms` Parameters: fms : `formula<fol> list` - The input set of formulas. Returns: `formula<fol> list` The set of Skolemized formulas.	Skolemizes a set of formulas. fms : `formula<fol> list` The input set of formulas. Returns: `formula<fol> list` The set of Skolemized formulas. Example `skolemizes !!>["exists x. P(f(g(x),z))"; "forall x. exists y. P(x,y)"]` Evaluates to [`P(old_f(old_g(f_x(z)),z))`; `forall x. P(x,f_y(x))`].
`skolems fms corr` Full Usage: `skolems fms corr` Parameters: fms : `formula<fol> list` - The input set of formulas. corr : `string list` - The list of strings to avoid as names of the Skolem functions. Returns: `formula<fol> list * string list` The pair of the Skolemized formulas set together with the updated list of strings to avoid as names of the Skolem functions.	Core Skolemization function for set of formulas. It is specifically intended to be used on formulas already simplified and in nnf. fms : `formula<fol> list` The input set of formulas. corr : `string list` The list of strings to avoid as names of the Skolem functions. Returns: `formula<fol> list * string list` The pair of the Skolemized formulas set together with the updated list of strings to avoid as names of the Skolem functions. Example `skolems !!>["exists x. P(f(g(x),z))"; "forall x. exists y. P(x,y)"] []` Evaluates to ([`P(old_f(old_g(f_x(z)),z))`; `forall x. P(x,f_y(x))`], ["f_y"; "f_x"]).