Lógica da computabilidade

Introduzido por Giorgi Japaridze em 2003, lógica da computabilidade é um programa de pesquisa e sistema matemático para re-desenvolver a lógica como uma teoria da computabilidade formal e sistemática, em confronto àlógica clássica, a qual é uma teoria de prova formal. Nessa abordagem, fórmulas lógicas representam problemas computacionais (ou, equivalentemente, recursos computacionais), e suas veracidades significam serem "sempre computáveis".

Problemas e recursos computacionais são entendidos em seu sentido mais interativo e geral. Eles são formalizados como jogos simulados por uma máquina perante o seu ambiente, e computabilidade significa a existência de uma máquina que vença o jogo contra qualquer comportamento possível do ambiente. Definindo o que máquinas simuladoras de jogos significam, lógica da computabilidade provê uma generalização da tese de Church-Turing para um nível interativo.

O conceito clássico de verdade acaba por ser um caso especial de computabilidade e de grau de interatividade zero. Sendo uma extensão conservativa da anterior, lógica da computabilidade é, ao mesmo tempo, por uma ordem de magnitude mais expressiva, construtiva e computacionalmente significativa. Prover uma resposta sistemática para a questão fundamental "o que (e como) pode ser computado?", possui um vasto leque de potenciais áreas de aplicação. Estas incluem teorias construtivas e aplicadas, sistemas de conhecimento básico, sistemas de planejamento e ação.

Além de lógica clássica, lógica linear (sendo entendido no sentido relaxado) e lógica intuicionista também acabam por ser fragmentos naturais da lógica da computabilidade. Portanto, conceitos importantes de "verdade intuitiva" e "verdade logico-linear" podem ser derivadas da semântica e da lógica da computabilidade.

Por ser semanticamente construído, lógica da computabilidade ainda não tem uma teoria de prova totalmente desenvolvida. Achar sistemas dedutivos para vários fragmentos disso e explorar suas propriedades sintáticas é uma área de pesquisa em contínuo andamento.

Referências

G. Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003), pages 1–99.

G. Japaridze, Propositional computability logic I. ACM Transactions on Computational Logic 7 (2006), pages 302-330.

G. Japaridze, Propositional computability logic II. ACM Transactions on Computational Logic 7 (2006), pages 331-362.

G. Japaridze, Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation 16 (2006), pages 489-532.

G. Japaridze, Computability logic: a formal theory of interaction. Interactive Computation: The New Paradigm. D.Goldin, S.Smolka and P.Wegner, eds. Springer Verlag, Berlin 2006, pages 183-223.

G. Japaridze, From truth to computability I. Theoretical Computer Science 357 (2006), pages 100-135.

G. Japaridze, From truth to computability II. Theoretical Computer Science 379 (2007), pages 20–52.

G. Japaridze, Intuitionistic computability logic. Acta Cybernetica 18 (2007), pages 77–113.

G. Japaridze, The logic of interactive Turing reduction. Journal of Symbolic Logic 72 (2007), pages 243-276.

G. Japaridze, The intuitionistic fragment of computability logic at the propositional level. Annals of Pure and Applied Logic 147 (2007), pages 187-227.

G. Japaridze, Cirquent calculus deepened. Journal of Logic and Computation 18 (2008), No.6, pp. 983–1028.

G. Japaridze, Sequential operators in computability logic^{[ligação inativa]}. Information and Computation 206 (2008), No.12, pp. 1443–1475.

G. Japaridze, Many concepts and two logics of algorithmic reduction. Studia Logica 91 (2009), No.1, pp. 1–24.

G. Japaridze, In the beginning was game semantics. Games: Unifying Logic, Language and Philosophy. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp. 249–350.

G. Japaridze, Towards applied theories based on computability logic. Journal of Symbolic Logic 75 (2010), pp. 565-601.

I. Mezhirov and N. Vereshchagin, On abstract resource semantics and computability logic. Journal of Computer and System Sciences 76 (2010), pp. 356-372.

N. Vereshchagin, Japaridze's computability logic and intuitionistic propositional calculus. Moscow State University, 2006.

Ver também

Lógica - Discute o uso de raciocínio em alguma atividade e é o estudo normativo, filosófico do raciocínio válido.
Lógica para computabilidade
Lógica do diálogo - Abordagem para a semântica formal que fundamenta os conceitos de verdade e validade no escopo de teoria dos jogos.
Computação interativa - Modelo matemático para o cálculo que envolve comunicação com o mundo externo.
Matemática - Ciência que estuda as propriedades e as relações entre os números.