Potentials of General-Purpose Reasoning Assistant System EUODHILOS
Hajime Sawamura, Toshiro Minami · Institutional Repositories DataBase (IRDB) · 1989
Much work has been done on special-purpose reasoning assistant systems whose underlying logics are fixed.In contrast with such a trend, this paper is devoted to a new dimension of computer-assisted reasoning research, that is, a general-purpose reasoning assistant system that aUows a user to defme his or her own logical system relevant for the objects in the problem domain and to reason about them.In the first half of the paper, the need, significance and design principle of EUODHLOS : a general- purpose system for computer-assisted reasoning, are discussed, then the system overview is described, placing emphases on the following three points: (1) formal system description language, (2) proving methodology based on several sheets for logical thought, (3) visual human-computer interface for reasoning.In the latter half, the potentials and usefulness of EUODHLOS are demonstrated through experiments and experiences of its use by a number of logics and proof examples therein, which have been used or devised in computer science, nificial inteMgence and so on. $m\cdot IRODUC\Pi ON$A new dimension of computer-assisted reasonin $g$ research is being explored in this paper.It aims at a general-purpose reasoning assistant system that aUows a user to interactively defme the syntax and inference rules of a formal system and to consffuct proofs in the defmed system.We have named such a system EUODHILOS, an acronym reflecting our philosophy or observation that every universe ae $4iscourseAasirs\Phi^{icalgtructure}$, which turns out to spell and sound like a Greek philosopher's name.In these days, various logics play important and even essential roles in computer science and artificial intelligence (e.g., [Tumer 84], [Genesereth 87], [Smets 88], [Thisdewaite 88]),