Module Lemma (.ml)

module Lemma: sig .. end

lemma learning

see the paper Lemma Learning in the Model Evolution Calculus by Peter Baumgartner, Alexander Fuchs, Cesare Tinelli.

common functionality used by the lemma learning modules (Lemma_lifted, Lemma_grounded).

These implement the computation of a lemma, i.e. a clause entailed by the problem clause set, from a closing context unifier. In essense this is done by resolution, starting with the closing clause, regressing over context literals used to close the clause, and resolving with the clauses on which the context literals were asserted. This is done recursively, till all assert literals are regressed, or some other termination criterion is met (like the unique implication point - UIP).

Types

type literal = Term.literal

Functions

val close_literal : literal

pseudo-context literal to regress, used to mark the regression task of the closing clause.

val simplify : literal list list -> literal list

accepts a list of literal lists, where each literal is the class of all regressed instances of the same context literal.

simplifies by trying to unify and reduce all instances of a class to a singleton.