From no-reply@arXiv.org Sat Feb 21 10:50:04 2009 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 n1L9o2D0014569 for ; Sat, 21 Feb 2009 10:50:04 +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 (single-drop); Sat, 21 Feb 2009 10:50:04 +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 ) id 1LaoQK-0002Vq-K8 for wirth@logic.at; Sat, 21 Feb 2009 10:45:28 +0100 Received: from dspam by mx.logic.tuwien.ac.at with spam-scanned (Exim 4.63) (envelope-from ) id 1LaoQK-0003gm-JT for wirth@logic.at; Sat, 21 Feb 2009 10:45:28 +0100 Received: from adminapp.mail.cornell.edu ([132.236.56.29]) by mx.logic.tuwien.ac.at with esmtp (Exim 4.63) (envelope-from ) id 1LaoQK-0003gh-67 for wirth@logic.at; Sat, 21 Feb 2009 10:45:28 +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 n1L9jOAS026572 for ; 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 n1L9jPWH026028 for ; 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 n1L9jOJE026026 for wirth@logic.at; Sat, 21 Feb 2009 04:45:24 -0500 Date: Sat, 21 Feb 2009 04:45:24 -0500 Message-Id: <200902210945.n1L9jOJE026026@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: RE: hput arXiv.tar.gz -> 0902.3730.tar.gz (0902.3730, 131kb) Reply-To: cs@arXiv.org X-FILTER-DSPAM: by mx.logic.tuwien.ac.at X-DSPAM-Result: Spam X-DSPAM-Processed: Sat Feb 21 10:45:28 2009 X-DSPAM-Confidence: 0.4949 X-DSPAM-Improbability: 1 in 99 chance of being ham X-DSPAM-Probability: 0.9900 X-DSPAM-Factors: 15, to+edit, 0.99000, listings, 0.99000, archives, 0.01000, foundation+for, 0.99000, at+Your, 0.99000, upper, 0.01000, unlikely, 0.01000, v3, 0.99000, line+so, 0.01000, unlikely+that, 0.01000, anonymous, 0.99000, paper+has, 0.01000, OFFICIAL, 0.99000, bytes, 0.01000, pride, 0.99000 To verify abstract and postscript, use http://arXiv.org/abs/0902.3730 Article-id: 0902.3730, Article password: di2nf (access still password restricted) Abstract will appear in mailing scheduled to begin at 20:00 Monday US Eastern time (i.e., Tue 24 Feb 09 01:00:00 GMT). Your title and abstract will appear in the next mailing exactly as below. (Except possibly for the NUMBER which IS NOT OFFICIAL until the next mailing of abstracts [20:00 US Eastern time (EDT/EST) Sun - Thu] -- it cannot be used to cross-list to other archives [e.g., from cs to math or physics] until after that time.) To correct any problems, you MUST replace NOW. Replacements on the same day (until the 16:00 US Eastern time deadline Mon-Fri) do not generate a revised date line, so do not hesitate to replace submission until everything is perfect (including removal of any extraneous files). ------------------------------------------------------------------------------ \\ arXiv:0902.3730 From: Claus-Peter Wirth 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. \\ Contains: 00README.XXX: 31 bytes amssymb.sty: 15232 bytes article.cls: 19939 bytes body.tex: 205286 bytes dina4.sty: 1336 bytes german.sty: 25453 bytes header.tex: 6838 bytes header12pt.tex: 3350 bytes headerarticle.tex: 826 bytes headerbiblio.tex: 12160 bytes headerforformulas.tex: 24663 bytes headerhot.tex: 39288 bytes headernamesrest.tex: 122312 bytes headerproof.tex: 806 bytes headersugarterms.tex: 1322 bytes headertheorem.tex: 6151 bytes makeidx.sty: 1776 bytes mssymb.sty: 9040 bytes pdf.tex: 153 bytes size12.clo: 8753 bytes specialfonts.tex: 18295 bytes times.sty: 883 bytes url.sty: 21092 bytes Stored as: 0902.3730.tar.gz (131kb) Warnings: Author 1: Claus-Peter Wirth arXiv.tar: unpacked 23 files from tar file PS files: 0902.3730.ps.gz (122kb) ------------------------------------------------------------------------------ Successful submission to the archives can be a significant source of pride and accomplishment. It entails many serious responsibilities: if you cannot check off on all of the items below, then you should replace your submission. (Note: *do not* resubmit, instead *replace*) ___ The Title/Author fields above are correct. ___ The abstract is complete, correct, and wrapped correctly. ___ Capitalization in title correct (we automatically lower case titles with excessive use of upper case, but we get some acronyms incorrect -- replace with uppercase letters only where they should be). ___ The authors are listed in `Firstname Lastname' order. ___ any anonymous ftp or http pointers to additional files are given in standard url format (e.g. ftp://myhost.domain/path/filename.ext or http://mywwwhost.domain/path/filename.html) ___ Periods are separated by a space from the end of any URL's ___ Any Journal-ref is a complete bibliographic reference to an already published version (includes volume and page number info in the case of a print journal). ___ All files including any figures were included. ___ This paper has not been submitted to any other arXiv.org e-print archives. ___ The full text of the paper itself is available directly from the archive. ___ The submission can be retrieved uncorrupted (TRY IT). Submitters who repeatedly leave errors uncorrected may lose submission privilege to the archives. (Replace using the current tentative paper number unless notified otherwise.) If your abstract is improperly wrapped, note that abstract linefill stops at whitespace indentation (e.g. a blank line or a line indented with space(s) denotes a new paragraph,and won't be wrapped). For further hints, keep reading or see http://arXiv.org/help/ . Guidelines for a proper title and abstract preparation are given at http://arXiv.org/help/prep . If you have not already read this, please read it now to ensure that you have followed the guidelines. It is an abuse of valuable archive admin time to edit abstracts by hand. If you need to replace this paper, then use the `replace' facility at http://arxiv.org/replace. Your entry will not officially appear in the listings until the next mailing goes out (and thus cannot yet be accessed via the search or the daily listings), and your paper number may be changed until that time, so it is necessary to wait a day before cross-listing, etc. DO NOT UNDER ANY CIRCUMSTANCES MAKE A DUPLICATE SUBMISSION OF THIS PAPER. A resubmission is treated as a separate submission, and given a new number, which will have to be removed by hand (and could result in loss of future submission privileges). Instead use the replace facility (see http://arxiv.org/help/replace). DO NOT UNDER ANY CIRCUMSTANCES MAKE A DUPLICATE SUBMISSION TO LIST THIS PAPER TO ANOTHER ARCHIVE within the arXiv system, since the system needs to know that it is one submission and not multiple. Instead use the cross-list facility (see http://arXiv.org/help/cross) to generate a cross-listing for it. ***NOTES*** 1) Avoid excessive cross-listings: cross-listings of a paper on archive-x to archive-y are intended for subjects of *direct* interest to subscribers of archive-y. Those subscribers of archive-y who have peripheral or direct interest in the subjects of archive-x are already subscribed to archive-x and neither need nor desire multiple receipt of the same abstract. (In particular, it is exceedingly unlikely that you could decide what is of direct interest to readers of archive-y if you yourself are not an active reader of archive-y.) 2) Common sense suggests that `replaced' papers are not immediately re-requested so if your intent is to communicate correct research it is in your interest to submit a final version in the first place, i.e. *avoid premature submissions*. If you later need to replace the submission, it would be helpful to indicate in the Comments: field (i.e. below Authors: ) how serious is the revision (e.g. v2: major conceptual changes, v3: minor grammatical changes, etc.), and include as a commented header in the revised version of the paper a guide to the changes for posterity.