Electronic Proceedings Article
@InProceedings
Internet-Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Hillenbrand, Thomas

dblp



Editor(s):

Dahn, Ingo
Vigneron, Laurent

dblp
dblp

Not MPII Editor(s):

Dahn, Ingo
Vigneron, Laurent

BibTeX cite key*:

Hillenbrand2003

Title, Conference

Title*:

Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER


citius.ps (357.05 KB)

Booktitle*:

Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03

Event Address*:

Valencia, Spain

URL of the conference:

http://rewriting.loria.fr/FTP-2003

Event Date*:
(no longer used):

June 12-14, 2003

URL for downloading the paper:

http://www1.elsevier.com/gej-ng/31/29/23/135/23/25/86.1.003.pdf

Event Start Date:

7 July 2003

Event End Date:

11 July 2003

Language:

English

Organization:


Publisher

Publisher's Name:

Elsevier

Publisher's URL:

http://www.elsevier.com/

Address*:

Amsterdam, The Netherlands

Type:

Invited Talk

Vol, No, pp., Year

Series:

Electronic Notes in Theoretical Computer Science

Volume:

86.1

Number:


Month:

June

Pages:

1-13



Sequence Number:


Year*:

2003

ISBN/ISSN:






Abstract, Links, ©

URL for Reference:


Note:


(LaTeX) Abstract:

In the last years, the development of automated theorem
provers has been advancing in a so to speak Olympic spirit,
following the motto "faster, higher, stronger"; and the
{Waldmeister} system has been a part of that endeavour. We
will survey the concepts underlying this prover, which
implements Knuth-Bendix completion in its unfailing variant.
The system architecture is based on a strict separation of
active and passive facts, and is realized via specifically
tailored representations for each of the central data
structures: indexing for the active facts, set-based
compression for the passive facts, successor sets for the
conjectures. In order to cope with large search spaces,
specialized redundancy criteria are employed, and the
empirically gained control knowledge is integrated to ease
the use of the system. We conclude with a discussion of
strengths and weaknesses, and a view of future prospects.

URL for the Abstract:

http://www1.elsevier.com/gej-ng/31/29/23/135/23/show/Products/notes/index.htt#003



Tags, Categories, Keywords:

Theorem Proving, Implementation of Logics

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

Expert

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort

BibTeX Entry:
@INPROCEEDINGS{Hillenbrand2003,
AUTHOR = {Hillenbrand, Thomas},
EDITOR = {Dahn, Ingo and Vigneron, Laurent},
TITLE = {Citius altius fortius: Lessons learned from the Theorem Prover {WALDMEISTER}},
BOOKTITLE = {Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03},
PUBLISHER = {Elsevier},
YEAR = {2003},
TYPE = {Invited Talk},
VOLUME = {86.1},
PAGES = {1--13},
SERIES = {Electronic Notes in Theoretical Computer Science},
ADDRESS = {Valencia, Spain},
MONTH = {June},
}


Entry last modified by Sabine Krott, 03/20/2007
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Thomas Hillenbrand
Created
03/20/2007 10:17:16 AM
Revisions
13.
12.
11.
10.
9.
Editor(s)
Sabine Krott
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Edit Dates
22.06.2004 10:28:50
17.06.2004 16:20:49
17.06.2004 15:41:49
14.06.2004 17:37:29
14.06.2004 17:16:55
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
citius.ps