Related papers: Proof Nets for PiL (Full Version)
We have developed a web-based pedagogical proof assistant, the Proof Tree Builder, that lets you apply rules upwards from the initial goal in sequent calculus and Hoare logic for a simple imperative language. We equipped our tool with a…
We introduce sound and complete labelled sequent calculi for the basic normal non-distributive modal logic L and some of its axiomatic extensions, where the labels are atomic formulas of the first order language of enriched formal contexts,…
Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the…
Clausal Language (CL) is a declarative programming and verifying system used in our teaching of computer science. CL is an implementation of, what we call, $\mathit{PR}{+}I\Sigma_1$ paradigm (primitive recursive functions with…
One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the…
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the…
This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of…
Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent…
Probabilistic extensions of logic programming languages, such as ProbLog, integrate logical reasoning with probabilistic inference to evaluate probabilities of output relations; however, prior work does not account for potential statistical…
We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used to establish a cut elimination argument for both calculi. In…
Petri nets provide accurate analogues to chemical reaction networks, with places representing individual molecules (the resources of the system) and transitions representing chemical reactions which convert educt molecules into product…
In this paper, we introduce a variant of the Lambek calculus allowing empty antecedents. This variant uses two connecives: the left division and a unary modality that occurs only with negative polarity and allows weakening in antecedents of…
We further develop the theoretical framework of proof mining, a program in mathematical logic that seeks to quantify and extract computational information from prima facie `non-computational' proofs from the mainstream mathematical…
We study conditions for a concurrent construction of proof-nets in the framework developed by Andreoli in recent papers. We define specific correctness criteria for that purpose. We first study closed modules (i.e. validity of the execution…
We show that a proof in multiplicative linear logic can be represented as a decorated surface, such that two proofs are logically equivalent just when their surfaces are geometrically equivalent. This is an extended abstract for…
Statistical network calculus is the probabilistic extension of network calculus, which uses a simple envelope approach to describe arrival traffic and service available for the arrival traffic in a node. One of the key features of network…
Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, however, its deployment…
Recently, Logic Explained Networks (LENs) have been proposed as explainable-by-design neural models providing logic explanations for their predictions. However, these models have only been applied to vision and tabular data, and they mostly…
We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded…
In this paper, we extend an available neural network verification technique to support a wider class of piece-wise linear activation functions. Furthermore, we extend the algorithms, which provide in their original form exact respectively…