|
|||||
|
|
Violet |
|
| Authors: | Steve Greenbaum |
| Affiliation: | (1) Hewlett-Packard Laboratories, 1501 Page Mill Road, MS 4A-D, Palo Alto, CA 94304-1126, USA |
| Abstract: | Violet is an easy-to-use theorem prover based on locking resolution, with integrated equality extensions that use term rewriting and Knuth–Bendix completion. Violet participated in the CADE-13 ATP System Competition. |
| Keywords: | automated theorem proving competition Violet resolution locking term rewriting Knuth– Bendix completion |
| 本文献已被 SpringerLink 等数据库收录！ | |