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

This represents a cut on a formula, where we obtain a list of clauses cut_pos representing the formula itself with the trail lemma, and a boolean literal cut_lit that is true iff the trail is true.

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)

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

Rewrite rule on literals

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

Additional data carried in the literal

Actions that modify the set of rules Compute_prec

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

Bundle of clause sets

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

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 formula of the form forall vars. \bigand_i C_i.

A ground term of an inductive type.

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

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