- Claus-Peter Wirth
- Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization
- Caferra, R. and Salzer, G., eds.,
Automated Deduction in Classical and Non-Classical Logics
LNAI 1761, pp. 283-298, Springer, 2000
- Cite as
- Copyright Owner
- There is a significantly
improved and extended version!
There is a long version!
- 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
- Complete Referee Reports ("JUSTIFICATION AND GENERAL COMMENTS" word-for-word)
- Full paper
- .07 Mbytes