# 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.

## References

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.

## Downloads

## Published

## How to Cite

*Mathematical Problems of Computer Science*,

*38*, 42–43. Retrieved from http://mpcs.sci.am/index.php/mpcs/article/view/481

## Issue

## Section

## License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.