Qelim (Calculemus)

Qelim Module

Namespace: Calculemus
Assembly: Calculemus.dll

Quantifier elimination basics.

Table of contents

Quantifier elimination
Example: dense linear orders

Quantifier elimination

Functions and values

Function or value	Description
`cnnf lfn fm` Full Usage: `cnnf lfn fm` Parameters: lfn : `formula<fol> -> formula<fol>` - The literal modification function. fm : `formula<fol>` - The input formula. Returns: `formula<fol>` A formula in disjunctive normal form equivalent to the input formula and with literals modified based on the literal modification function.	Returns a disjunctive normal form of the input formula applying a given `literal modification' function to the literals. lfn : `formula<fol> -> formula<fol>` The literal modification function. fm : `formula<fol>` The input formula. Returns: `formula<fol>` A formula in disjunctive normal form equivalent to the input formula and with literals modified based on the literal modification function. Example `!!"~(s = t) /\ ~(s < t)" \|> cnnf lfn_dlo` Evaluates to `(s < t \/ t < s) /\ (s = t \/ t < s)`.
`lift_qelim afn nfn qfn fm` Full Usage: `lift_qelim afn nfn qfn fm` Parameters: afn : `string list -> formula<fol> -> formula<fol>` - A function to convert inequalities not included in the core language. nfn : `formula<fol> -> formula<fol>` - A disjunctive normal form function. qfn : `string list -> formula<fol> -> formula<fol>` - The core quantifier elimination function. fm : `formula<fol>` - The input formula. Returns: `formula<fol>`	Main quantifier elimination function afn : `string list -> formula<fol> -> formula<fol>` A function to convert inequalities not included in the core language. nfn : `formula<fol> -> formula<fol>` A disjunctive normal form function. qfn : `string list -> formula<fol> -> formula<fol>` The core quantifier elimination function. fm : `formula<fol>` The input formula. Returns: `formula<fol>`
`qelim bfn x p` Full Usage: `qelim bfn x p` Parameters: bfn : `formula<fol> -> formula<fol>` - The core quantifier elimination procedure. x : `string` - The existentially quantified variable. p : `formula<fol>` - The body of the existential formula. Returns: `formula<fol>` The equivalent formula of \(\exists x.\ p\) with the existential quantifier applied only to the conjuncts in \(p\) that involve \(x\).	Accepts the core quantifier elimination procedure and generalizes it slightly to work for \(\exists x.\ p\) where \(p\) is any conjunction of literals, some perhaps not involving \(x\). bfn : `formula<fol> -> formula<fol>` The core quantifier elimination procedure. x : `string` The existentially quantified variable. p : `formula<fol>` The body of the existential formula. Returns: `formula<fol>` The equivalent formula of \(\exists x.\ p\) with the existential quantifier applied only to the conjuncts in \(p\) that involve \(x\).

Example: dense linear orders

Functions and values

Function or value	Description
`afn_dlo vars fm` Full Usage: `afn_dlo vars fm` Parameters: vars : `'a` - Unused params required by Qelim.lift_qelim signature. fm : `formula<fol>` - The input literal. Returns: `formula<fol>` A formula equivalent to the input literal with inequality relations not included in the language converted into admitted ones.	Converts inequality relations not included in the core language into equivalent admitted relations. vars : `'a` Unused params required by Qelim.lift_qelim signature. fm : `formula<fol>` The input literal. Returns: `formula<fol>` A formula equivalent to the input literal with inequality relations not included in the language converted into admitted ones. Example `afn_dlo [] !!"s <= t"` Evaluates to `~t < s`.
`dlobasic fm` Full Usage: `dlobasic fm` Parameters: fm : `formula<fol>` - The input formula. Returns: `formula<fol>`	Basic quantifier elimination function for dense linear orders. fm : `formula<fol>` The input formula. Returns: `formula<fol>`
`lfn_dlo fm` Full Usage: `lfn_dlo fm` Parameters: fm : `formula<fol>` - The input literal. Returns: `formula<fol>` A formula equivalent to the input literal without negation, if the input formula is of the form `~(s < t)` or `~(s = t)`; otherwise, the input formula unchanged.	Literal modification function to remove negated dlo literals. fm : `formula<fol>` The input literal. Returns: `formula<fol>` A formula equivalent to the input literal without negation, if the input formula is of the form `~(s < t)` or `~(s = t)`; otherwise, the input formula unchanged. Example `lfn_dlo !!"~s < t"` Evaluates to `s = t \/ t < s`. Example `lfn_dlo !!"~s = t"` Evaluates to `s < t \/ t < s`. Example `lfn_dlo !!"~s = t /\ ~s < t"` Evaluates to `~s = t /\ ~s < t`.
`quelim_dlo fm` Full Usage: `quelim_dlo fm` Parameters: fm : `formula<fol>` - The input dlo formula. Returns: `formula<fol>` A quantifier free formula equivalent to input one (provided this is a dlo formula).	Quantifier elimination function for dense linear orders formulas. fm : `formula<fol>` The input dlo formula. Returns: `formula<fol>` A quantifier free formula equivalent to input one (provided this is a dlo formula). Example `quelim_dlo !!"forall x y. exists z. z < x /\ z < y"` Evaluates to `true`. Example `quelim_dlo !!"exists z. z < x /\ z < y"` Evaluates to `true`. Example `quelim_dlo !!"exists z. x < z /\ z < y"` Evaluates to `x < y`. Example `quelim_dlo !!"(forall x. x < a ==> x < b)"` Evaluates to `~(b < a \/ b < a)`.