- Authors
- Claus-Peter Wirth
- Title
- Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized delta-Rule but Without Skolemization, and now including Lemma Application
- In
- the web only
- 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.
Lemma application is now included into all calculi.
- Full paper
-
- Format
- .ps.gz
- Size
- .17 Mbytes
-
- Format
- .dvi.gz
- Size
- .11 Mbytes
-
The fonts of this version differ from the original
and some originally identical fonts are different in this version,
but the whole file can be searched!
- Format
- .pdf.gz
- Size
- .25 Mbytes