Module Z3.Proof

module Proof: sig .. end
Functions to manipulate proof expressions

val is_true : Expr.expr -> bool
Indicates whether the term is a Proof for the expression 'true'.
val is_asserted : Expr.expr -> bool
Indicates whether the term is a proof for a fact asserted by the user.
val is_goal : Expr.expr -> bool
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
val is_oeq : Expr.expr -> bool
Indicates whether the term is a binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
val is_modus_ponens : Expr.expr -> bool
Indicates whether the term is proof via modus ponens

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
Indicates whether the term is a proof for (R t t), where R is a reflexive relation. This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.
val is_symmetry : Expr.expr -> bool
Indicates whether the term is proof by symmetricity of a relation

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
Indicates whether the term is a proof by transitivity of a relation

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
Indicates whether the term is a proof by condensed transitivity of a relation

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
Indicates whether the term is a monotonicity proof object.

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
Indicates whether the term is a quant-intro proof

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
Indicates whether the term is a distributivity proof object.

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
Indicates whether the term is a proof by elimination of AND

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
Indicates whether the term is a proof by eliminiation of not-or

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
Indicates whether the term is a proof by rewriting

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
Indicates whether the term is a proof by rewriting

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
Indicates whether the term is a proof for pulling quantifiers out.

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
Indicates whether the term is a proof for pulling quantifiers out.

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
Indicates whether the term is a proof for pushing quantifiers in.

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
Indicates whether the term is a proof for elimination of unused variables.

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
Indicates whether the term is a proof for destructive equality resolution

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
Indicates whether the term is a proof for quantifier instantiation

A proof of (or (not (forall (x) (P x))) (P a))

val is_hypothesis : Expr.expr -> bool
Indicates whether the term is a hypthesis marker. Mark a hypothesis in a natural deduction style proof.
val is_lemma : Expr.expr -> bool
Indicates whether the term is a proof by lemma

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
Indicates whether the term is a proof by unit resolution

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
Indicates whether the term is a proof by iff-true

T1: p iff-true T1: (iff p true)

val is_iff_false : Expr.expr -> bool
Indicates whether the term is a proof by iff-false

T1: (not p) iff-false T1: (iff p false)

val is_commutativity : Expr.expr -> bool
Indicates whether the term is a proof by commutativity

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
Indicates whether the term is a proof for Tseitin-like axioms

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
Indicates whether the term is a proof for introduction of a name

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
Indicates whether the term is a proof for application of a definition

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
Indicates whether the term is a proof iff-oeq

T1: (iff p q) iff~ T1: (~ p q)

val is_nnf_pos : Expr.expr -> bool
Indicates whether the term is a proof for a positive NNF step

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
Indicates whether the term is a proof for a negative NNF step

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
Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.

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
Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.

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
Indicates whether the term is a proof for a Skolemization step

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
Indicates whether the term is a proof by modus ponens for equi-satisfiability.

Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) mp~ T1 T2: q

val is_theory_lemma : Expr.expr -> bool
Indicates whether the term is a proof for theory lemma

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: