Theory superposition
theory superposition
imports Main terms equational_clausal_logic well_founded_continued "HOL-Library.Multiset"
multisets_continued
begin
section ‹Definition of the Superposition Calculus›
subsection ‹Extended Clauses›
text ‹An extended clause is a clause associated with a set of terms.
The intended meaning is that the terms occurring in the attached set are assumed to be in normal
form: any application of the superposition rule on these terms is therefore useless and can be
blocked. Initially the set of irreducible terms attached to each clause is empty. At each inference
step, new terms can be added or deleted from this set.›