Author name cluster

Kaustuv Chaudhuri

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

TCS Journal 2019 Journal Article

Formalized meta-theory of sequent calculi for linear logics

Kaustuv Chaudhuri
Leonardo Lima
Giselle Reis

When studying sequent calculi, proof theorists often have to prove properties about the systems, whether to show that they are “well-behaved”, amenable to automated proof search, complete with respect to another system, consistent, among other reasons. These proofs usually involve many very similar cases, which leads to authors rarely writing them in full detail, only pointing to one or two more complicated cases. Moreover, the amount of details makes them more error-prone for humans. Computers, on the other hand, are very good at handling details and repetitiveness. In this work we have formalized textbook proofs of the meta-theory of sequent calculi for linear logic in Abella. Using the infrastructure developed, the proofs can be easily adapted to other substructural logics. We implemented rules as clauses in an intuitive and straightforward way, similar to logic programming, using operations on multisets for the explicit contexts. Although the proofs are quite big, they use only elementary reasoning principles, which makes the proof techniques fairly portable to other formal reasoning systems.

Details DOI

LPAR Conference 2015 Conference Paper

An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials

Kaustuv Chaudhuri
Giselle Reis

Abstract In linear logic, formulas can be split into two sets: classical (those that can be used as many times as necessary) or linear (those that are consumed and no longer available after being used). Subexponentials generalize this notion by allowing the formulas to be split into many sets, each of which can then be specified to be classical or linear. This flexibility increases its expressiveness: we already have adequate encodings of a number of other proof systems, and for computational models such as concurrent constraint programming, in linear logic with subexponentials ( The alternative text for this image may have been generated using AI. ). Bigraphs were proposed by Milner in 2001 as a model for ubiquitous computing, subsuming models of computation such as CCS and the \(\pi \) -calculus and capable of modeling connectivity and locality at the same time. In this work we present an encoding of the bigraph structure in The alternative text for this image may have been generated using AI. , thus giving an indication of the expressive power of this logic, and at the same time providing a framework for reasoning and operating on bigraphs. Our encoding is adequate and therefore the operations of composition and juxtaposition can be performed on the logical level. Moreover, all the proof-theoretical tools of The alternative text for this image may have been generated using AI. become available for querying and proving properties of bigraph structures.

Details

LFMTP Workshop 2014 Conference Paper

Automatically Deriving Schematic Theorems for Dynamic Contexts

Olivier Savary Bélanger
Kaustuv Chaudhuri

Hypothetical judgments go hand-in-hand with higher-order abstract syntax for meta-theoretic reasoning. The dynamic assumptions of these judgments often have a simple regular structure of repetitions of related assumptions; reflecting on this regular structure can let us derive a number of structural properties about the elements of the context automatically. We present an extension of the Abella theorem prover with a new mechanism for defining particular kinds of regular context relations, called schemas, and tacticals to derive theorems from these schemas as needed. Importantly, our extension leaves the trusted kernel of Abella unchanged. We show that these tacticals can eliminate many commonly encountered kinds of administrative lemmas that would otherwise have to be proven manually, which is a common source of complaints from Abella users.

Details

CSL Conference 2012 Conference Paper

A Systematic Approach to Canonicity in the Classical Sequent Calculus

Kaustuv Chaudhuri
Stefan Hetzl
Dale Miller 0001

The sequent calculus is often criticized for requiring proofs to contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps-such as instantiating a block of quantifiers-by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity: proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings, and atomic flows are examples of such revolutionary formalisms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means of abstracting away the details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that make the foci as parallel as possible are canonical. Moreover, such proofs are isomorphic to expansion proofs - a well known, minimalistic, and parallel generalization of Herbrand disjunctions - for classical first-order logic. This technique is a systematic way to recover the desired essence of any sequent proof without abandoning the sequent calculus.

Details

CSL Conference 2011 Conference Paper

The Focused Calculus of Structures

Kaustuv Chaudhuri
Nicolas Guenot
Lutz Straßburger

The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited both for the search and for the representation of sequent proofs. The calculus of structures is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but standard presentations of this calculus are too permissive, allowing too many proofs. In order to make it more amenable to proof search, we transplant the focusing theorem from the sequent calculus to the calculus of structures. The key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof.

Details

CSL Conference 2010 Conference Paper

Classical and Intuitionistic Subexponential Logics Are Equally Expressive

Kaustuv Chaudhuri

Abstract 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 other direction has no truth-preserving propositional encodings. We show here that subexponential logic, which is a family of substructural refinements of classical logic, each parametric over a preorder over the subexponential connectives, does not suffer from this asymmetry if the preorder is systematically modified as part of the encoding. Precisely, we show a bijection between synthetic (i. e. , focused) partial sequent derivations modulo a given encoding. Particular instances of our encoding for particular subexponential preorders give rise to both known and novel adequacy theorems for substructural logics.

Details

LPAR Conference 2008 Conference Paper

Focusing Strategies in the Sequent Calculus of Synthetic Connectives

Kaustuv Chaudhuri

Abstract It is well-known that focusing striates a sequent derivation into phases of like polarity where each phase can be seen as inferring a synthetic connective. We present a sequent calculus of synthetic connectives based on neutral proof patterns, which are a syntactic normal form for such connectives. Different focusing strategies arise from different polarisations and arrangements of synthetic inference rules, which are shown to be complete by synthetic rule permutations. A simple generic cut-elimination procedure for synthetic connectives respects both the ordinary focusing and the maximally multi-focusing strategies, answering the open question of cut-admissibility for maximally multi-focused proofs.

Details

CSL Conference 2005 Conference Paper

Focusing the Inverse Method for Linear Logic

Kaustuv Chaudhuri
Frank Pfenning

Abstract Focusing is traditionally seen as a means of reducing inessential non-determinism in backward-reasoning strategies such as uniform proof-search or tableaux systems. In this paper we construct a form of focused derivations for propositional linear logic that is appropriate for forward reasoning in the inverse method. We show that the focused inverse method conservatively generalizes the classical hyperresolution strategy for Horn-theories, and demonstrate through a practical implementation that the focused inverse method is considerably faster than the non-focused version.

Details