One Inference Mechanism based on Automated Theorem Proving

To combine the logic programming system and the conventional procedural programming system, we intend to introduce the production rules as a data type in Pascal. Then, the compiler system should have the ability to accept this type of data and the inference mechanism to respond the questions in the program. As a method of inferences, we pick out one method of automated theorem proving. In this paper, we describe how to prove the theorems in propositional logic and predicate logic, and to apply the method to the inference mechanism. We propose to transform the rules given as data into internal form to perform inference efficiently, and denote the role of rule-compiler