Combining (Calculemus)

Combining Module

Namespace: Calculemus
Assembly: Calculemus.dll

Combined decision procedure.

Functions and values

Function or value	Description
`add_default langs` Full Usage: `add_default langs` Parameters: langs : `(('a -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` Returns: `(('a -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list`	langs : `(('a -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` Returns: `(('a -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list`
`allpartitions` Full Usage: `allpartitions` Returns: `'a list -> 'a list list list`	Returns: `'a list -> 'a list list list`
`arrangement part` Full Usage: `arrangement part` Parameters: part : `string list list` Returns: `formula<fol> list`	part : `string list list` Returns: `formula<fol> list`
`arreq l` Full Usage: `arreq l` Parameters: l : `string list` Returns: `formula<fol> list`	l : `string list` Returns: `formula<fol> list`
`belongs (fn, pr, dp) fm` Full Usage: `belongs (fn, pr, dp) fm` Parameters: fn : `string * int -> bool` pr : `string * int -> bool` dp : `'a` fm : `formula<fol>` Returns: `bool`	fn : `string * int -> bool` pr : `string * int -> bool` dp : `'a` fm : `formula<fol>` Returns: `bool`
`chooselang langs fm` Full Usage: `chooselang langs fm` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fm : `formula<fol>` Returns: `(string * int -> bool) * (string * int -> bool) * 'a`	langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fm : `formula<fol>` Returns: `(string * int -> bool) * (string * int -> bool) * 'a`
`dest_def fm` Full Usage: `dest_def fm` Parameters: fm : `formula<fol>` Returns: `string * term`	fm : `formula<fol>` Returns: `string * term`
`findasubset p m l` Full Usage: `findasubset p m l` Parameters: p : `'a list -> 'b` m : `int` l : `'a list` Returns: `'b`	p : `'a list -> 'b` m : `int` l : `'a list` Returns: `'b`
`findsubset p l` Full Usage: `findsubset p l` Parameters: p : `'a list -> bool` l : `'a list` Returns: `'a list`	p : `'a list -> bool` l : `'a list` Returns: `'a list`
`homo langs fms cont` Full Usage: `homo langs fms cont` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fms : `formula<fol> list` cont : `formula<fol> list -> bigint -> formula<fol> list -> 'b` Returns: `bigint -> formula<fol> list -> 'b`	langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fms : `formula<fol> list` cont : `formula<fol> list -> bigint -> formula<fol> list -> 'b` Returns: `bigint -> formula<fol> list -> 'b`
`homogenize langs fms` Full Usage: `homogenize langs fms` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fms : `formula<fol> list` Returns: `formula<fol> list`	langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fms : `formula<fol> list` Returns: `formula<fol> list`
`homol langs fm cont n defs` Full Usage: `homol langs fm cont n defs` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fm : `formula<fol>` cont : `formula<fol> -> bigint -> formula<fol> list -> 'b` n : `bigint` defs : `formula<fol> list` Returns: `'b`	langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fm : `formula<fol>` cont : `formula<fol> -> bigint -> formula<fol> list -> 'b` n : `bigint` defs : `formula<fol> list` Returns: `'b`
`homot (fn, pr, dp) tm cont n defs` Full Usage: `homot (fn, pr, dp) tm cont n defs` Parameters: fn : `string * int -> bool` pr : `'a` dp : `'b` tm : `term` cont : `term -> bigint -> formula<fol> list -> 'c` n : `bigint` defs : `formula<fol> list` Returns: `'c`	fn : `string * int -> bool` pr : `'a` dp : `'b` tm : `term` cont : `term -> bigint -> formula<fol> list -> 'c` n : `bigint` defs : `formula<fol> list` Returns: `'c`
`int_lang` Full Usage: `int_lang` Returns: `(string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)`	Returns: `(string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)`
`langpartition langs fms` Full Usage: `langpartition langs fms` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fms : `formula<fol> list` Returns: `formula<fol> list list`	langs : `((string * int -> bool) * (string * int -> bool) * 'a) list` fms : `formula<fol> list` Returns: `formula<fol> list list`
`listify f l cont` Full Usage: `listify f l cont` Parameters: f : `'a -> ('b -> 'c) -> 'c` l : `'a list` cont : `'b list -> 'c` Returns: `'c`	f : `'a -> ('b -> 'c) -> 'c` l : `'a list` cont : `'b list -> 'c` Returns: `'c`
`nelop langs fm` Full Usage: `nelop langs fm` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fm : `formula<fol>` Returns: `bool`	langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fm : `formula<fol>` Returns: `bool`
`nelop001 langs fm` Full Usage: `nelop001 langs fm` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fm : `formula<fol>` Returns: `bool`	langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fm : `formula<fol>` Returns: `bool`
`nelop1 langs fms0` Full Usage: `nelop1 langs fms0` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fms0 : `formula<fol> list` Returns: `bool`	langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fms0 : `formula<fol> list` Returns: `bool`
`nelop1001 langs fms0` Full Usage: `nelop1001 langs fms0` Parameters: langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fms0 : `formula<fol> list` Returns: `bool`	langs : `((string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)) list` fms0 : `formula<fol> list` Returns: `bool`
`nelop_refute eqs ldseps` Full Usage: `nelop_refute eqs ldseps` Parameters: eqs : `formula<fol> list` ldseps : `(('a * 'b * (formula<fol> -> bool)) * formula<fol> list) list` Returns: `bool`	eqs : `formula<fol> list` ldseps : `(('a * 'b * (formula<fol> -> bool)) * formula<fol> list) list` Returns: `bool`
`nelop_refute001 vars ldseps` Full Usage: `nelop_refute001 vars ldseps` Parameters: vars : `string list` ldseps : `(('a * 'b * (formula<fol> -> bool)) * formula<fol> list) list` Returns: `bool`	vars : `string list` ldseps : `(('a * 'b * (formula<fol> -> bool)) * formula<fol> list) list` Returns: `bool`
`real_lang` Full Usage: `real_lang` Returns: `(string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)`	Returns: `(string * int -> bool) * (string * int -> bool) * (formula<fol> -> bool)`
`redeqs eqs` Full Usage: `redeqs eqs` Parameters: eqs : `formula<fol> list` Returns: `formula<fol> list`	eqs : `formula<fol> list` Returns: `formula<fol> list`
`trydps ldseps fms` Full Usage: `trydps ldseps fms` Parameters: ldseps : `(('a * 'b * (formula<fol> -> bool)) * formula<fol> list) list` fms : `formula<fol> list` Returns: `bool`	ldseps : `(('a * 'b * (formula<fol> -> bool)) * formula<fol> list) list` fms : `formula<fol> list` Returns: `bool`