Propositional lax logic (Q1368378)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Propositional lax logic |
scientific article |
Statements
Propositional lax logic (English)
0 references
26 November 1997
0 references
The authors investigate the use of a special intuitionistic modal logic with several applications to the performance evaluation of computer hardware. The logic contains a single modal operator enjoying aspects of ``possibility'' and ``necessity''. Several formal properties of the logic are well developed. E.g., (1) a cut-elimination theorem for the usual Gentzen-style sequent presentation of the logic, (2) a major Deduction Theorem, (3) the completeness of the logic with respect to Kripke constraint models, and (4) the finite model property for the logic relative to the class of constraint models. Early examples of mention of a similar modal operator by \textit{H. B. Curry} [A theory of formal deducibility (Notre Dame Math. Lectures, Volume 6) (1950; Zbl 0041.34807)] have come a long way!
0 references
propositional modal logic
0 references
Kripke models
0 references
hardware verification
0 references
intuitionistic modal logic
0 references
performance evaluation of computer hardware
0 references
0 references