Propositional logic, or first-order logic, defines the fundamental rules for modeling Boolean relationships. It is used extensively within the field of computer science to model logical scenarios and represent situations that evaluate to a value of true or false.

Automated Theorem Proving (ATP) is the process of proving any mathematical theorem. In most cases, these theorems can be reduced to first-order logical expressions, and consequently, there are extensive tools to evaluate first-order logic. One method of ATP in logical expressions is modeled in the Boolean satisfiability (SAT) problem. The SAT problem asks whether a set of propositional formulas under Conjunctive Normal Form (CNF) is satisfiable. The SAT problem can be solved algorithmically, with optimizations to SAT-solving still being studied today.

The advancement of machine learning in natural language processing capabilities has led to a heightened interest in a machine’s ability to understand and model natural language as propositional logic, independent of human intermission. If a machine could model natural language in such a way, then proving facts and consistencies in articles could be highly automated. Further, the capability to model natural language as propositional logic could have further applications in software development to assist with debugging, finding loop invariants, or adhering to specifications.

This research bridges the gap between natural language and propositional logic by building and evaluating a novel end-to-end solution that takes English sentences modeled as logical scenarios and converts these into propositional logic expressions. From there, these expressions are converted to CNF and solved for satisfiability. This approach utilizes existing libraries and models to build this pipeline to evaluate methods of understanding English language as logical expressions.