Skip navigation
Skip navigation

A Combined Superposition and Model Evolution Calculus

Baumgartner, Peter; Waldmann, Uwe


We present a new calculus for first-order theorem proving with equality, Mσ+Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-triv

CollectionsANU Research Publications
Date published: 2010
Type: Journal article
Source: Journal of Automated Reasoning
DOI: 10.1007/s10817-010-9214-x


File Description SizeFormat Image
01_Baumgartner_A_Combined_Superposition_and_2010.pdf659.1 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator