This paper summarizes our investigations into the computational detection of secondary and tertiary structure of ribosomal RNA. We have developed a new automated procedure that not only identifies potential secondary and tertiary structural interactions, but also provides the covariation evidence that supports the proposed bondings, and any counterevidence that can be detected in the known sequences. A small number of previously unknown higher-order structural features have been detected in individual RNA molecules (16S rRNA and 7S RNA) through the use of our automated procedure. We are systematically studying mitochondrial rRNA, seeking tertiary structure within 16S rRNA and quaternary structure between 16S and 23S rRNA. To test hypotheses suggested by an examination of our program's output, our colleagues in biology are sequencing key portions of the 23S ribosomal RNA for species in which the known 16S ribosomal RNA exhibits variation (from the dominant pattern) at the site of a proposed bonding. Our ultimate hope is that automated covariation analysis will contribute significantly to a refined picture of ribosomal structure.

Two open questions m ternary Boolean algebras have been answered with the aid of an existmg automated theorem-proving program without recourse to any additional programming.The new automated theorem-provmg techraques developed in answering the open questions are presented here.Essentially, the ex~stmg theorem prover is used m a nonstandard way to seek and verify small fmite models and counterexamples for a first-order axiom system Exhibiting a model of an axiom system proves it consment; this facility complements traditional theorem-provmg methods, which can only prove mconslstency.

A new inference rule for resolution based theorem proving, termed qualified hyperresolution, is presented from a practical point of view. The method of qualification is intended to deal with clause sets involving not-everywhere-defined functions. Two examples illustrating the effects of the method are discussed in detail. The potential practical value of the method is indicated by substantial improvements over the performance of ordinary hyperresolution obtained in five test problems.