Logics For Computability

Logics for computability are formulations of logic which capture some aspect of computability as a basic notion. This usually involves a mix of special logical connectives as well as semantics which explains how the logic is to be interpreted in a computational way.

Probably the first formal treatment of logic for computability is the realizability interpretation by Stephen Kleene in 1945, who gave an interpretation of intuitionistic number theory in terms of Turing machine computations. His motivation was to make precise the Heyting-Brouwer-Kolmogorov (BHK) interpretation of intuitionism, according to which proofs of mathematical statements are to be viewed as constructive procedures.

With the rise of many other kinds of logic, such as modal logic and linear logic, and novel semantic models, such as game semantics, logics for computability have been formulated in several contexts. Here we mention two.

Read more about Logics For Computability:  Modal Logic For Computability, Japaridze's Computability Logic

Famous quotes containing the word logics:

    When logics die,
    The secret of the soil grows through the eye,
    And blood jumps in the sun;
    Above the waste allotments the dawn halts.
    Dylan Thomas (1914–1953)