Related papers: Cut-restriction: from cuts to analytic cuts

Transition Algebra (TA) is a type of infinite logic introduced to discuss rewriting systems. The natural deductive proof systems already introduced in TA satisfy completeness for countable signatures. However, it lacks compactness, making…

Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent…

We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with…

A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal…

The notion of weak truth-table reducibility plays an important role in recursion theory. In this paper, we introduce an elaboration of this notion, where a computable bound on the use function is explicitly specified. This elaboration…

Completeness of a logic program means that the program produces all the answers required by its specification. The cut is an important construct of programming language Prolog. It prunes part of the search space, this may result in a loss…

We introduce a generic presentation of 'syntactic objects built by mixed induction and coinduction' encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a notion…

The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more…

These lecture notes survey the emerging area of Universal Proof Theory, which investigates general questions about the existence, equivalence, and characterization of good proof systems for broad classes of logics. In particular, the notes…

The paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction…

Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems.…

Accurately segmenting a citation string into fields for authors, titles, etc. is a challenging task because the output typically obeys various global constraints. Previous work has shown that modeling soft constraints, where the model is…

Decision trees are a widely used method for classification, both by themselves and as the building blocks of multiple different ensemble learning methods. The Max-Cut decision tree involves novel modifications to a standard, baseline model…

We explore the consequences of layering a Lambek proof system over an arbitrary (constraint) logic. A simple model-theoretic semantics for our hybrid language is provided for which a particularly simple combination of Lambek's and the proof…

Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of…

This paper develops a unified identification framework for counterfactual analysis in incomplete models characterized by support and moment restrictions. I demonstrate that identifying structural parameters and conducting counterfactual…

We show that if a theory R defined by a rewrite system is super-consistent, the classical sequent calculus modulo R enjoys the cut elimination property, which was an open question. For such theories it was already known that proofs strongly…

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development…

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…

We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and equational reasoning are mediated by the use of contextual…