Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
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.
2018 ◽
Keyword(s):
2018 ◽
Vol 29
(8)
◽
pp. 1177-1216
2007 ◽
Vol 72
(4)
◽
pp. 1204-1218
◽
2018 ◽
Keyword(s):
Keyword(s):
2008 ◽
Vol DMTCS Proceedings vol. AI,...
(Proceedings)
◽