Jump to content

Computability logic

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Luiz Vasconcelos Filho (talk | contribs) at 21:56, 26 April 2013. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Introduzida por Giorgi Japaridze em 2003, lógica de computabilidade é um programa de pesquisa e quadro matemático para reabilitação lógica como uma Teoria da Computabilidade formal sistemática, ao contrário da lógica clássica , a qual é uma teoria formal de prova. Nessa abordagem, fórmulas lógicas representam problemas computacionais(ou, equivalentemente, capacidades computacionais), e sua validade significa ser “sempre computável”.

Problemas e capacidades computacionais são compreendidas em seus sensos mais geral-interativos. Eles são formalizados como jogos entre a máquina e o seu meio, e computabilidade refere-se à existência de uma máquina que vença o jogo, qualquer que seja o comportamento do ambiente. Definindo o que seriam máquinas jogadoras, lógica de computabilidade provê a generalização da Tese de Church-Turing para o nível interativo.

O conceito clássico de verdade acaba se tornando[citation needed] uma caso especial de computabilidade, a Interatividade de Grau Zero. Isso faz da lógica clássica um fragmento especial da lógica de computabilidade. Sendo uma extensão conservadora do padrão, lógica de computabilidade é, ao mesmo tempo, pela ordem de magnitude mais expressiva, construtiva e computacionalmente significativa. Fornecendo uma resposta sistemática para a questão fundamental “quem (e como) pode ser computado?”, isso tem uma vasta gama de potenciais áreas de aplicação. Isso inclui teorias aplicadas construtivas, sistemas com base de conhecimento, sistemas de planejamento e ação.

Por trás da lógica clássica, lógica linear (compreendida em um senso simples) e lógica intuitiva também acabam se tornando fragmentos naturais do lógica de computabilidade. Logo, conceitos significativos de “verdade intuitiva” e “verdade de lógica linear” pode ser derivada a partir da semântica da lógica de computabilidade.

Sendo semanticamente construído, como ainda lógica de computabilidade não tem uma teoria de prova completamente desenvolvida. Encontrando sistemas dedutivos para fragmentos variados disso e explorando sua propriedades sintáticas é uma área de pesquisa em andamento.

Referências

  • 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.

Veja também

Template:Lógica