Get our free extension to see links to code for papers anywhere online!Free add-on: code for papers everywhere!Free add-on: See code for papers anywhere!
Abstract:We present a combination of raising, explicit variable dependency representation, the liberalized delta-rule, and preservation of solutions for first-order deductive theorem proving. Our main motivation is to provide the foundation for our work on inductive theorem proving, where the preservation of solutions is indispensable.
* Caferra, R. and Salzer, G., eds., Automated Deduction in Classical
and Non-Classical Logics (FTP'98), LNAI 1761, pp. 283-298, Springer, 2000 * ii + 40 pages