Logic Proofs = Ideal inclusions
Roger Germundsson · 1991
: The two approaches of propositional logic (semantic and proof theoretic) are found to have equivalent formulations in commutative algebra over finite fields. In particular the semantic approach corresponds to an algebro geometric formulation and the proof theoretic corresponds to an ideal theoretic framework. Based on this correspondence a new completeness proof is given. An implementation of this proof system in Mathematica is also given which basically is based on Grobner basis computations. Keywords: Sematics, Proof Theory, Ideal, Algebraic Geometry, Variety, Grobner Bases 1 Introduction This section presents the major results and the disposition of the article. The basic idea of this article is to use algebraic methods to do (propositional) logic proofs. More specifically logic propositions may be mapped to polynomials in such a way that truth values are preserved. By using this representation one can simulate logic proofs in either of two modes: Semantic: The semantic approach...