非表示:
キーワード:
-
要旨:
In many theorem proving applications, a proper treatment of
equational theories or equality is mandatory. In this paper we show
how to integrate a modern treatment of equality in the Model
Evolution calculus (ME), a first-order version of the propositional
DPLL procedure. The new calculus, MEE, is a proper extension of
the ME calculus without equality. Like ME it maintains an explicit
``candidate model'', which is searched for by DPLL-style splitting.
For equational reasoning MEE uses an adapted version of the ordered
paramodulation inference rule, where equations used for
paramodulation are drawn (only) from the candidate model. The
calculus also features a generic, semantically justified
simplification rule which covers many simplification techniques
known from superposition-style theorem proving. Our main result is
the refutational completeness of the MEE calculus.
