@InProceedings{wirthtableau,
  author     ={Claus-Peter Wirth},
  title      ={Full First-Order Free Variable Sequents 
               and Tableaus in Implicit Induction},
  booktitle  ={Automated Reasoning with Analytic Tableaus and Related Methods
               (TABLEAU'99)},
  editor     ={Neil V. Murray},
  year       ={1999},
  series     ={Lecture Notes in Artificial Intelligence},
  number     ={1617},
  pages      ={293--307},
  note       ={{\url{http://www.ags.uni-sb.de/~cp/WWW/p/tab99/welcome.html}}},
  publisher  ={Springer},
  ISBN       ={3-540-66086-0},
  ISSN       ={0302-9743},
  abstract   ={We show how to integrate implicit inductive theorem proving 
into free variable sequent and tableau calculi
and compare the appropriateness of tableau calculi 
for this integration with that of sequent calculi.}}