Related papers: A new graphical calculus of proofs
This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $\lambda$-calculus giving a computational semantics for deductions in $\mathsf{IEL}^{-}$. By using…
This is a survey of {\lambda}-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and…
Propositional G\"odel logic extends intuitionistic logic with the non-constructive principle of linearity $A\rightarrow B\ \lor\ B\rightarrow A$. We introduce a Curry-Howard correspondence for this logic and show that a particularly simple…
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…
This paper is the second part of an introduction to linear logic and ludics, both due to Girard. It is devoted to proof nets, in the limited, yet central, framework of multiplicative linear logic and to ludics, which has been recently…
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given…
We considers how a particular kind of graph corresponds to multiplicative intuitionistic linear logic formula. The main feature of the graphical notation is that it absorbs certain symmetries between conjunction and implication. We look at…
Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for every two statements the first implies the second or the second implies the first. We present a natural deduction and a Curry-Howard correspondence for…
The syntactic nature of logic and computation separates them from other fields of mathematics. Nevertheless, syntax has been the only way to adequately capture the dynamics of proofs and programs such as cut-elimination, and the finiteness…
We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and…
This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem provers allow for the…
We introduce the notion of coherent graphs, and show how those can be used to define dynamic semantics for Multiplicative Linear Logic (MLL) extended with non-determinism. Thanks to the use of a coherence relation rather than mere formal…
In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any…
Interaction nets are a graphical formalism inspired by Linear Logic proof-nets often used for studying higher order rewriting e.g. \Beta-reduction. Traditional presentations of interaction nets are based on graph theory and rely on…
A theory graph is a network of axiomatic theories connected with meaning-preserving mappings called theory morphisms. Theory graphs are well suited for organizing large bodies of mathematical knowledge. Traditional and formal proofs do not…
Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a…
We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part…
This paper provides a call-by-name and a call-by-value term calculus, both of which have a Curry-Howard correspondence to the box fragment of the intuitionistic modal logic IK. The strong normalizability and the confluency of the calculi…
The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic…
The original idea of proof nets can be formulated by means of interaction nets syntax. Additional machinery as switching, jumps and graph connectivity is needed in order to ensure correspondence between a proof structure and a correct proof…