On Designing the Method of Syntax Descriptions for Logics

概要

論文の詳細を見る
This paper deals with the feature of describing the syntax of logical expressions for the general-purpose (i. e. logic-independent) reasoning assistant system EUODHILOS. It is a system which assists us in reasoning in a variety of universes of discourse. This is why we call it general-purpose, and it follows that we have to define the logic to be dealt with at the beginning. It also gives us supports in the proofs of the theorems in the defined logic. In the system, a logic consists of language and derivation systems. The former consists of making fonts for new symbols and of describing the syntax of logical expressions. The latter consists of axioms with two kinds of rules ; inference and rewriting rules. In the current version, the style of inference rules is fixed like that of natural deduction. Rewriting rules are also given similarly. Therefore we have to take care mainly on the syntax description. At the rest of this paper, we show how the syntax is described in the current version and some ideas to improve it.
一般社団法人情報処理学会の論文
1989-10-16