An Updated Demodulation Strategy for Ring Problems

Robert Veroff
University of New Mexico, Albuquerque, NM 87131, U.S.A.
email: [email protected]

December 1994

Abstract. One of the objectives of a demodulation strategy is to minimize the proliferation of redundant information by keeping facts in a normal or canonical form. In this article we describe an updated version of a set of demodulators that was designed especially for problems in ring theory. The new set of demodulators, which takes advantage of features found in the automated reasoning program OTTER, is simpler and more efficient than the original.

Key words: automated reasoning programs, demodulation, ring theory

1. Introduction

In [4] we presented a set of demodulators designed especially for use by the automated reasoning program AURA [3] to solve problems in ring theory. Using this set of demodulators we were able to obtain a proof of a problem in ring theory|x3 = x implies commutativity| considered to be a benchmark problem for automated reasoning programs [1]. In the years since the original article was written, automated reasoning programs have become substantially more sophisticated. In this article we present a new set of demodulators designed to take advantage of features found in the automated reasoning program Otter [2]. These features include, for example,

built-in support for integers and integer arithmetic,

support for infix, prefix, and postfix operators,

demodulators that apply to entire literals instead of terms,

symbols that are effectively invisible with respect to the lexical ordering of terms,

evaluable functions and predicates, and

conditional demodulators|demodulators that apply only if a precondition evaluates to true.

Although the new set of demodulators essentially mimics the functionality of the original set, it is simpler, more intuitive, and more efficient.

2. Representation

Consider the following definition of a ring. A ring is a tuple (R; +; ?; ; e), where R is a
nonempty set of elements, + and ? are binary operations on R, is a unary operation on
R, e is an element of R, and the following axioms hold.