Canonicalization and demodulation

Publisher Website
Google Scholar
Abstract
Mechanisms that were developed for the Argonne National Laboratory - Northern Illinois University theorem proving system are discussed. By defining special input clauses and demodulators, it is possible to simulate mathematical processes such as canonicalization of polynomials with no special programming. The mechanisms presented resulted from a study of the X/sup 3/ = X problem in ring theory. The use of the mechanisms allowed this problem to the solved for the first time by the automated theorem proving system.

This publication has 0 references indexed in Scilit: