| has abstract
| - Computability logic (CoL) is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth. It was introduced and so named by Giorgi Japaridze in 2003. In classical logic, formulas represent true/false statements. In CoL, formulas represent computational problems. In classical logic, the validity of a formula depends only on its form, not on its meaning. In CoL, validity means being always computable. More generally, classical logic tells us when the truth of a given statement always follows from the truth of a given set of other statements. Similarly, CoL tells us when the computability of a given problem A always follows from the computability of other given problems B1,...,Bn. Moreover, it provides a uniform way to actually construct a solution (algorithm) for such an A from any known solutions of B1,...,Bn. CoL formulates computational problems in their most general – interactive sense. CoL defines a computational problem as a game played by a machine against its environment. Such problem is computable if there is a machine that wins the game against every possible behavior of the environment. Such game-playing machine generalizes the Church-Turing thesis to the interactive level. The classical concept of truth turns out to be a special, zero-interactivity-degree case of computability. This makes classical logic a special fragment of CoL. Thus CoL is a conservative extension of classical logic. Computability logic is more expressive, constructive and computationally meaningful than classical logic. Besides classical logic, independence-friendly (IF) logic and certain proper extensions of linear logic and intuitionistic logic also turn out to be natural fragments of CoL. Hence meaningful concepts of "intuitionistic truth", "linear-logic truth" and "IF-logic truth" can be derived from the semantics of CoL. CoL systematically answers the fundamental question of what can be computed and how; thus CoL has many applications, such as constructive applied theories, knowledge base systems, systems for planning and action. Out of these, only applications in constructive applied theories have been extensively explored so far: a series of CoL-based number theories, termed "clarithmetics", have been constructed as computationally and complexity-theoretically meaningful alternatives to the classical-logic-based Peano arithmetic and its variations such as systems of bounded arithmetic. Traditional proof systems such as natural deduction and sequent calculus are insufficient for axiomatizing nontrivial fragments of CoL. This has necessitated developing alternative, more general and flexible methods of proof, such as cirquent calculus. (en)
- La logica della computabilità (Computability logic o CoL) è un programma di ricerca e un modello matematico per riqualificare la logica come una teoria formale sistematica della computabilità, in contrapposizione alla logica classica che può essere vista come una teoria formale della verità. È stato presentata per la prima volta e così nominata da nel 2003. Se si confronta la CoL con la logica classica si potrebbe dire che, mentre nella seconda le formule rappresentano enunciati veri o falsi, nella CoL rappresentano problemi computazionali. Nella logica classica, la validità di una formula è intesa come "la formula è sempre vera", ossia indipendentemente dall'interpretazione delle sue sottoformule primitive (variabili extralogiche, cioè enunciati atomici). In modo simile, nella CoL validità significa essere sempre computabile. Più in generale, la logica classica ci dice quando la verità di un certo enunciato segue sempre dalla verità di un dato insieme di altri enunciati. Allo stesso modo, la CoL ci dice quando la computabilità di un certo problema A segue sempre dalla computabilità di altri problemi dati B1, ...,Bn. Inoltre, la CoL fornisce un metodo uniforme per realizzare effettivamente una soluzione (algoritmo) di tale problema A da qualsiasi soluzione nota di B1, ..., Bn. La logica della computabilità interpreta i problemi computazionali nel loro senso più generale - interattivo. Questi, infatti, sono formalizzati come giochi giocati da una macchina contro il suo ambiente, e la computabilità significa l'esistenza di una macchina che vince il gioco contro qualsiasi possibile comportamento dell'ambiente. Definendo il significato di queste macchine-giocatori, la CoL fornisce una generalizzazione della Tesi di Church-Turing al livello della computazione interattiva, che è anche il tipo usuale di computazione dei computer reali (con diversi input e output). Il classico concetto di verità risulta così essere un caso speciale con interattività di grado zero della computabilità. Questo rende la logica classica un frammento particolare della CoL. Essendo un'estensione conservativa della logica classica, la logica della computabilità è, allo stesso tempo, di un ordine di grandezza più espressiva, costruttiva e computazionalmente significativa. Oltre alla logica classica, l' (IF) e alcune estensioni proprie della logica lineare e della logica intuizionista si rivelano essere, parimenti, frammenti naturali della logica della computabilità. Quindi concetti significativi di "verità intuizionista", "verità lineare" e "IF-verità" possono essere derivati dalla semantica della CoL. Fornendo una risposta sistematica alla domanda fondamentale di ciò che può essere calcolato e come, CoL sostiene un'ampia gamma di potenziali aree applicative. Queste includono teorie costruttive applicate, knowledge base systems e sistemi di pianificazione e azione. Di questi, solo le applicazioni in teorie costruttive applicate sono state estesamente esplorate fino ad ora: sono state costruite una serie di teorie dei numeri basati sulla CoL, chiamate "clarithmetics", come alternative significative, dal punto di vista computazionale della teoria della complessità, dell'Aritmetica di Peano basata sulla logica classica e delle sue variazioni come i sistemi di aritmetica limitata. I tradizionali sistemi formali di dimostrazione come la deduzione naturale o il calcolo dei sequenti risultano insufficienti per l'assiomatizzazione di frammenti più o meno non triviali della CoL. Ciò ha comportato lo sviluppo di metodi di prova alternativi, più generali e flessibili, come il . (it)
- Introduzido por 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 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 para vários fragmentos disso e explorar suas propriedades sintáticas é uma área de pesquisa em contínuo andamento. (pt)
- 相对于是真理的形式理论的经典逻辑，在2003年发明的可计算性逻辑(Computability logic)是把逻辑恢复为系统的形式的可计算性理论的一个研究程序和数学框架。在这种方法下逻辑公式表示计算问题（或等价的计算资源），而它们的有效性意味着"总是可计算的"。 计算问题和资源的理解是在它们最一般的意义上的 - 交互的意义上的。它们被形式化为机器扮演的针对它的环境的游戏，而可计算性意味着存在着一个机器针对经由环境的任何可能行为赢得了游戏。定义了这种游戏扮演机器所意味的东西，可计算性逻辑在交互层面提供了邱奇-图灵论题的一般化。 真理的经典概念转变为可计算性的特殊的零交互度的情况。这使经典逻辑成为可计算性逻辑的特殊片段。作为前者的保守扩展的同时，可计算性逻辑有着一个数量级之上的表达力、创造性和计算意义。提供了对基本问题"什么是可以（如何）计算的?"的系统的回答，它有潜在的广泛的应用领域。其中包括构造性应用理论，知识库系统，计划和行动系统。 除了经典逻辑之外，线性逻辑（在不严格的意义上理解）和直觉逻辑也转变成可计算性逻辑的自然片段了。因为"直觉真理"和"线性逻辑真理"的有意义的概念可从可计算性逻辑的语义中推导出来。 正在做着语义构造，至今可计算性逻辑仍没有完全开发出证明论。为它的各种片段找到演绎系统并探索它们的性质是正在研究中的领域。 (zh)
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
