Related papers: Kuroda's Translation for Higher-Order Logic

Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for…

Several different proof translations exist between classical and intuitionistic logic (negative translations), and intuitionistic and linear logic (Girard translations). Our aims in this paper are (1) to consider extensions of…

The Kuroda negative translation translates classical logic only into intuitionistic logic, not into minimal logic. We present eight variants of the Kuroda negative translation that translate classical logic even into minimal logic. The…

The lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend lambda-PRK to…

Double-negation translations are used to encode and decode classical proofs in intuitionistic logic. We show that, in the cut-free fragment, we can simplify the translations and introduce fewer negations. To achieve this, we consider the…

In topos theory it is well-known that any nucleus j gives rise to a translation of intuitionistic logic into itself in a way which generalises the Goedel-Gentzen negative translation. Here we show that there exists a similar j-translation…

We extend the {\lambda}-calculus with constructs suitable for relational and functional-logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to unify…

It is standard to regard the intuitionistic restriction of a classical logic as increasing the expressivity of the logic because the classical logic can be adequately represented in the intuitionistic logic by double-negation, while the…

This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics…

In this note, we give a linear-size translation from formulas of first-order logic into equations of the calculus of relations preserving validity and finite validity. Our translation also gives a linear-size conservative reduction from…

We examine the interplay between projectivity (in the sense that was introduced by S.~Ghilardi) and uniform post-interpolant for the classical and intuitionistic propositional logic. More precisely, we explore whether a projective…

The $\lambda$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functional…

This paper aims to provide an analysis of what it means when we say that a pair of theories, very generously construed, are equivalent in the sense that they are interdefinable. With regard to theories articulated in first order logic, we…

Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform…

Notions of k-asimulation and asimulation are introduced as asymmetric counterparts to k-bisimulation and bisimulation, respectively. It is proved that a first-order formula is equivalent to a standard translation of an intuitionistic…

This report first shows the equivalence bewteen several formulations of classical logic in intuitionistic logic (tertium non datur, reductio ad absurdum, Pierce's law). Then it establishes the correctness of the G\"odel-Kolmogorov…

Many theories of semantic interpretation use lambda-term manipulation to compositionally compute the meaning of a sentence. These theories are usually implemented in a language such as Prolog that can simulate lambda-term operations with…

We find a translation with particularly nice properties from intuitionistic propositional logic in countably many variables to intuitionistic propositional logic in two variables. In addition, the existence of a possibly-not-as-nice…

One way of proving theorems in modal logics is translating them into the predicate calculus and then using conventional resolution-style theorem provers. This approach has been regarded as inappropriate in practice, because the resulting…

We propose an integration of possibility theory into non-classical logics. We obtain many formal results that generalize the case where possibility and necessity functions are based on classical logic. We show how useful such an approach is…