Stal (Calculemus)

Stal Module

Namespace: Calculemus
Assembly: Calculemus.dll

Stalmarck method.

Functions and values

Function or value	Description
`align (p, q)` Full Usage: `align (p, q)` Parameters: p : `formula<'a>` q : `formula<'a>` Returns: `formula<'a> * formula<'a>`	p : `formula<'a>` q : `formula<'a>` Returns: `formula<'a> * formula<'a>`
`atom lit` Full Usage: `atom lit` Parameters: lit : `formula<'a>` Returns: `formula<'a>`	lit : `formula<'a>` Returns: `formula<'a>`
`consequences (arg1, arg2) fm eqs` Full Usage: `consequences (arg1, arg2) fm eqs` Parameters: arg0 : `formula<'a>` arg1 : `formula<'a>` fm : `formula<'a>` eqs : `(formula<'a> * formula<'a>) list` Returns: `(formula<'a> * formula<'a>) list`	arg0 : `formula<'a>` arg1 : `formula<'a>` fm : `formula<'a>` eqs : `(formula<'a> * formula<'a>) list` Returns: `(formula<'a> * formula<'a>) list`
`equate2 (p, q) eqv` Full Usage: `equate2 (p, q) eqv` Parameters: p : `formula<'a>` q : `formula<'a>` eqv : `partition<formula<'a>>` Returns: `partition<formula<'a>>`	p : `formula<'a>` q : `formula<'a>` eqv : `partition<formula<'a>>` Returns: `partition<formula<'a>>`
`equatecons (p0, q0) (arg3, arg4)` Full Usage: `equatecons (p0, q0) (arg3, arg4)` Parameters: p0 : `formula<'a>` q0 : `formula<'a>` arg2 : `partition<formula<'a>>` arg3 : `func<formula<'a>, ('b * 'c list) list>` Returns: `'c list * (partition<formula<'a>> * func<formula<'a>, ('b * 'c list) list>)`	p0 : `formula<'a>` q0 : `formula<'a>` arg2 : `partition<formula<'a>>` arg3 : `func<formula<'a>, ('b * 'c list) list>` Returns: `'c list * (partition<formula<'a>> * func<formula<'a>, ('b * 'c list) list>)`
`equateset s0 (arg2, arg3)` Full Usage: `equateset s0 (arg2, arg3)` Parameters: s0 : `formula<'a> list` arg1 : `partition<formula<'a>>` arg2 : `func<formula<'a>, ('b * 'c list) list>` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * 'c list) list>`	s0 : `formula<'a> list` arg1 : `partition<formula<'a>>` arg2 : `func<formula<'a>, ('b * 'c list) list>` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * 'c list) list>`
`inter els (arg2, arg3) (arg4, arg5) rev1 rev2 (arg8, arg9)` Full Usage: `inter els (arg2, arg3) (arg4, arg5) rev1 rev2 (arg8, arg9)` Parameters: els : `formula<'a> list` arg1 : `partition<formula<'a>>` arg2 : `'b` arg3 : `partition<formula<'a>>` arg4 : `'c` rev1 : `func<formula<'a>, formula<'a> list>` rev2 : `func<formula<'a>, formula<'a> list>` arg7 : `partition<formula<'a>>` arg8 : `func<formula<'a>, ('d * 'e list) list>` Returns: `partition<formula<'a>> * func<formula<'a>, ('d * 'e list) list>`	els : `formula<'a> list` arg1 : `partition<formula<'a>>` arg2 : `'b` arg3 : `partition<formula<'a>>` arg4 : `'c` rev1 : `func<formula<'a>, formula<'a> list>` rev2 : `func<formula<'a>, formula<'a> list>` arg7 : `partition<formula<'a>>` arg8 : `func<formula<'a>, ('d * 'e list) list>` Returns: `partition<formula<'a>> * func<formula<'a>, ('d * 'e list) list>`
`irredundant rel eqs` Full Usage: `irredundant rel eqs` Parameters: rel : `partition<formula<'a>>` eqs : `(formula<'a> * formula<'a>) list` Returns: `(formula<'a> * formula<'a>) list`	rel : `partition<formula<'a>>` eqs : `(formula<'a> * formula<'a>) list` Returns: `(formula<'a> * formula<'a>) list`
`relevance trigs` Full Usage: `relevance trigs` Parameters: trigs : `(('a * 'a) * 'b) list` Returns: `func<'a, (('a * 'a) * 'b) list>`	trigs : `(('a * 'a) * 'b) list` Returns: `func<'a, (('a * 'a) * 'b) list>`
`reverseq domain eqv` Full Usage: `reverseq domain eqv` Parameters: domain : `'a list` eqv : `partition<'a>` Returns: `func<'a, 'a list>`	domain : `'a list` eqv : `partition<'a>` Returns: `func<'a, 'a list>`
`saturate n (arg2, arg3) assigs allvars` Full Usage: `saturate n (arg2, arg3) assigs allvars` Parameters: n : `int` arg1 : `partition<formula<'a>>` arg2 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` assigs : `(formula<'a> * formula<'a>) list` allvars : `formula<'a> list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`	n : `int` arg1 : `partition<formula<'a>>` arg2 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` assigs : `(formula<'a> * formula<'a>) list` allvars : `formula<'a> list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`
`saturate_upto vars n m trigs assigs` Full Usage: `saturate_upto vars n m trigs assigs` Parameters: vars : `formula<'a> list` n : `int` m : `int` trigs : `((formula<'a> * formula<'a>) * (formula<'a> * formula<'a>) list) list` assigs : `(formula<'a> * formula<'a>) list` Returns: `bool`	vars : `formula<'a> list` n : `int` m : `int` trigs : `((formula<'a> * formula<'a>) * (formula<'a> * formula<'a>) list) list` assigs : `(formula<'a> * formula<'a>) list` Returns: `bool`
`splits n (arg2, arg3) allvars vars` Full Usage: `splits n (arg2, arg3) allvars vars` Parameters: n : `int` arg1 : `partition<formula<'a>>` arg2 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` allvars : `formula<'a> list` vars : `formula<'a> list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`	n : `int` arg1 : `partition<formula<'a>>` arg2 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` allvars : `formula<'a> list` vars : `formula<'a> list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`
`stal_intersect (arg1, arg2) (arg3, arg4) (arg5, arg6)` Full Usage: `stal_intersect (arg1, arg2) (arg3, arg4) (arg5, arg6)` Parameters: arg0 : `partition<formula<'a>>` arg1 : `func<formula<'a>, ('b * 'c list) list>` arg2 : `partition<formula<'a>>` arg3 : `func<formula<'a>, ('b * 'c list) list>` arg4 : `partition<formula<'a>>` arg5 : `func<formula<'a>, ('b * 'c list) list>` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * 'c list) list>`	arg0 : `partition<formula<'a>>` arg1 : `func<formula<'a>, ('b * 'c list) list>` arg2 : `partition<formula<'a>>` arg3 : `func<formula<'a>, ('b * 'c list) list>` arg4 : `partition<formula<'a>>` arg5 : `func<formula<'a>, ('b * 'c list) list>` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * 'c list) list>`
`stalmarck fm` Full Usage: `stalmarck fm` Parameters: fm : `formula<prop>` Returns: `bool`	fm : `formula<prop>` Returns: `bool`
`trigger` Full Usage: `trigger` Returns: `formula<prop> -> ((formula<prop> * formula<prop>) * (formula<prop> * formula<prop>) list) list`	Returns: `formula<prop> -> ((formula<prop> * formula<prop>) * (formula<prop> * formula<prop>) list) list`
`triggers fm` Full Usage: `triggers fm` Parameters: fm : `formula<'a>` Returns: `((formula<'a> * formula<'a>) * (formula<'a> * formula<'a>) list) list`	fm : `formula<'a>` Returns: `((formula<'a> * formula<'a>) * (formula<'a> * formula<'a>) list) list`
`triplicate fm` Full Usage: `triplicate fm` Parameters: fm : `formula<prop>` Returns: `formula<prop> * formula<prop> list`	fm : `formula<prop>` Returns: `formula<prop> * formula<prop> list`
`truefalse pfn` Full Usage: `truefalse pfn` Parameters: pfn : `partition<formula<'a>>` Returns: `bool`	pfn : `partition<formula<'a>>` Returns: `bool`
`zero_saturate (arg1, arg2) assigs` Full Usage: `zero_saturate (arg1, arg2) assigs` Parameters: arg0 : `partition<formula<'a>>` arg1 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` assigs : `(formula<'a> * formula<'a>) list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`	arg0 : `partition<formula<'a>>` arg1 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` assigs : `(formula<'a> * formula<'a>) list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`
`zero_saturate_and_check (arg1, arg2) trigs` Full Usage: `zero_saturate_and_check (arg1, arg2) trigs` Parameters: arg0 : `partition<formula<'a>>` arg1 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` trigs : `(formula<'a> * formula<'a>) list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`	arg0 : `partition<formula<'a>>` arg1 : `func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>` trigs : `(formula<'a> * formula<'a>) list` Returns: `partition<formula<'a>> * func<formula<'a>, ('b * (formula<'a> * formula<'a>) list) list>`