相关论文: From truth to computability I

We explain how recent developments in the fields of realisability models for linear logic -- or geometry of interaction -- and implicit computational complexity can lead to a new approach of implicit computational complexity. This…

"Clarithmetic" is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html) instead of the more traditional classical or intuitionistic logics.…

The earlier paper "Introduction to clarithmetic I" constructed an axiomatic system of arithmetic based on computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html), and proved its soundness and extensional completeness with respect…

Computability logic (CoL) is a formal theory of interactive computation. It understands computational problems as games played by two players: a machine and its environment, uses logical formalism to describe valid principles of…

Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization CL18 of the basic propositional fragment of computability…

In this paper, we introduce a foundation for computable model theory of rational Pavelka logic (an extension of {\L}ukasiewicz logic) and continuous logic, and prove effective versions of some theorems in model theory. We show how to reduce…

Evidence-based reasoning is at the core of many problem-solving and decision-making tasks in a wide variety of domains. Generalizing from the research and development of cognitive agents in several such domains, this paper presents progress…

Several philosophical issues in connection with computer simulations rely on the assumption that results of simulations are trustworthy. Examples of these include the debate on the experimental role of computer simulations \cite{Parker2009,…

Within the program of finding axiomatizations for various parts of computability logic, it was proved earlier that the logic of interactive Turing reduction is exactly the implicative fragment of Heyting's intuitionistic calculus. That sort…

This letter introduces a new, substantially simplified version of the branching recurrence operation of computability logic (see http://www.cis.upenn.edu/~giorgi/cl.html), and proves its equivalence to the old, "canonical" version.

The theory of computational complexity focuses on functions and, hence, studies programs whose interactive behavior is reduced to a simple question/answer pattern. We propose a broader theory whose ultimate goal is expressing and analyzing…

The notion of weak truth-table reducibility plays an important role in recursion theory. In this paper, we introduce an elaboration of this notion, where a computable bound on the use function is explicitly specified. This elaboration…

Computational Logic is the use of computers to establish facts in a logical formalism. Originating in 19th-century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms,…

By nature, transmissible human knowledge is enumerable: every sentence, movie, audio record can be encoded in a sufficiently long string of 0's and 1's. The works of G\"odel, Turing and others showed that there are inherent limits and…

This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games…

Logic has its origins in basic questions about the nature of the real world and how we describe it. This article seeks to bring out the physical and epistemological relevance of some of the more recent technical work in logic and…

A major part of computability theory focuses on the analysis of a few structures of central importance. As a tool, the method of coding with first-order formulas has been applied with great success. For instance, in the c.e. Turing degrees,…

The field of computability and complexity was, where computer science sprung from. Turing, Church, and Kleene all developed formalisms that demonstrated what they held "intuitively computable". The times change however and today's…

Computability theory is traditionally conceived as the theoretical basis of informatics. Nevertheless, numerous proposals transcend computability theory, in particular by emphasizing interaction of modules, or components, parts,…

We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and…