English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  A Phytography of WALDMEISTER

Löchner, B., & Hillenbrand, T. (2002). A Phytography of WALDMEISTER. AI Communications, 15, 127-133.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Löchner, Bernd1, Author           
Hillenbrand, Thomas1, 2, 3, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551              
3Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2003-07-292002
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: eDoc: 202144
Other: Local-ID: C1256104005ECAFC-4116BB9292AC8F43C1256C1D0040D29D-LoechnerHillenbrandAICOM2002
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: AI Communications
Source Genre: Journal
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 15 Sequence Number: - Start / End Page: 127 - 133 Identifier: ISSN: 0921-7126