Skip navigation
Skip navigation

Superposition and Model Evolution Combined

Baumgartner, Peter; Waldmann, Uwe

Description

We present a new calculus for first-order theorem proving with equality, Με+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-tri

CollectionsANU Research Publications
Date published: 2009
Type: Conference paper
URI: http://hdl.handle.net/1885/57194
Source: Proceedings of the 22nd International Conference on Automated Deduction
DOI: 10.1007/978-3-642-02959-2_2

Download

File Description SizeFormat Image
01_Baumgartner_Superposition_and_Model_2009.pdf273.74 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