Index of types

find redundant clauses in ProofState.ActiveSet w.r.t the clause.

backward simplification by a unit clause.

A hook to convert a particular statement into a list of clauses

num^power divides monome or not.

An extension is allowed to modify an environment

Generation of clauses regardless of current clause

An inference returns a list of conclusions

Rule that checks whether the clause is trivial (a tautology)

Classification of proof steps

Rewrite rule on literals

(maybe) rewrite a clause to a set of clauses.

Proof Step with its conclusion

Some values are parametrized by the list of statements

Additional data carried in the literal

Actions that modify the set of rules Compute_prec

might print the literal on the given buffer.

check whether the clause is redundant w.r.t the set

Rewrite system

Simplify the clause structurally (basic simplifications), in the simplification monad.

List of constraints (term = monome).

Full description of a position in a literal.

statistics on clauses : num active, num passive, num simplification

statistics on the state (num active, num passive, num simplification)

The SZS status of a state

Monad type, representing an action starting at phase 'p1 and stopping at phase 'p2

A context is represented as a regular array of literals, containing at least one specific variable x, paired with this variable x.

focus on a term in one of the two monomes

A monome over terms, with coefficient of type 'a

A proof step, without the conclusion

Array of literals

a literal, that is, a signed atomic formula

An extension contains a number of actions that can modify the Flex_state.t during preprocessing, or modify the Env_intf.S once it is built.

attribute a weight to a clause.

Eligibility criterion for a literal

A priority queue.

Rewrite rule on terms

A boolean valuation