A PROGRAM FOR GENERATING AND ANALYZING TERM REWRITING SYSTEMS

摘要: This thesis presents new results in the use of term rewriting systems for automatic theorem proving. The design and implementation REVE 2, a computer program that incorporates these results, is described. In addition, an introduction to basic theory, procedures, algorithms provided, manner suitable non-specialists. A principal application reasoning about equational inductive theories associated with finite set axioms. this context, Knuth-Bendix completion procedure typically used hope constructing confluent termination system from proofs theorems have been: 1) need user interaction, 2) lack available state-of-the art implementations. 2 reduces interaction two ways. First, it uses orderings whose implementations automatically compute all possible valid extensions ordering allow unorderable equation be ordered. Second, robust, task-based, failure-resistant fine-grained scheme postponement. From beginning, has been fundamental goal make well-documented, highly-modular, easily-modified program, based on sound principles software engineering. interface designed ease by both novice expert.