Some New Propositional Proof Systems for Intuitionistic and Minimal Logics

Abstract

One of the most fundamental problems of the proof complexity theory is to find an efficient proof system for propositional calculus. The investigations of proof complexity start for the systems of Classical Propositional Logic (CPL). However, natural real conclusions have constructive character in most cases. Therefore the investigation of the proofs complexities is important for systems of Intuitionistic Propositional Logic (IPL) and in some cases also for Minimal (Johansson's) Propositional Logic (MPL).
Many of the proof systems of classical propositional logic use presentation of tautologies or contradictions in disjunctive normal forms (DNF) or in conjunctive normal forms (CNF), but such presentations for non-classical tautologies are not entirely correct.
By analogy with the notions of determinative conjuncts and determinative DNF, given in [1] for classical tautologies, we introduce the same notions for non-classical tautologies and give the algorithms for construction of I-determinative DNF and M-determinative DNF for intuitionistic and minimal tautologies accordingly [2].
On the base of introduced non-classical determinative DNF we can define for IPL and MPL the analogies of well-known classical proof systems Res(k), R(lin), Cutting Plannes(CP), wich are different generalizations of resolution system R.
We denote the introduced systems by IRes(k), IR(lin), ICP and MRes(k), MR(lin), MCP for IPL and MPL accordingly.
To compare the efficiencies of introduced systems with the known non-classical resolution systems IR and MR we use the well-known notion of exponential speed-up from [3].