de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

A Phytography of WALDMEISTER

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44934

Löchner,  Bernd
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44621

Hillenbrand,  Thomas
International Max Planck Research School, MPI for Informatics, Max Planck Society;
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-2F02-3
Zusammenfassung
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.