DEVELOPMENT

Print Friendly and PDF

 ENACTPROVER


Electronic Machine Program on Theorem Proving. 

(EMPROTHEP)


The introduction is on enact model theorems and axioms developed from these models by Kleene axioms or theorems. The goals and objectives of this project is detailed below. Methodology to be used in the implementation approach and conduct of research are also discussed.  

This research is on provable forms based on syntactic 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 in machine-level interpretation. Enactprover is a machine program for reading and writing Kleene theorem proving axioms based on enactment logic.



ENACTPROVER: GOALS AND OBJECTIVES


This research project has the following goals and objectives:


1.It is to implement an electronic machine provable solution capable of proving the model theorems of enactment logic.

2.It is to interprets the parameters of enact function with enactprover interpreter.

3.It is to stream the outputs into an integrated development environment (Enactprover IDE) for display and human reading on communication.

4.Realistic passing values will be enacted to bring much meaning tthe machine interpretation.

5.Novelty is in the programming style (color codes) of something of fellowship something of color. 

6.Novelty again is in the graphical user interface theme in the development process.


Download: Link

This article work is on a preprint server at ScienceOpen. Check for doi at the download page. 

Comments