Skip navigation
Skip navigation

A Combined Superposition and Model Evolution Calculus

Baumgartner, Peter; Waldmann, Uwe

Description

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
URI: http://hdl.handle.net/1885/58990
Source: Journal of Automated Reasoning
DOI: 10.1007/s10817-010-9214-x

Download

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:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator