Superposition and Model Evolution Combined
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
|Collections||ANU Research Publications|
|Source:||Proceedings of the 22nd International Conference on Automated Deduction|
|01_Baumgartner_Superposition_and_Model_2009.pdf||273.74 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.