Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Löchner, Bernd
Hillenbrand, Thomas		dblp
dblp
Not MPG Author(s):
Löchner, Bernd

BibTeX cite key*:

LoechnerHillenbrandAICOM2002

Title

Title*:

A Phytography of WALDMEISTER

Journal

Journal Title*:

AI Communications
Journal's URL:

http://www.dbai.tuwien.ac.at/AICOM

Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

IOS Press
Publisher's URL:

http://www.iospress.nl

Publisher's
Address:

Amsterdam, the Netherlands
ISSN:

0921-7126

Vol, No, pp, Date

Volume*:

15
Number:

2-3

Publishing Date:

August 2002

Pages*:

127-133
Number of
VG Pages:

7

Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

The architecture of the {Waldmeister} prover for unit equational
deduction is based on a strict separation of active and passive
facts. After an inspection of the system's proof procedure, the
representation of each of the central data structures is outlined,
namely indexing for the active facts, compression for the passive
facts, successor sets for the hypotheses, and minimal recording of
inference steps for the proof object. 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. The paper concludes with a quantitative comparison of
the {Waldmeister} versions over the years, and a view of the future
prospects.

URL for the Abstract:


Categories,
Keywords:

Theorem Proving

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Intranet

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@ARTICLE{LoechnerHillenbrandAICOM2002,
AUTHOR = {L{\"o}chner, Bernd and Hillenbrand, Thomas},
 TITLE = {A Phytography of {WALDMEISTER}},
 JOURNAL = {AI Communications},
 PUBLISHER = {IOS Press},
 YEAR = {2002},
 NUMBER = {2-3},
 VOLUME = {15},
 PAGES = {127--133},
 ADDRESS = {Amsterdam, the Netherlands},
 MONTH = {August},
 ISBN = {0921-7126},
}

Entry last modified by Christine Kiesel, 03/12/2010
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
08/22/2002 01:48:02 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Christine Kiesel
Uwe Brahm
Thomas Hillenbrand
Christine Kiesel
Christine Kiesel		Edit Dates
29.07.2003 15:18:11
07/25/2003 01:49:21 PM
07/02/2003 09:17:47 PM
15.01.2003 15:13:25
15.01.2003 15:12:32