---
title: "A Model Elimination Calculus for Generalized Clauses"
authors:
  - "Toni Bollinger"
doi: ""
url: "https://ijcai.org/proceedings/1991/19"
pdf: "https://ijcai.org/proceedings/1991/0019.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "126-130"
track: "Automated Reasoning"
keywords:
---

# A Model Elimination Calculus for Generalized Clauses

Toni Bollinger

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, pages 126-130.

## Abstract

Generalized clauses differ from (ordinary) clauses by allowing conjunctions of literals in the role of (ordinary) literals , i.e. they are disjlmctions of conjunctions of simple literals. An advantage of this clausal form is that implications with conjunctive conclusions or disjunctive premises are not split into multiple clallSes. An extension of Loveland's 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 instances of cmljunctive conclusions. Using these lemmas it is po11sible to avoid multiple proofs of the premises of implications with conjunctive conclusions.