|
| volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 1 van 10 gevonden artikelen
| Titel: |
A phytography of WALDMEISTER |
| Auteur: |
Bernd Löchner Thomas Hillenbrand |
| Verschenen in: |
AI communications |
| Paginering: | Jaargang 15 (2002) nr. 2-3 pagina's 127-133 |
| Jaar: |
2002-07-16 |
| Inhoud: |
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. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 1 van 10 gevonden artikelen
| volgende >> |