Name
Abstract | ||
|---|---|---|
Abstract: IntroductionWe present recent developments within the equational theorem prover Waldmeister,an implementation of unfailing Knuth-Bendix completion [BDP89]with renements towards ordered completion. The new developments rely ona novel organization of the underlying saturation-based proof procedure into asystem architecture. As is known, the saturation process tends to quicklyll thememory available unless preventive measures are employed. To overcome thisproblem, our new \Waldmeister... |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/978-3-540-45085-6_27 | Lecture Notes in Artificial Intelligence |
Keywords | Field | DocType |
theorem prover | Discrete mathematics,Computer science,Automated theorem proving,Algorithm,Systems architecture,Proof procedure,Equational theory | Conference |
Volume | ISSN | Citations |
2741 | 0302-9743 | 11 |
PageRank | References | Authors |
0.60 | 6 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| jeanmarie gaillourdet | 1 | 16 | 1.73 |
| Thomas Hillenbrand | 2 | 190 | 15.90 |
| Bernd Löchner | 3 | 97 | 8.68 |
| hendrik spies | 4 | 11 | 0.60 |
| franz baader | 5 | 34 | 2.97 |