Related papers: The computational content of classical arithmetic

A rather easy yet rigorous proof of a version of G\"odel's first incompleteness theorem is presented. The version is "each recursively enumerable theory of natural numbers with 0, 1, +, *, =, logical and, logical not, and the universal…

Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples.…

We study the first-order primal infon logic. It is the core of the policy language DKAL. We provide Gentzen-style calculi for two versions of this logic that are not equivalent. For both versions we investigate the semantics: one of them is…

A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into…

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…

We develop a classical model of computation (the S model) which captures some important features of quantum computation, and which allows to design fast algorithms for solving specific problems. In particular, we show that Deutsch's problem…

We refine the arithmetical hierarchy of various classical principles by finely investigating the derivability relations between these principles over Heyting arithmetic. We mainly investigate some restricted versions of the law of excluded…

The article gives a survey of mathematical proofs that rely on computer calculations and formal proofs.

It is discussed a practical possibility of a provable programming of mathematics basing on intuitionism and the dependent types feature of a programming language.The principles of constructive mathematics and provable programming are…

In this note we demonstrate that a number of case-heavy combinatorial proofs in the mathematical phylogenetics literature can be proven more compactly using computational support. We use these techniques to also prove several new…

We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a…

To enable the study of open sets in computational approaches to mathematics, lots of extra data and structure on these sets is assumed. For both foundational and mathematical reasons, it is then a natural question, and the subject of this…

Over extended systems of finite type arithmetic, we utilize a formal representation of the outer measure to define a translation which allows for the systematic formalization of probabilistic statements. As a main result, this translation…

We consider sets/relations/computations defined by *Elementary Inference Systems* I, which are obtained from Smullyan's *elementary formal systems* using Gentzen's notation for inference rules, and proof trees for atoms P(t_1,...,t_n),…

We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational…

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…

Grover's algorithm relies on the superposition and interference of quantum mechanics, which is more efficient than classical computing in specific tasks such as searching an unsorted database. Due to the high complexity of quantum…

This paper develops a proof-theoretic framework for abstract interpretation by systematically associating logical systems with finite abstractions. Building on earlier work on the internal logics of abstractions, we propose a general…

Inspired by the efficient proof procedures discussed in {\em Computability logic} \cite{Jap03,Japic,Japfin}, we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system and has the following…

Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been…