TEXT EDITING AND BEYOND - A STUDY IN LOGIC MODELING

This paper presents a logic modeling exercise in which we develop, tes t and implement a logic model for a text editor and use it to test exi sting text editing software. We begin by presenting a first order Horn logic axiomatization of a text editor by providing domain equations f or the primitive operations insert, delete and character retrieval. We show that this logic model captures the essential aspects of the text editing task and how more complex features are built using these prim itives. We discuss possible implementations and conclude that any oper ational semantics - the set of algorithms that perform the task - must be strongly related to the logic model we present. In other words, ea ch operational semantics constitutes a model of the logic theory. Next , we illustrate the usefulness of the model by implementing a basic te xt editing system and testing the correctness of an existing text edit or. We conclude by describing how we are integrating these modeling te chniques into a larger and more complex knowledge-based system.