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