Related papers: Cut-restriction: from cuts to analytic cuts
Multiplicative-Additive System Virtual (MAV) is a logic that extends Multiplicative-Additive Linear Logic with a self-dual non-commutative operator expressing the concept of "before" or "sequencing". MAV is also an extenson of the the logic…
This paper proposes a basic proof theoretic framework for major modal logics: {\sf S5} and some of its subsystems. The framework is based on a version of hypersequent calculus, and the basic modal systems we handle here are the system {\sf…
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…
A non-deterministic call-by-need lambda-calculus \calc with case, constructors, letrec and a (non-deterministic) erratic choice, based on rewriting rules is investigated. A standard reduction is defined as a variant of left-most outermost…
We focus on the persistence principle over weak interpretability logic. Our object of study is the logic obtained by adding the persistence principle to weak interpretability logic from several perspectives. Firstly, we prove that this…
We present two deductively equivalent calculi for non-deterministic many-valued logics. One is defined by axioms and the other - by rules of inference. The two calculi are obtained from the truth tables of the logic under consideration in a…
Recent studies on frequent itemset mining algorithms resulted in significant performance improvements. However, if the minimal support threshold is set too low, or the data is highly correlated, the number of frequent itemsets itself can be…
One often sees a sharp distinction in mathematics between descriptions from the outside and from the inside. Think of defining a set in the plane through an algebraic equation, or dynamically as the closure of the orbit of some point under…
Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called proof links to the standard first-order LK-calculus. Proof links allow proofs to reference proofs thus giving…
This paper revisits the problem of determinacy inference addressing the problem of how to uniformly handle cut. To this end a new semantics is introduced for cut, which is abstracted to systematically derive a backward analysis that derives…
One recurring problem in program development is that of understanding how to re-use code developed by a third party. In the context of (constraint) logic programming, part of this problem reduces to figuring out how to query a program. If…
Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive…
Pure, or type-free, Linear Logic proof nets are Turing complete once cut-elimination is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing the complexity of cut-elimination to be…
Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives. As a consequence, we can give a subatomic proof system for…
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This…
Motivated by applications in declarative data analysis, we study $\mathit{Datalog}_{\mathbb{Z}}$---an extension of positive Datalog with arithmetic functions over integers. This language is known to be undecidable, so we propose two…
While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the…
Pull-tabbing is an evaluation approach for functional logic computations, based on a graph transformation recently proposed, which avoids making irrevocable non-deterministic choices that would jeopardize the completeness of computations.…
Retrograde analysis reads programs from the end to the beginning: treat statements as constraints on prior states, propagate sets of states backward, and compare the reachable inputs with the intended specification. This tutorial condenses…
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…