Intuitionistic propositional calculus in the extended framework with modal operator. II

DOI10.2478/FORMA-2022-0001MaRDI QIDQ6489396zbMATH OpenFDO

Authors Takao Inoue, Riku Hanaoka

Publication date 22 April 2024

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

zbMATH Keywords

intuitionistic logicdeduction theoremconsequence operator

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• scientific article; zbMATH DE number 3935005
• scientific article; zbMATH DE number 3976993
• scientific article; zbMATH DE number 1873426
• Intuitionistic logic according to Dijkstra's calculus of equational deduction
• A strong completeness theorem in intuitionistic quantified modal logic

Cites work

• Constructivism in mathematics. An introduction. Volume II
• Intuitionism. An introduction. 3rd revised ed
• Logic and structure
• Mizar: state-of-the-art and beyond
• The role of the Mizar mathematical library for interactive proof development in Mizar

This page was built for publication: Intuitionistic propositional calculus in the extended framework with modal operator. II

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6489396)