Return-Path: no-reply@arXiv.org
Delivery-Date: Sat Feb 21 10:50:06 2009
X-Spam-Checker-Version: SpamAssassin 3.1.8 (2007-02-13) on zhuangzi.site
X-Spam-Level: 
X-Spam-Status: No, score=-102.3 required=5.0 tests=AWL,BAYES_00,
	UNPARSEABLE_RELAY,USER_IN_WHITELIST autolearn=ham version=3.1.8
Received: from zhuangzi.site (localhost [127.0.0.1])
	by zhuangzi.site (8.13.8/8.13.8/SuSE Linux 0.8) with ESMTP id n1L9o2D1014569
	for <cp@localhost>; Sat, 21 Feb 2009 10:50:06 +0100
Envelope-to: wirth@logic.at
Received: from mail.logic.at [128.130.175.3]
	by zhuangzi.site with POP3 (fetchmail-6.3.5)
	for <cp@localhost> (single-drop); Sat, 21 Feb 2009 10:50:06 +0100 (CET)
Received: from mx.logic.tuwien.ac.at ([128.130.175.19])
	by gamma.logic.tuwien.ac.at with esmtp (Exim 4.63)
	(envelope-from <no-reply@arXiv.org>)
	id 1LaoQM-0002Vt-TA
	for wirth@logic.at; Sat, 21 Feb 2009 10:45:30 +0100
Received: from dspam by mx.logic.tuwien.ac.at with spam-scanned (Exim 4.63)
	(envelope-from <no-reply@arXiv.org>)
	id 1LaoQM-0003gu-SW
	for wirth@logic.at; Sat, 21 Feb 2009 10:45:30 +0100
Received: from adminapp.mail.cornell.edu ([132.236.56.29])
	by mx.logic.tuwien.ac.at with esmtp (Exim 4.63)
	(envelope-from <no-reply@arXiv.org>)
	id 1LaoQM-0003gg-Gw
	for wirth@logic.at; Sat, 21 Feb 2009 10:45:30 +0100
Received: from arxiv.org (arxiv1.library.cornell.edu [128.84.158.114])
	by adminapp.mail.cornell.edu (8.13.6/8.12.6) with ESMTP id n1L9jOgv026575
	for <wirth@logic.at>; Sat, 21 Feb 2009 04:45:24 -0500 (EST)
Received: from arxiv1.library.cornell.edu (localhost.localdomain [127.0.0.1])
	by arxiv.org (8.13.1/8.13.1) with ESMTP id n1L9jPcM026033
	for <wirth@logic.at>; Sat, 21 Feb 2009 04:45:25 -0500
Received: (from e-prints@localhost)
	by arxiv1.library.cornell.edu (8.13.1/8.13.1/Submit) id n1L9jPs4026032
	for wirth@logic.at; Sat, 21 Feb 2009 04:45:25 -0500
Date: Sat, 21 Feb 2009 04:45:25 -0500
Message-Id: <200902210945.n1L9jPs4026032@arxiv1.library.cornell.edu>
X-Authentication-Warning: arxiv1.library.cornell.edu: e-prints set sender to no-reply@arXiv.org using -f
Precedence: bulk
X-Supported-By: U.S. National Science Foundation, Agreement 0132355 (7/01-6/04)
From: no-reply@arXiv.org
To: wirth@logic.at
Subject: 0902.3730 password (SAVE)
Reply-To: cs@arXiv.org
X-FILTER-DSPAM: by mx.logic.tuwien.ac.at
X-DSPAM-Result: Innocent
X-DSPAM-Processed: Sat Feb 21 10:45:30 2009
X-DSPAM-Confidence: 0.6393
X-DSPAM-Improbability: 1 in 178 chance of being spam
X-DSPAM-Probability: 0.0000
X-DSPAM-Factors: 27,
	foundation+for, 0.99000,
	before+it, 0.99000,
	R+and, 0.01000,
	Date+Sat, 0.99000,
	solutions+for, 0.01000,
	the+foundation, 0.99000,
	theorem, 0.01057,
	theorem, 0.01057,
	Logics, 0.01152,
	first+order, 0.01798,
	to+replace, 0.02091,
	the+article, 0.03104,
	the+article, 0.03104,
	variable, 0.03235,
	it+If, 0.04097,
	rule+and, 0.04097,
	allow+the, 0.04097,
	Automated, 0.04734,
	AI, 0.05234,
	this+article, 0.05388,
	this+article, 0.05388,
	License, 0.05687,
	Informatik, 0.05784,
	GMT, 0.06021,
	motivation, 0.06021,
	Salzer, 0.06464,
	proving, 0.06533

            *** 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 <wirth@logic.at>
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.
\\