@TechReport{wirthgreen,
year={1998},
author={Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}},
title={Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized {$\delta$}-Rule but Without {Skolemization}},
institution={FB Informatik, {Univ.\ Dortmund}},
type={Research Report (green/grey series)},
number={698/1998},
note={Short version in \salzername, \caferraname\ (\eds). \Proc\ \nth 2\,\Int\ Workshop on First-Order Theorem Proving (FTP'98), \PP{244}{255}, \Tech\ \Univ\ Vienna, 1998. Short version also in \cite[\PP{283}{298}]{ftpwien}. \url{http://www.ags.uni-sb.de/~cp/p/ftp98}, \url{http://arxiv.org/abs/0902.3730}},
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.},
}