module Proof:sig
..end
val is_true : Expr.expr -> bool
val is_asserted : Expr.expr -> bool
val is_goal : Expr.expr -> bool
val is_oeq : Expr.expr -> bool
val is_modus_ponens : Expr.expr -> bool
Given a proof for p and a proof for (implies p q), produces a proof for q.
T1: p
T2: (implies p q)
mp T1 T2
: q
The second antecedents may also be a proof for (iff p q).
val is_reflexivity : Expr.expr -> bool
val is_symmetry : Expr.expr -> bool
Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).
T1: (R t s)
symmetry T1
: (R s t)
T1 is the antecedent of this proof object.
val is_transitivity : Expr.expr -> bool
Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof
for (R t u).
T1: (R t s)
T2: (R s u)
trans T1 T2
: (R t u)
val is_Transitivity_star : Expr.expr -> bool
Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
It combines several symmetry and transitivity proofs.
Example:
T1: (R a b)
T2: (R c b)
T3: (R c d)
trans* T1 T2 T3
: (R a d)
R must be a symmetric and transitive relation.
Assuming that this proof object is a proof for (R s t), then
a proof checker must check if it is possible to prove (R s t)
using the antecedents, symmetry and transitivity. That is,
if there is a path from s to t, if we view every
antecedent (R a b) as an edge between a and b.
val is_monotonicity : Expr.expr -> bool
T1: (R t_1 s_1)
...
Tn: (R t_n s_n)
monotonicity T1 ... Tn
: (R (f t_1 ... t_n) (f s_1 ... s_n))
Remark: if t_i == s_i, then the antecedent Ti is suppressed.
That is, reflexivity proofs are supressed to save space.
val is_quant_intro : Expr.expr -> bool
Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
T1: (~ p q)
quant-intro T1
: (~ (forall (x) p) (forall (x) q))
val is_distributivity : Expr.expr -> bool
Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.
This proof object has no antecedents.
Remark. This rule is used by the CNF conversion pass and
instantiated by f = or, and g = and.
val is_and_elimination : Expr.expr -> bool
Given a proof for (and l_1 ... l_n), produces a proof for l_i
T1: (and l_1 ... l_n)
and-elim T1
: l_i
val is_or_elimination : Expr.expr -> bool
Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).
T1: (not (or l_1 ... l_n))
not-or-elim T1
: (not l_i)
val is_rewrite : Expr.expr -> bool
A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.
This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.
Examples:
(= (+ ( x : expr ) 0) x)
(= (+ ( x : expr ) 1 2) (+ 3 x))
(iff (or ( x : expr ) false) x)
val is_rewrite_star : Expr.expr -> bool
A proof for rewriting an expression t into an expression s. This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases if the parameter PROOF_MODE is 2. The cases are:
val is_pull_quant : Expr.expr -> bool
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
val is_pull_quant_star : Expr.expr -> bool
A proof for (iff P Q) where Q is in prenex normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object has no antecedents
val is_push_quant : Expr.expr -> bool
A proof for:
(iff (forall (x_1 ... x_m) (and p_1x_1 ... x_m
... p_nx_1 ... x_m
))
(and (forall (x_1 ... x_m) p_1x_1 ... x_m
)
...
(forall (x_1 ... x_m) p_nx_1 ... x_m
)))
This proof object has no antecedents
val is_elim_unused_vars : Expr.expr -> bool
A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) px_1 ... x_n
)
(forall (x_1 ... x_n) px_1 ... x_n
))
It is used to justify the elimination of unused variables.
This proof object has no antecedents.
val is_der : Expr.expr -> bool
A proof for destructive equality resolution:
(iff (forall (x) (or (not (= ( x : expr ) t)) Px
)) Pt
)
if ( x : expr ) does not occur in t.
This proof object has no antecedents.
Several variables can be eliminated simultaneously.
val is_quant_inst : Expr.expr -> bool
A proof of (or (not (forall (x) (P x))) (P a))
val is_hypothesis : Expr.expr -> bool
val is_lemma : Expr.expr -> bool
T1: false
lemma T1
: (or (not l_1) ... (not l_n))
This proof object has one antecedent: a hypothetical proof for false.
It converts the proof in a proof for (or (not l_1) ... (not l_n)),
when T1 contains the hypotheses: l_1, ..., l_n.
val is_unit_resolution : Expr.expr -> bool
T1: (or l_1 ... l_n l_1' ... l_m')
T2: (not l_1)
...
T(n+1): (not l_n)
unit-resolution T1 ... T(n+1)
: (or l_1' ... l_m')
val is_iff_true : Expr.expr -> bool
T1: p
iff-true T1
: (iff p true)
val is_iff_false : Expr.expr -> bool
T1: (not p)
iff-false T1
: (iff p false)
val is_commutativity : Expr.expr -> bool
comm
: (= (f a b) (f b a))
f is a commutative operator.
This proof object has no antecedents.
Remark: if f is bool, then = is iff.
val is_def_axiom : Expr.expr -> bool
Proof object used to justify Tseitin's like axioms:
(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)
This proof object has no antecedents.
Note: all axioms are propositional tautologies.
Note also that 'and' and 'or' can take multiple arguments.
You can recover the propositional tautologies by
unfolding the Boolean connectives in the axioms a small
bounded number of steps (=3).
val is_def_intro : Expr.expr -> bool
Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:
When e is of Boolean type:
def-intro
: (and (or n (not e)) (or (not n) e))
or:
def-intro
: (or (not n) e)
when e only occurs positively.
When e is of the form (ite cond th el):
def-intro
: (and (or (not cond) (= n th)) (or cond (= n el)))
Otherwise:
def-intro
: (= n e)
val is_apply_def : Expr.expr -> bool
apply-def T1
: F ~ n
F is 'equivalent' to n, given that T1 is a proof that
n is a name for F.
val is_iff_oeq : Expr.expr -> bool
T1: (iff p q)
iff~ T1
: (~ p q)
val is_nnf_pos : Expr.expr -> bool
Proof for a (positive) NNF step. Example:
T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
nnf-pos T1 T2 T3 T4
: (~ (iff s_1 s_2)
(and (or r_1 r_2') (or r_1' r_2)))
The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:
(a) When creating the NNF of a positive force quantifier.
The quantifier is retained (unless the bound variables are eliminated).
Example
T1: q ~ q_new
nnf-pos T1
: (~ (forall (x T) q) (forall (x T) q_new))
(b) When recursively creating NNF over Boolean formulas, where the top-level
connective is changed during NNF conversion. The relevant Boolean connectives
for NNF_POS are 'implies', 'iff', 'xor', 'ite'.
NNF_NEG furthermore handles the case where negation is pushed
over Boolean connectives 'and' and 'or'.
val is_nnf_neg : Expr.expr -> bool
Proof for a (negative) NNF step. Examples:
T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
nnf-neg T1 ... Tn
: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)
and
T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
nnf-neg T1 ... Tn
: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)
and
T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
nnf-neg T1 T2 T3 T4
: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))
val is_nnf_star : Expr.expr -> bool
A proof for (~ P Q) where Q is in negation normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
val is_cnf_star : Expr.expr -> bool
A proof for (~ P Q) where Q is in conjunctive normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
val is_skolemize : Expr.expr -> bool
Proof for:
sk
: (~ (not (forall ( x : expr ) (p ( x : expr ) y))) (not (p (sk y) y)))
sk
: (~ (exists ( x : expr ) (p ( x : expr ) y)) (p (sk y) y))
This proof object has no antecedents.
val is_modus_ponens_oeq : Expr.expr -> bool
Modus ponens style rule for equi-satisfiability.
T1: p
T2: (~ p q)
mp~ T1 T2
: q
val is_theory_lemma : Expr.expr -> bool
Generic proof for theory lemmas.
The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are: