Subject: 0902.3730 password (SAVE)
From: [email-masked]
To: [email-masked]
Date: Sat, 21 Feb 2009 04:45:25 -0500

*** SAVE THIS MESSAGE FOR FUTURE REFERENCE ***
          (and forward to any collaborators for safekeeping)

Your user/password combination for this article is

 User-ID: 0902.3730
 Password: di2nf

You will need this ID/password pair to do any of the following:

  - to check the article before it is announced
  - to cross-list the article 
  - to add publication information
  - to replace the article with a revised version

Keep this password safe -- all future replacements will require it.

If you submit this article to an overlay journal based on arXiv you may
need to supply the following identifier to allow the collaborating
service to track your submission: arXiv:tracking/ddd18165ffab4b90

------------------------------------------------------------------------------
\\
arXiv:0902.3730
From: Claus-Peter Wirth <[email-masked]>
Date: Sat, 21 Feb 2009 09:45:20 GMT   (131kb)

Title: Full First-Order Sequent and Tableau Calculi With Preservation of
  Solutions and the Liberalized delta-Rule but Without Skolemization
Authors: Claus-Peter Wirth
Categories: cs.AI cs.LO
Comments: ii + 40 pages
Report-no: Research Report 698/1998 (green/grey series), Fachbereich
  Informatik, University of Dortmund
Journal-ref: Caferra, R. and Salzer, G., eds., Automated Deduction in Classical
  and Non-Classical Logics (FTP'98), LNAI 1761, pp. 283-298, Springer, 2000
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
\\
  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.
\\