Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | 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:




MPG Subunit:


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/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
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