Publications: Electronic Proceedings Article: Citius altius fortius: Lessons learned from the Theorem Prover {WALDMEISTER}

Title*:	Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER
Attachment(s):	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, 06/22/2004

Edit History (please click the blue arrow to see the details)

	Editor(s) Thomas Hillenbrand	Created 05/26/2003 02:45:59 PM
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

Attachment Section

citius.ps

citius.ps