Functions
CERTIF	cweakening (char name, CERTIF c, size_t m, const EXPR bs)
	`weakening` rule (additional). More...

CERTIF	cassume (char *name, size_t num)
	`assume` rule (number 1 in Alethe). More...

CERTIF	ctrue (char *name)
	`true` rule (number 3 in Alethe). More...

CERTIF	cfalse (char *name)
	`false` rule (number 4 in Alethe). More...

CERTIF	cresolution (char name, size_t nb, const CERTIF premisses)
	`th_resolution` and `resolution` rules (number 6 and 7 in Alethe). More...

CERTIF	clia_generic (char name, size_t nb, const EXPR l)
	`lia_generic` rule (number 12 in Alethe). More...

CERTIF	ceq_reflexive (char *name, EXPR t)
	`eq_reflexive` rule (number 23 in Alethe). More...

CERTIF	ceq_transitive (char name, size_t n, const EXPR ts)
	`eq_transitive` rule (number 24 in Alethe). More...

CERTIF	ceq_congruent (char name, size_t n, const EXPR clause)
	`eq_congruent` rule (number 25 in Alethe). More...

CERTIF	ceq_congruent_pred (char name, size_t n, const EXPR clause)
	`eq_congruent_pred` rule (number 26 in Alethe). More...

CERTIF	ceq_congruent_pred_b (char name, size_t n, const EXPR clause)
	`eq_congruent_pred_b` rule (a small variant of the previous one). More...

CERTIF	cand (char *name, CERTIF c, int k)
	`and` rule (number 28 in Alethe). More...

CERTIF	cnot_or (char *name, CERTIF c, int k)
	`not_or` rule (number 29 in Alethe). More...

CERTIF	cor (char *name, CERTIF c)
	`or` rule (number 30 in Alethe). More...

CERTIF	cnot_and (char *name, CERTIF c)
	`not_and` rule (number 31 in Alethe). More...

CERTIF	cxor1 (char *name, CERTIF c)
	`xor1` rule (number 32 in Alethe). More...

CERTIF	cxor2 (char *name, CERTIF c)
	`xor2` rule (number 33 in Alethe). More...

CERTIF	cnot_xor1 (char *name, CERTIF c)
	`not_xor1` rule (number 34 in Alethe). More...

CERTIF	cnot_xor2 (char *name, CERTIF c)
	`not_xor2` rule (number 35 in Alethe). More...

CERTIF	cimplies (char *name, CERTIF c)
	`implies` rule (number 36 in Alethe). More...

CERTIF	cnot_implies1 (char *name, CERTIF c)
	`not_implies1` rule (number 37 in Alethe). More...

CERTIF	cnot_implies2 (char *name, CERTIF c)
	`not_implies2` rule (number 38 in Alethe). More...

CERTIF	cequiv1 (char *name, CERTIF c)
	`equiv1` rule (number 39 in Alethe). More...

CERTIF	cequiv2 (char *name, CERTIF c)
	`equiv2` rule (number 40 in Alethe). More...

CERTIF	cnot_equiv1 (char *name, CERTIF c)
	`not_equiv1` rule (number 41 in Alethe). More...

CERTIF	cnot_equiv2 (char *name, CERTIF c)
	`not_equiv2` rule (number 42 in Alethe). More...

CERTIF	cand_pos (char name, size_t n, const EXPR fs, int k)
	`and_pos` rule (number 43 in Alethe). More...

CERTIF	cand_neg (char name, size_t n, const EXPR fs)
	`and_neg` rule (number 44 in Alethe). More...

CERTIF	cor_pos (char name, size_t n, const EXPR fs)
	`or_pos` rule (number 45 in Alethe). More...

CERTIF	cor_neg (char name, size_t n, const EXPR fs, int k)
	`or_neg` rule (number 46 in Alethe). More...

CERTIF	cxor_pos1 (char *name, EXPR a, EXPR b)
	`xor_pos1` rule (number 47 in Alethe). More...

CERTIF	cxor_pos2 (char *name, EXPR a, EXPR b)
	`xor_pos2` rule (number 48 in Alethe). More...

CERTIF	cxor_neg1 (char *name, EXPR a, EXPR b)
	`xor_neg1` rule (number 49 in Alethe). More...

CERTIF	cxor_neg2 (char *name, EXPR a, EXPR b)
	`xor_neg2` rule (number 50 in Alethe). More...

CERTIF	cimplies_pos (char *name, EXPR a, EXPR b)
	`implies_pos` rule (number 51 in Alethe). More...

CERTIF	cimplies_neg1 (char *name, EXPR a, EXPR b)
	`implies_neg1` rule (number 52 in Alethe). More...

CERTIF	cimplies_neg2 (char *name, EXPR a, EXPR b)
	`implies_neg2` rule (number 53 in Alethe). More...

CERTIF	cequiv_pos1 (char *name, EXPR a, EXPR b)
	`equiv_pos1` rule (number 54 in Alethe). More...

CERTIF	cequiv_pos2 (char *name, EXPR a, EXPR b)
	`equiv_pos2` rule (number 55 in Alethe). More...

CERTIF	cequiv_neg1 (char *name, EXPR a, EXPR b)
	`equiv_neg1` rule (number 56 in Alethe). More...

CERTIF	cequiv_neg2 (char *name, EXPR a, EXPR b)
	`equiv_neg2` rule (number 57 in Alethe). More...

Detailed Description

Our certificate format implements parts of the Alethe format.

See also: https://verit.loria.fr/documentation/alethe-spec.pdf; See in particular the description of the rules starting p.26.

Some missing aspects are:

the context is not supported
some rules are not supported

Some additional aspects are:

the rule not_not is useless as SMTCoq reasons module double negation
it implements an additional rule: weakening.

Each rule has the same name as in the document (with an additional c at the beginning), and the documentation refers to the number of the rule in the document.

The first parameter of each rule is a name given to the step, to be used with the debugging checker. All names must be unique.

Warning: Make sure not to produce clauses containing both a formula and its negation (even modulo double negation), as it is considered trivial by SMTCoq. It may be a cause of failure.

Function Documentation

◆ cand()

CERTIF cand	(	char *	name,
		CERTIF	c,
		int	k
	)

and rule (number 28 in Alethe).

Given a proof of the clause {(and f1 ... fn)} and a non-negative integer k, proves the clause {fk}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(and f1 ... fn)}`.
k	An integer between `1` and `n`.

Returns: The corresponding certificate.

◆ cand_neg()

CERTIF cand_neg	(	char *	name,
		size_t	n,
		const EXPR *	fs
	)

and_neg rule (number 44 in Alethe).

Given the formulas f1 ... fn, proves the tautological clause {(and f1 ... fn) (not f1) ... (not fn)}.

Parameters

name	The unique name given to the proof step.
n	The number of formulas in the resulting conjunction.
fs	A pointer to the list of formulas.

Returns: The corresponding certificate.

◆ cand_pos()

CERTIF cand_pos	(	char *	name,
		size_t	n,
		const EXPR *	fs,
		int	k
	)

and_pos rule (number 43 in Alethe).

Given the formulas f1 ... fn and a non-negative integer k, proves the tautological clause {(not (and f1 ... fn)) fk}.

Parameters

name	The unique name given to the proof step.
n	The number of formulas in the resulting conjunction.
fs	A pointer to the list of formulas.
k	An integer between `1` and `n`.

Returns: The corresponding certificate.

◆ cassume()

CERTIF cassume	(	char *	name,
		size_t	num
	)

assume rule (number 1 in Alethe).

Refer to an assertion by its index, in the order they were given.

The first assertion has index 0.

Parameters

name	The unique name given to the proof step.
num	The index of the assertion.

Returns: The corresponding certificate.

◆ ceq_congruent()

CERTIF ceq_congruent	(	char *	name,
		size_t	n,
		const EXPR *	clause
	)

eq_congruent rule (number 25 in Alethe).

Proves the tautological clause {(not (= t1 u1)) ... (not (= tn un)) (= f(t1, ..., tn) f(u1, ..., un))}

Warning: The tis and uis must be non-Boolean terms, and the codomain of f must not be Bool.

Parameters

name	The unique name given to the proof step.
n	The number of literals in the final clause.
clause	A pointer to the list of literals in the final clause.

Returns: The corresponding certificate.

◆ ceq_congruent_pred()

CERTIF ceq_congruent_pred	(	char *	name,
		size_t	n,
		const EXPR *	clause
	)

eq_congruent_pred rule (number 26 in Alethe).

Proves the tautological clause {(not (= t1 u1)) ... (not (= tn un)) (= P(t1, ..., tn) P(u1, ..., un))}

Warning: The tis and uis must be non-Boolean terms, and the codomain of P must be Bool.

Parameters

name	The unique name given to the proof step.
n	The number of literals in the final clause.
clause	A pointer to the list of literals in the final clause.

Returns: The corresponding certificate.

◆ ceq_congruent_pred_b()

CERTIF ceq_congruent_pred_b	(	char *	name,
		size_t	n,
		const EXPR *	clause
	)

eq_congruent_pred_b rule (a small variant of the previous one).

Proves the tautological clause {(not (= t1 u1)) ... (not (= tn un)) (not P(t1, ..., tn)) P(u1, ..., un)}

Warning: The tis and uis must be non-Boolean terms, and the codomain of P must be Bool.

Parameters

name	The unique name given to the proof step.
n	The number of literals in the final clause.
clause	A pointer to the list of literals in the final clause.

Returns: The corresponding certificate.

◆ ceq_reflexive()

CERTIF ceq_reflexive	(	char *	name,
		EXPR	t
	)

eq_reflexive rule (number 23 in Alethe).

Given a term t, proves the tautological clause {(= t t)}.

Warning: Applies only to a non-Boolean term.

Parameters

name	The unique name given to the proof step.
t	The term.

Returns: The corresponding certificate.

◆ ceq_transitive()

CERTIF ceq_transitive	(	char *	name,
		size_t	n,
		const EXPR *	ts
	)

eq_transitive rule (number 24 in Alethe).

Given the terms t1 ... tn, proves the tautological clause {(not (= t1 t2)) ... (not (= t{n-1} tn)) (= t1 tn)}

Warning: The tis must be non-Boolean terms.

Parameters

name	The unique name given to the proof step.
n	The number of terms.
ts	A pointer to the list of terms.

Returns: The corresponding certificate.

◆ cequiv1()

CERTIF cequiv1	(	char *	name,
		CERTIF	c
	)

equiv1 rule (number 39 in Alethe).

Given a proof of the clause {(= a b)}, proves the clause {(not a) b}.

Warning: a and b must be Boolean expressions

Parameters

name	The unique name given to the proof step.
c	The proof of `{(= a b)}`.

Returns: The corresponding certificate.

◆ cequiv2()

CERTIF cequiv2	(	char *	name,
		CERTIF	c
	)

equiv2 rule (number 40 in Alethe).

Given a proof of the clause {(= a b)}, proves the clause {a (not b)}.

Warning: a and b must be Boolean expressions

Parameters

name	The unique name given to the proof step.
c	The proof of `{(= a b)}`.

Returns: The corresponding certificate.

◆ cequiv_neg1()

CERTIF cequiv_neg1	(	char *	name,
		EXPR	a,
		EXPR	b
	)

equiv_neg1 rule (number 56 in Alethe).

Given the formulas a and b, proves the tautological clause {(= a b) (not a) (not b)}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the equality.
b	The right-hand side formula of the equality.

Returns: The corresponding certificate.

◆ cequiv_neg2()

CERTIF cequiv_neg2	(	char *	name,
		EXPR	a,
		EXPR	b
	)

equiv_neg2 rule (number 57 in Alethe).

Given the formulas a and b, proves the tautological clause {(= a b) a b}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the equality.
b	The right-hand side formula of the equality.

Returns: The corresponding certificate.

◆ cequiv_pos1()

CERTIF cequiv_pos1	(	char *	name,
		EXPR	a,
		EXPR	b
	)

equiv_pos1 rule (number 54 in Alethe).

Given the formulas a and b, proves the tautological clause {(not (= a b)) a (not b)}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the equality.
b	The right-hand side formula of the equality.

Returns: The corresponding certificate.

◆ cequiv_pos2()

CERTIF cequiv_pos2	(	char *	name,
		EXPR	a,
		EXPR	b
	)

equiv_pos2 rule (number 55 in Alethe).

Given the formulas a and b, proves the tautological clause {(not (= a b)) (not a) b}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the equality.
b	The right-hand side formula of the equality.

Returns: The corresponding certificate.

◆ cfalse()

CERTIF cfalse ( char * name )

false rule (number 4 in Alethe).

Proves the tautological clause {(not false)}.

Parameters

name	The unique name given to the proof step.

Returns: The corresponding certificate.

◆ cimplies()

CERTIF cimplies	(	char *	name,
		CERTIF	c
	)

implies rule (number 36 in Alethe).

Given a proof of the clause {(=> a b)}, proves the clause {(not a) b}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(=> a b)}`.

Returns: The corresponding certificate.

◆ cimplies_neg1()

CERTIF cimplies_neg1	(	char *	name,
		EXPR	a,
		EXPR	b
	)

implies_neg1 rule (number 52 in Alethe).

Given the formulas a and b, proves the tautological clause {(implies a b) a}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the implication.
b	The right-hand side formula of the implication.

Returns: The corresponding certificate.

◆ cimplies_neg2()

CERTIF cimplies_neg2	(	char *	name,
		EXPR	a,
		EXPR	b
	)

implies_neg2 rule (number 53 in Alethe).

Given the formulas a and b, proves the tautological clause {(implies a b) (not b)}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the implication.
b	The right-hand side formula of the implication.

Returns: The corresponding certificate.

◆ cimplies_pos()

CERTIF cimplies_pos	(	char *	name,
		EXPR	a,
		EXPR	b
	)

implies_pos rule (number 51 in Alethe).

Given the formulas a and b, proves the tautological clause {(not (implies a b)) (not a) b}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the implication.
b	The right-hand side formula of the implication.

Returns: The corresponding certificate.

◆ clia_generic()

CERTIF clia_generic	(	char *	name,
		size_t	nb,
		const EXPR *	l
	)

lia_generic rule (number 12 in Alethe).

Proves the given clause in the theory of linear integer arithmetic.

Parameters

name	The unique name given to the proof step.
nb	The number of literals in the clause.
l	A pointer to the literals of the clause.

Returns: The corresponding certificate.

◆ cnot_and()

CERTIF cnot_and	(	char *	name,
		CERTIF	c
	)

not_and rule (number 31 in Alethe).

Given a proof of the clause {(not (and f1 ... fn))}, proves the clause {(not f1) ... (not fn)}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (and f1 ... fn))}`.

Returns: The corresponding certificate.

◆ cnot_equiv1()

CERTIF cnot_equiv1	(	char *	name,
		CERTIF	c
	)

not_equiv1 rule (number 41 in Alethe).

Given a proof of the clause {(not (= a b))}, proves the clause {a b}.

Warning: a and b must be Boolean expressions

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (= a b))}`.

Returns: The corresponding certificate.

◆ cnot_equiv2()

CERTIF cnot_equiv2	(	char *	name,
		CERTIF	c
	)

not_equiv2 rule (number 42 in Alethe).

Given a proof of the clause {(not (= a b))}, proves the clause {(not a) (not b)}.

Warning: a and b must be Boolean expressions

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (= a b))}`.

Returns: The corresponding certificate.

◆ cnot_implies1()

CERTIF cnot_implies1	(	char *	name,
		CERTIF	c
	)

not_implies1 rule (number 37 in Alethe).

Given a proof of the clause {(not (=> a b))}, proves the clause {a}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (=> a b))}`.

Returns: The corresponding certificate.

◆ cnot_implies2()

CERTIF cnot_implies2	(	char *	name,
		CERTIF	c
	)

not_implies2 rule (number 38 in Alethe).

Given a proof of the clause {(not (=> a b))}, proves the clause {(not b)}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (=> a b))}`.

Returns: The corresponding certificate.

◆ cnot_or()

CERTIF cnot_or	(	char *	name,
		CERTIF	c,
		int	k
	)

not_or rule (number 29 in Alethe).

Given a proof of the clause {(not (or f1 ... fn))} and a non-negative integer k, proves the clause {(not fk)}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (or f1 ... fn))}`.
k	An integer between `1` and `n`.

Returns: The corresponding certificate.

◆ cnot_xor1()

CERTIF cnot_xor1	(	char *	name,
		CERTIF	c
	)

not_xor1 rule (number 34 in Alethe).

Given a proof of the clause {(not (xor a b))}, proves the clause {a (not b)}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (xor a b))}`.

Returns: The corresponding certificate.

◆ cnot_xor2()

CERTIF cnot_xor2	(	char *	name,
		CERTIF	c
	)

not_xor2 rule (number 35 in Alethe).

Given a proof of the clause {(not (xor a b))}, proves the clause {(not a) b}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(not (xor a b))}`.

Returns: The corresponding certificate.

◆ cor()

CERTIF cor	(	char *	name,
		CERTIF	c
	)

or rule (number 30 in Alethe).

Given a proof of the clause {(or f1 ... fn)}, proves the clause {f1 ... fn}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(or f1 ... fn)}`.

Returns: The corresponding certificate.

◆ cor_neg()

CERTIF cor_neg	(	char *	name,
		size_t	n,
		const EXPR *	fs,
		int	k
	)

or_neg rule (number 46 in Alethe).

Given the formulas f1 ... fn and a non-negative integer k, proves the tautological clause {(or f1 ... fn) (not fk)}.

Parameters

name	The unique name given to the proof step.
n	The number of formulas in the resulting disjunction.
fs	A pointer to the list of formulas.
k	An integer between `1` and `n`.

Returns: The corresponding certificate.

◆ cor_pos()

CERTIF cor_pos	(	char *	name,
		size_t	n,
		const EXPR *	fs
	)

or_pos rule (number 45 in Alethe).

Given the formulas f1 ... fn, proves the tautological clause {(not (or f1 ... fn)) f1 ... fn}.

Parameters

name	The unique name given to the proof step.
n	The number of formulas in the resulting disjunction.
fs	A pointer to the list of formulas.

Returns: The corresponding certificate.

◆ cresolution()

CERTIF cresolution	(	char *	name,
		size_t	nb,
		const CERTIF *	premisses
	)

th_resolution and resolution rules (number 6 and 7 in Alethe).

Resolution of two or more clauses.

Parameters

name	The unique name given to the proof step.
nb	The number of clauses to be resolved.
premisses	The proof of the clauses to be resolved.

Returns: The corresponding certificate.

◆ ctrue()

CERTIF ctrue ( char * name )

true rule (number 3 in Alethe).

Proves the tautological clause {true}.

Parameters

name	The unique name given to the proof step.

Returns: The corresponding certificate.

◆ cweakening()

CERTIF cweakening	(	char *	name,
		CERTIF	c,
		size_t	m,
		const EXPR *	bs
	)

weakening rule (additional).

Given a proof of the clause {f1 ... fn} and a possibly larger clause {f1 ... fn b[n+1] ... bm}, proves the clause {f1 ... fn b[n+1] ... bm}

The order does not matter. The initial clause may contain the additional literals not false and true as well.

Parameters

name	The unique name given to the proof step.
c	The proof of `{f1` ... fn}.
m	The number of literals in the final clause `{f1 ... fn b[n+1] ... bm}`.
bs	A pointer to the list of literals in the final clause.

Returns: The corresponding certificate.

◆ cxor1()

CERTIF cxor1	(	char *	name,
		CERTIF	c
	)

xor1 rule (number 32 in Alethe).

Given a proof of the clause {(xor a b)}, proves the clause {a b}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(xor a b)}`.

Returns: The corresponding certificate.

◆ cxor2()

CERTIF cxor2	(	char *	name,
		CERTIF	c
	)

xor2 rule (number 33 in Alethe).

Given a proof of the clause {(xor a b)}, proves the clause {(not a) (not b)}.

Parameters

name	The unique name given to the proof step.
c	The proof of `{(xor a b)}`.

Returns: The corresponding certificate.

◆ cxor_neg1()

CERTIF cxor_neg1	(	char *	name,
		EXPR	a,
		EXPR	b
	)

xor_neg1 rule (number 49 in Alethe).

Given the formulas a and b, proves the tautological clause {(xor a b) a (not b)}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the exclusive or.
b	The right-hand side formula of the exclusive or.

Returns: The corresponding certificate.

◆ cxor_neg2()

CERTIF cxor_neg2	(	char *	name,
		EXPR	a,
		EXPR	b
	)

xor_neg2 rule (number 50 in Alethe).

Given the formulas a and b, proves the tautological clause {(xor a b) (not a) b}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the exclusive or.
b	The right-hand side formula of the exclusive or.

Returns: The corresponding certificate.

◆ cxor_pos1()

CERTIF cxor_pos1	(	char *	name,
		EXPR	a,
		EXPR	b
	)

xor_pos1 rule (number 47 in Alethe).

Given the formulas a and b, proves the tautological clause {(not (xor a b)) a b}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the exclusive or.
b	The right-hand side formula of the exclusive or.

Returns: The corresponding certificate.

◆ cxor_pos2()

CERTIF cxor_pos2	(	char *	name,
		EXPR	a,
		EXPR	b
	)

xor_pos2 rule (number 48 in Alethe).

Given the formulas a and b, proves the tautological clause {(not (xor a b)) (not a) (not b)}

Parameters

name	The unique name given to the proof step.
a	The left-hand side formula of the exclusive or.
b	The right-hand side formula of the exclusive or.

Returns: The corresponding certificate.

Functions

Detailed Description

Function Documentation

◆ cand()

◆ cand_neg()

◆ cand_pos()

◆ cassume()

◆ ceq_congruent()

◆ ceq_congruent_pred()

◆ ceq_congruent_pred_b()

◆ ceq_reflexive()

◆ ceq_transitive()

◆ cequiv1()

◆ cequiv2()

◆ cequiv_neg1()

◆ cequiv_neg2()

◆ cequiv_pos1()

◆ cequiv_pos2()

◆ cfalse()

◆ cimplies()

◆ cimplies_neg1()

◆ cimplies_neg2()

◆ cimplies_pos()

◆ clia_generic()

◆ cnot_and()

◆ cnot_equiv1()

◆ cnot_equiv2()

◆ cnot_implies1()

◆ cnot_implies2()

◆ cnot_or()

◆ cnot_xor1()

◆ cnot_xor2()

◆ cor()

◆ cor_neg()

◆ cor_pos()

◆ cresolution()

◆ ctrue()

◆ cweakening()

◆ cxor1()

◆ cxor2()

◆ cxor_neg1()

◆ cxor_neg2()

◆ cxor_pos1()

◆ cxor_pos2()