×

The Church Rosser property in computer algebra and special theorem proving: an investigation of critical pair/completion algorithms. (English) Zbl 0562.68023

Dissertationen der Johannes Kepler-Universität Linz, 49. Linz: Johannes Kepler-Universität; Wien: Verband der Wissenschaftlichen Gesellschaften Österreichs (VWGÖ) 193 p. ÖS 180.00; DM 27.00 (1984).
This work deals with a very important property (the Church-Rosser property) of reduction relations which plays an outstanding role in specifying the decision procedure for the associated symmetric-reflexive- transitive closure of these relations. This property in connection with suited algorithms for the calculation of canonical forms is very useful in symbolic computation (computer algebra, automatic theorem proving, automatic generation and verification of programs). The author exhibits the aforementioned topic, the kernel of the work being the exposition of critical-pair/completion algorithms and of criteria for improving them.
Reviewer: V.Calmatuianu

MSC:

68W30 Symbolic computation and algebraic computation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68-02 Research exposition (monographs, survey articles) pertaining to computer science