Cesare Tinelli's Publications

Peter Baumgartner and Cesare Tinelli. The Model Evolution Calculus with Equality. In Proceedings of the 20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, 2005.

Abstract. In many theorem proving applications, a proper treatment of equa- tional 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, ME_E , 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 ME_E uses an adapted version of the ordered paramodu- lation inference rule, where equations used for paramodulation are drawn (only) from the candidate model. The calculus also features a generic, semantically justi- fied simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main result is the correctness of the ME_E calculus in the presence of very general redundancy elimination criteria.