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
    0 references
    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

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references