A Model Elimination Calculus for Generalized Clauses.
Toni Bollinger · 1992
Generalized clauses differ from (ordinary) clauses by allowing conjunctions of literals in the role of (ordinary) literals, i.e. they are dis junctions of conjunctions of simple literals. An advantage of this clausal form is that implica tions with conjunctive conclusions or disjunc tive premises are not split into multiple clauses. An extension of Lovelands model elimination calculus [Loveland, 1969a, Loveland, 1978] is presented able to deal with such generalized clauses. Furthermore we describe a method for generating lemmas that correspond to valid in stances of conjunctive conclusions. Using these lemmas it is possible to avoid multiple proofs of the premises of implications with conjunctive conclusions. 1