Hierarchic Superposition with Weak Abstraction
Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even
|Collections||ANU Research Publications|
|01_Baumgartner_Hierarchic_Superposition_with_2013.pdf||220.78 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.