Microcomputer translator for medical text: Theorem verification for chapter two of Zeman's modal logic

The increasing availability of computer readable documents and advances in computing power have created a renewed interest in computer translators. This paper describes the TRANSOFT medical document translator, a table-driven system written in American National Standard MUMPS, which handles a variety of translation problems. As one test of the TRANSOFT system, we submitted all theorems from Chapter Two of Zeman's Modal Logic to verification by Gentzen reduction and the Quine-McCluskey algorithm. Three apparent typographical errors were detected, but the translator otherwise confirmed the 179 theorems in this chapter. The TRANSOFT translator has the advantages of user control of the lexicon and grammar and sufficient conditions to prevent indefinite cycling of the program.