A Combined Superposition and Model Evolution Calculus
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
|Collections||ANU Research Publications|
|Source:||Journal of Automated Reasoning|
|01_Baumgartner_A_Combined_Superposition_and_2010.pdf||659.1 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.