SemanticProver is the implementation of two main theories of logic; the first being that of a truth assignment, and the other being a metalogical framework to manipulate and reason about truth assignments. A truth assignment is simply a mapping between any known logical statement and its truth value in a logically possible world. When more than one situation is logically possible, truth assignments can be reasoned over as trees, giving the power of propositional completeness. Thus, SemanticProver can take any propositional argument, and efficiently determine whether that argument is valid or invalid.

Secondly, SemanticProver provides a formal definition of many meta-logical statements, including concepts of equivalence, contradiction and subsumption, and an automated reasoner which proves metalogical necessities about these concepts. This is achieved by representing metalogical concepts about logical sentences as necessary truth assignments, and reasoning over the truth assignments on the logical level. Then, truth assignments from forwards and backwards reasoning are unified to create a sound formal semantic proof (with all proper justifications of definition and semantic inference rules).

Finally, SemanticProver provides a user-friendly graphical interface which will display the truth assignment tree structures in a convenient, readable format, along with a corresponding list of inferences used to generate the tree. This GUI also includes many example problems in the built-in test suite which demonstrate SemanticProver’s use and efficiency. In its current state, SemanticProver is a promising direction for the unification of logic via automated metalogical proof, and is being extended to operate over full first-order logic (with identity and functions). Source code and an executable .jar can be found at https://github.com/kevingoneill/SemanticProver.