ProofSystem (Calculemus)

ProofSystem Module

Namespace: Calculemus
Assembly: Calculemus.dll
Parent Module: Lcf

The Core LCF proof system The core proof system is the minimum set of inference rules and/or axioms sound and complete with respect to the defined semantics.

Types

Type	Description
thm

Functions and values

Function or value	Description
`axiom_addimp p q` Full Usage: `axiom_addimp p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- p -> (q -> p) p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_allimp x p q` Full Usage: `axiom_allimp x p q` Parameters: x : `string` p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- (!x. p -> q) -> (!x. p) -> (!x. q) x : `string` p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_and p q` Full Usage: `axiom_and p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- p /\ q <-> (p -> q -> ⊥) -> ⊥ p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_distribimp p q r` Full Usage: `axiom_distribimp p q r` Parameters: p : `formula<fol>` q : `formula<fol>` r : `formula<fol>` Returns: `thm`	\|- (p -> q -> r) -> (p -> q) -> (p -> r) p : `formula<fol>` q : `formula<fol>` r : `formula<fol>` Returns: `thm`
`axiom_doubleneg p` Full Usage: `axiom_doubleneg p` Parameters: p : `formula<fol>` Returns: `thm`	\|- ((p -> ⊥) -> ⊥) -> p p : `formula<fol>` Returns: `thm`
`axiom_eqrefl t` Full Usage: `axiom_eqrefl t` Parameters: t : `term` Returns: `thm`	\|- t = t t : `term` Returns: `thm`
`axiom_exists x p` Full Usage: `axiom_exists x p` Parameters: x : `string` p : `formula<fol>` Returns: `thm`	(?x. p) <-> ~(!x. ~p) x : `string` p : `formula<fol>` Returns: `thm`
`axiom_existseq x t` Full Usage: `axiom_existseq x t` Parameters: x : `string` t : `term` Returns: `thm`	\|- (?x. x = t) [provided x not in FVT(t)] x : `string` t : `term` Returns: `thm`
`axiom_funcong f lefts rights` Full Usage: `axiom_funcong f lefts rights` Parameters: f : `string` lefts : `term list` rights : `term list` Returns: `thm`	\|- s1 = t1 -> ... -> sn = tn -> f(s1, ..., sn) = f(t1, ..., tn) f : `string` lefts : `term list` rights : `term list` Returns: `thm`
`axiom_iffimp1 p q` Full Usage: `axiom_iffimp1 p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- (p <-> q) -> p -> q p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_iffimp2 p q` Full Usage: `axiom_iffimp2 p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- (p <-> q) -> q -> p p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_impall x p` Full Usage: `axiom_impall x p` Parameters: x : `string` p : `formula<fol>` Returns: `thm`	\|- p -> !x. p [provided x not in FV(p)] x : `string` p : `formula<fol>` Returns: `thm`
`axiom_impiff p q` Full Usage: `axiom_impiff p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- (p -> q) -> (q -> p) -> (p <-> q) p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_not p` Full Usage: `axiom_not p` Parameters: p : `formula<fol>` Returns: `thm`	\|- ~p <-> (p -> ⊥) p : `formula<fol>` Returns: `thm`
`axiom_or p q` Full Usage: `axiom_or p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	\|- p \/ q <-> ~(~p /\ ~q) p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`axiom_predcong p lefts rights` Full Usage: `axiom_predcong p lefts rights` Parameters: p : `string` lefts : `term list` rights : `term list` Returns: `thm`	\|- s1 = t1 -> ... -> sn = tn -> f(s1, ..., sn) = f(t1, ..., tn) p : `string` lefts : `term list` rights : `term list` Returns: `thm`
`axiom_true` Full Usage: `axiom_true` Returns: `thm`	\|- ⊤ <-> (⊥ -> ⊥) Returns: `thm`
`concl arg1` Full Usage: `concl arg1` Parameters: arg0 : `thm` Returns: `formula<fol>`	maps a theorem back to the formula that it proves arg0 : `thm` Returns: `formula<fol>`
`gen x arg2` Full Usage: `gen x arg2` Parameters: x : `string` arg1 : `thm` Returns: `thm`	generalization (proper inference rule) \|- p ==> !x. p x : `string` arg1 : `thm` Returns: `thm`
`modusponens pq arg2` Full Usage: `modusponens pq arg2` Parameters: pq : `thm` arg1 : `thm` Returns: `thm`	modusponens (proper inference rule) \|- p -> q \|- p ==> \|- q pq : `thm` arg1 : `thm` Returns: `thm`