A Machine-Level Interpretation of Deductive Rules on Enact I and Enact II Model Theorems.

This research proposal is on provable forms based on s yntactic theorem using Kleene Axiom schema. Enact model I and II of propositional formulas from enactment logic are proven in terms of theorems based on deductive rules. Work proves by deduction rules that Enact Model I and II are model theorems[1] in machinelevel interpretation. Enactprover is a machine program for reading and writing Kleene theorem proving axioms based one enactment logic.