Lcffol (Calculemus)

Lcffol Module

Namespace: Calculemus
Assembly: Calculemus.dll

LCF implementation of first-order tableaux.

Functions and values

Function or value	Description
`add_assum' fm thp (arg3, arg4)` Full Usage: `add_assum' fm thp (arg3, arg4)` Parameters: fm : `formula<fol>` thp : `(term -> term) * 'a -> thm` arg2 : `term -> term` arg3 : `'a` Returns: `thm`	fm : `formula<fol>` thp : `(term -> term) * 'a -> thm` arg2 : `term -> term` arg3 : `'a` Returns: `thm`
`complits' (xs, lits) i (e, s)` Full Usage: `complits' (xs, lits) i (e, s)` Parameters: xs : `formula<fol> list` lits : `formula<fol> list` i : `int` e : `term -> term` s : `formula<fol>` Returns: `thm`	xs : `formula<fol> list` lits : `formula<fol> list` i : `int` e : `term -> term` s : `formula<fol>` Returns: `thm`
`deskol' skh thp (e, s)` Full Usage: `deskol' skh thp (e, s)` Parameters: skh : `formula<fol>` thp : `(term -> term) * 'a -> thm` e : `term -> term` s : `'a` Returns: `thm`	skh : `formula<fol>` thp : `(term -> term) * 'a -> thm` e : `term -> term` s : `'a` Returns: `thm`
`deskolcont thp (env, sks, k)` Full Usage: `deskolcont thp (env, sks, k)` Parameters: thp : `(term -> term) * formula<fol> -> thm` env : `func<string, term>` sks : `(formula<fol> * term) list` k : `'a` Returns: `thm`	thp : `(term -> term) * formula<fol> -> thm` env : `func<string, term>` sks : `(formula<fol> * term) list` k : `'a` Returns: `thm`
`elim_skolemvar th` Full Usage: `elim_skolemvar th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`eliminate_connective' fm thp (arg3, arg4)` Full Usage: `eliminate_connective' fm thp (arg3, arg4)` Parameters: fm : `formula<fol>` thp : `(term -> term) * 'a -> thm` arg2 : `term -> term` arg3 : `'a` Returns: `thm`	fm : `formula<fol>` thp : `(term -> term) * 'a -> thm` arg2 : `term -> term` arg3 : `'a` Returns: `thm`
`ex_falso' fms (e, s)` Full Usage: `ex_falso' fms (e, s)` Parameters: fms : `formula<fol> list` e : `term -> term` s : `formula<fol>` Returns: `thm`	fms : `formula<fol> list` e : `term -> term` s : `formula<fol>` Returns: `thm`
`form_match (arg1, arg2) env` Full Usage: `form_match (arg1, arg2) env` Parameters: arg0 : `formula<fol>` arg1 : `formula<fol>` env : `func<string, term>` Returns: `func<string, term>`	arg0 : `formula<fol>` arg1 : `formula<fol>` env : `func<string, term>` Returns: `func<string, term>`
`imp_false_rule' th es` Full Usage: `imp_false_rule' th es` Parameters: th : `'a -> thm` es : `'a` Returns: `thm`	th : `'a -> thm` es : `'a` Returns: `thm`
`imp_front' n thp es` Full Usage: `imp_front' n thp es` Parameters: n : `int` thp : `'a -> thm` es : `'a` Returns: `thm`	n : `int` thp : `'a -> thm` es : `'a` Returns: `thm`
`imp_true_rule' th1 th2 es` Full Usage: `imp_true_rule' th1 th2 es` Parameters: th1 : `'a -> thm` th2 : `'a -> thm` es : `'a` Returns: `thm`	th1 : `'a -> thm` th2 : `'a -> thm` es : `'a` Returns: `thm`
`lcffol fm` Full Usage: `lcffol fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`lcfrefute fm n cont` Full Usage: `lcfrefute fm n cont` Parameters: fm : `formula<fol>` n : `int` cont : `((term -> term) * formula<fol> -> thm) -> func<string, term> * (formula<fol> * term) list * int -> 'a` Returns: `'a`	fm : `formula<fol>` n : `int` cont : `((term -> term) * formula<fol> -> thm) -> func<string, term> * (formula<fol> * term) list * int -> 'a` Returns: `'a`
`lcftab skofun (fms, lits, n) cont (arg6, arg7, arg8)` Full Usage: `lcftab skofun (fms, lits, n) cont (arg6, arg7, arg8)` Parameters: skofun : `formula<fol> -> term` fms : `formula<fol> list` lits : `formula<fol> list` n : `int` cont : `((term -> term) * formula<fol> -> thm) -> func<string, term> * (formula<fol> * term) list * int -> 'a` arg5 : `func<string, term>` arg6 : `(formula<fol> * term) list` arg7 : `int` Returns: `'a`	skofun : `formula<fol> -> term` fms : `formula<fol> list` lits : `formula<fol> list` n : `int` cont : `((term -> term) * formula<fol> -> thm) -> func<string, term> * (formula<fol> * term) list * int -> 'a` arg5 : `func<string, term>` arg6 : `(formula<fol> * term) list` arg7 : `int` Returns: `'a`
`mk_skol (fm, fx) q` Full Usage: `mk_skol (fm, fx) q` Parameters: fm : `formula<fol>` fx : `term` q : `formula<fol>` Returns: `formula<fol>`	fm : `formula<fol>` fx : `term` q : `formula<fol>` Returns: `formula<fol>`
`quantforms e fm` Full Usage: `quantforms e fm` Parameters: e : `bool` fm : `formula<'a>` Returns: `formula<'a> list`	e : `bool` fm : `formula<'a>` Returns: `formula<'a> list`
`simpcont thp (env, sks, k)` Full Usage: `simpcont thp (env, sks, k)` Parameters: thp : `(term -> term) * formula<fol> -> 'a` env : `func<string, term>` sks : `(formula<fol> * term) list` k : `'b` Returns: `'a`	thp : `(term -> term) * formula<fol> -> 'a` env : `func<string, term>` sks : `(formula<fol> * term) list` k : `'b` Returns: `'a`
`skolemfuns fm` Full Usage: `skolemfuns fm` Parameters: fm : `formula<fol>` Returns: `(formula<fol> * term) list`	fm : `formula<fol>` Returns: `(formula<fol> * term) list`
`spec' y fm n thp (e, s)` Full Usage: `spec' y fm n thp (e, s)` Parameters: y : `term` fm : `formula<fol>` n : `int` thp : `(term -> term) * 'a -> thm` e : `term -> term` s : `'a` Returns: `thm`	y : `term` fm : `formula<fol>` n : `int` thp : `(term -> term) * 'a -> thm` e : `term -> term` s : `'a` Returns: `thm`
`unify_complementsf env (arg2, arg3)` Full Usage: `unify_complementsf env (arg2, arg3)` Parameters: env : `func<string, term>` arg1 : `formula<fol>` arg2 : `formula<fol>` Returns: `func<string, term>`	env : `func<string, term>` arg1 : `formula<fol>` arg2 : `formula<fol>` Returns: `func<string, term>`
`use_laterimp i fm` Full Usage: `use_laterimp i fm` Parameters: i : `formula<fol>` fm : `formula<fol>` Returns: `thm`	i : `formula<fol>` fm : `formula<fol>` Returns: `thm`