On some Systems of Minimal Propositional Logic with Loop Detection Mechanisms


  • Hovhannes Bolibekyan Yerevan State University


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.

Author Biography

Hovhannes Bolibekyan, Yerevan State University

Department of Informatics and Applied Mathematics


Bolibekyan H.R., Chubaryan A.A., On some proof systems for I. Johansson's minimal logic of predicates, Proceedings of the Logic Colloquium 2003, p. 56.

Gabbay D., Algorithmic proof with diminishing resources, Part 1, Springer Lecture Notes in Computer Science, 533, pp. 156-173, 1991

Bolibekyan H., Muradyan T., On some loop detection strategies for minimal propositional logic, Proceedings of the Logic Colloquium 2011, p. 45-46.




How to Cite

Bolibekyan, H. (2021). On some Systems of Minimal Propositional Logic with Loop Detection Mechanisms. Mathematical Problems of Computer Science, 38, 42–43. Retrieved from http://mpcs.sci.am/index.php/mpcs/article/view/481