Real (Calculemus)

Real Module

Namespace: Calculemus
Assembly: Calculemus.dll

Real quantifier elimination.

Functions and values

Function or value	Description
`basic_real_qelim vars fm` Full Usage: `basic_real_qelim vars fm` Parameters: vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`	vars : `string list` fm : `formula<fol>` Returns: `formula<fol>`
`casesplit vars dun pols cont sgns` Full Usage: `casesplit vars dun pols cont sgns` Parameters: vars : `string list` dun : `term list` pols : `term list` cont : `sign list list -> formula<fol>` sgns : `(term * sign) list` Returns: `formula<fol>`	vars : `string list` dun : `term list` pols : `term list` cont : `sign list list -> formula<fol>` sgns : `(term * sign) list` Returns: `formula<fol>`
`condense ps` Full Usage: `condense ps` Parameters: ps : `sign list list` Returns: `sign list list`	ps : `sign list list` Returns: `sign list list`
`dedmatrix cont mat` Full Usage: `dedmatrix cont mat` Parameters: cont : `sign list list -> 'a` mat : `sign list list` Returns: `'a`	cont : `sign list list -> 'a` mat : `sign list list` Returns: `'a`
`delconst vars dun p ops cont sgns` Full Usage: `delconst vars dun p ops cont sgns` Parameters: vars : `string list` dun : `term list` p : `term` ops : `term list` cont : `sign list list -> formula<fol>` sgns : `(term * sign) list` Returns: `formula<fol>`	vars : `string list` dun : `term list` p : `term` ops : `term list` cont : `sign list list -> formula<fol>` sgns : `(term * sign) list` Returns: `formula<fol>`
`grpform fm` Full Usage: `grpform fm` Parameters: fm : `formula<fol>` Returns: `formula<fol>`	fm : `formula<fol>` Returns: `formula<fol>`
`grpterm tm` Full Usage: `grpterm tm` Parameters: tm : `term` Returns: `term`	tm : `term` Returns: `term`
`inferisign ps` Full Usage: `inferisign ps` Parameters: ps : `sign list list` Returns: `sign list list`	ps : `sign list list` Returns: `sign list list`
`inferpsign (pd, qd)` Full Usage: `inferpsign (pd, qd)` Parameters: pd : `sign list` qd : `sign list` Returns: `sign list`	pd : `sign list` qd : `sign list` Returns: `sign list`
`matrix vars pols cont sgns` Full Usage: `matrix vars pols cont sgns` Parameters: vars : `string list` pols : `term list` cont : `sign list list -> formula<fol>` sgns : `(term * sign) list` Returns: `formula<fol>`	vars : `string list` pols : `term list` cont : `sign list list -> formula<fol>` sgns : `(term * sign) list` Returns: `formula<fol>`
`pdivide_pos vars sgns s p` Full Usage: `pdivide_pos vars sgns s p` Parameters: vars : `string list` sgns : `(term * sign) list` s : `term` p : `term` Returns: `term`	vars : `string list` sgns : `(term * sign) list` s : `term` p : `term` Returns: `term`
`poly_diff vars p` Full Usage: `poly_diff vars p` Parameters: vars : `string list` p : `term` Returns: `term`	vars : `string list` p : `term` Returns: `term`
`poly_diffn x n p` Full Usage: `poly_diffn x n p` Parameters: x : `term` n : `BigInteger` p : `term` Returns: `term`	x : `term` n : `BigInteger` p : `term` Returns: `term`
`real_qelim` Full Usage: `real_qelim` Returns: `formula<fol> -> formula<fol>`	Returns: `formula<fol> -> formula<fol>`
`real_qelim'` Full Usage: `real_qelim'` Returns: `formula<fol> -> formula<fol>`	Returns: `formula<fol> -> formula<fol>`
`rel_signs` Full Usage: `rel_signs` Returns: `(string * sign list) list`	Returns: `(string * sign list) list`
`split_sign sgns pol cont` Full Usage: `split_sign sgns pol cont` Parameters: sgns : `(term * sign) list` pol : `term` cont : `(term * sign) list -> formula<fol>` Returns: `formula<fol>`	sgns : `(term * sign) list` pol : `term` cont : `(term * sign) list -> formula<fol>` Returns: `formula<fol>`
`split_trichotomy sgns pol cont_z cont_pn` Full Usage: `split_trichotomy sgns pol cont_z cont_pn` Parameters: sgns : `(term * sign) list` pol : `term` cont_z : `(term * sign) list -> formula<fol>` cont_pn : `(term * sign) list -> formula<fol>` Returns: `formula<fol>`	sgns : `(term * sign) list` pol : `term` cont_z : `(term * sign) list -> formula<fol>` cont_pn : `(term * sign) list -> formula<fol>` Returns: `formula<fol>`
`testform pmat fm` Full Usage: `testform pmat fm` Parameters: pmat : `(term * sign) list` fm : `formula<fol>` Returns: `bool`	pmat : `(term * sign) list` fm : `formula<fol>` Returns: `bool`