Skip to main content
CSIRO Logo Data 61 logo

Model evolution with equality — revised and implemented

Authors

Peter Baumgartner, Bjoern Pelzer and Cesare Tinelli

NICTA

Universitaet Koblenz-Landau
Germany

The University of Iowa
USA

Abstract

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 superposition inference rule, where equations used for superposition 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 theoretical result is the correctness of the MEE calculus in the presence of very general redundancy elimination criteria. We also describe our implementation of the calculus, the E-Darwin system, and we report on practical experiments with it on the TPTP problems library.

BibTeX Entry

  @article{Baumgartner_PT_12,
    author           = {Baumgartner, Peter and Pelzer, Bjoern and Tinelli, Cesare},
    doi              = {10.1016/j.jsc.2011.12.031},
    number           = {9},
    month            = sep,
    year             = {2012},
    keywords         = {automated theorem proving, instance-based methods},
    title            = {Model Evolution with Equality --- Revised and Implemented},
    volume           = {47},
    pages            = {1011--1045},
    journal          = {Journal of Symbolic Computation},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/3983.pdf}
  }

Download