On some Systems of Minimal Propositional Logic with Loop Detection Mechanisms

Abstract

Backwards proof search and theorem proving with a standard cut-free calculus for the propositional fragment of minimal logic is insufficient because of three problems. Firstly, the proof search is not in general terminating caused by the possibility of looping. Secondly, it might generate proofs which are permutations of each other and represent the same natural deduction. Finally, during the proof some choice should be made to decide which rules to apply and where to use them.