Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
Articles
Romas Alonderis
Institute of Mathematics and Informatics
Published 2008-12-21
https://doi.org/10.15388/LMR.2008.18105
PDF

Keywords

Glivenko theorem
classical propositional sequent calculus
intuitionistic propositional sequent calculus

How to Cite

Alonderis R. (2008) “Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus”, Lietuvos matematikos rinkinys, 48(proc. LMS), pp. 256–262. doi: 10.15388/LMR.2008.18105.

Abstract

In the paper, we define some classes of sequents of the propositional intuitionistic logic. These are classes of primarily and α-primarily reducible sequents. Then we show how derivability of these sequents in a propositional intuitionistic logic sequent calculus LJ0 can be checked by means of a propositional classical logic sequent calculus LK0.

PDF
Creative Commons License

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

Please read the Copyright Notice in Journal Policy