35 results on '"Chaudhuri, Kaustuv"'
Search Results
2. Subformula Linking for Intuitionistic Logic with Application to Type Theory
- Author
-
Chaudhuri, Kaustuv, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Platzer, André, editor, and Sutcliffe, Geoff, editor
- Published
- 2021
- Full Text
- View/download PDF
3. A Hybrid Linear Logic for Constrained Transition Systems
- Author
-
Despeyroux, Joelle and Chaudhuri, Kaustuv
- Subjects
Computer Science - Logic in Computer Science - Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus., Comment: LIPIcs. TYPES'2013, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014. arXiv admin note: substantial text overlap with arXiv:1310.4310
- Published
- 2016
4. Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice
- Author
-
Cervesato, Iliano and Chaudhuri, Kaustuv
- Subjects
Computer Science - Logic in Computer Science ,Computer Science - Programming Languages - Abstract
This volume constitutes the proceedings of LFMTP 2015, the Tenth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, held on August 1st, 2015 in Berlin, Germany. The workshop was a one-day satellite event of CADE-25, the 25th International Conference on Automated Deduction. Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades. This workshop brought together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
- Published
- 2015
- Full Text
- View/download PDF
5. Undecidability of Multiplicative Subexponential Logic
- Author
-
Chaudhuri, Kaustuv
- Subjects
Computer Science - Logic in Computer Science ,F.4.2 - Abstract
Subexponential logic is a variant of linear logic with a family of exponential connectives--called subexponentials--that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that classical propositional multiplicative linear logic extended with one unrestricted and two incomparable linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable., Comment: In Proceedings LINEARITY 2014, arXiv:1502.04419
- Published
- 2015
- Full Text
- View/download PDF
6. A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology
- Author
-
Chaudhuri, Kaustuv and Despeyroux, Joelle
- Subjects
Computer Science - Logic in Computer Science - Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus. We also present some preliminary experiments of direct encoding of biological systems in the logic.
- Published
- 2013
7. Reasoning About Higher-Order Relational Specifications
- Author
-
Wang, Yuting, Chaudhuri, Kaustuv, Gacek, Andrew, and Nadathur, Gopalan
- Subjects
Computer Science - Logic in Computer Science - Abstract
The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dynamically changing sets of assumptions and that is key to encoding side conditions and contexts that occur frequently in structural operational semantics (SOS) style presentations. Specifications are often useful in reasoning about the systems they describe. The Abella theorem prover supports such reasoning by explicitly embedding the specification logic within a rich reasoning logic; specifications are then reasoned about through this embedding. However, realizing an induction principle in the face of dynamically changing assumption sets is nontrivial and the original Abella system uses only a subset of the HH specification logic for this reason. We develop a method here for supporting inductive reasoning over all of HH. Our approach takes advantage of a focusing property of HH to isolate the use of an assumption and the ability to finitely characterize the structure of any such assumption in the reasoning logic. We demonstrate the effectiveness of these ideas via several specification and meta-theoretic reasoning examples that have been implemented in an extended version of Abella., Comment: Principles and Practice of Declarative Programming (2013)
- Published
- 2013
- Full Text
- View/download PDF
8. Verifying Safety Properties With the TLA+ Proof System
- Author
-
Chaudhuri, Kaustuv, Doligez, Damien, Lamport, Leslie, and Merz, Stephan
- Subjects
Computer Science - Logic in Computer Science - Abstract
TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties.
- Published
- 2010
- Full Text
- View/download PDF
9. Classical and Intuitionistic Subexponential Logics are Equally Expressive
- Author
-
Chaudhuri, Kaustuv
- Subjects
Computer Science - Logic in Computer Science - 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., Comment: 15 pages, to appear in 19th EACSL Annual Conference on Computer Science Logic (CSL 2010)
- Published
- 2010
10. A TLA+ Proof System
- Author
-
Chaudhuri, Kaustuv C., Doligez, Damien, Lamport, Leslie, and Merz, Stephan
- Subjects
Computer Science - Logic in Computer Science - Abstract
We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Different provers can be used to verify different obligations. The currently supported back-ends are the tableau prover Zenon and Isabelle/TLA+, an axiomatisation of TLA+ in Isabelle/Pure. The proof obligations for a complete TLA+ proof can also be used to certify the theorem in Isabelle/TLA+.
- Published
- 2008
11. Distributing and trusting proof checking: a preliminary report
- Author
-
Al Wardani, Farah, Chaudhuri, Kaustuv, Miller, Dale, Miller, Dale, Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
- Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] - Abstract
When a proof-checking kernel completes the checking of a formal proof, that kernel asserts that a specific formula follows from a collection of lemmas within a given logic. We describe a framework in which such an assertion can be made globally so that any other proof assistant willing to trust that kernel can use that assertion without rechecking (or even understanding) the formal proof associated with that assertion. In this framework, we propose to move beyond autarkic proof checkers-i.e., self-sufficient provers that trust proofs only when they are checked by their kernel-to an explicitly non-autarkic setting. This framework must, of course, explicitly track which agents (proof checkers and their operators) are being trusted when a trusting proof checker makes its assertions. We describe how we have integrated this framework into a particular theorem prover while making minor changes to how the prover inputs and outputs text files. This framework has been implemented using off-the-shelf web-based technologies, such as JSON, IPFS, IPLD, and public key cryptography.
- Published
- 2022
12. A Logical Characterization of Forward and Backward Chaining in the Inverse Method
- Author
-
Chaudhuri, Kaustuv, Pfenning, Frank, and Price, Greg
- Published
- 2008
- Full Text
- View/download PDF
13. Formalized meta-theory of sequent calculi for linear logics
- Author
-
Chaudhuri, Kaustuv, primary, Lima, Leonardo, additional, and Reis, Giselle, additional
- Published
- 2019
- Full Text
- View/download PDF
14. Formalized Meta-Theory of Sequent Calculi for Substructural Logics
- Author
-
Chaudhuri, Kaustuv, primary, Lima, Leonardo, additional, and Reis, Giselle, additional
- Published
- 2017
- Full Text
- View/download PDF
15. A Two-Level Logic Approach to Reasoning about Typed Specification Languages
- Author
-
Southern, Mary, Chaudhuri, Kaustuv, Department of Computer Science and Engineering, University of Minnesota [Twin Cities] (UMN), University of Minnesota System-University of Minnesota System, Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Venkatesh Raman and S. P. Suresh, European Project: 291592,EC:FP7:ERC,ERC-2011-ADG_20110209,PROOFCERT(2012), and Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France
- Subjects
000 Computer science, knowledge, general works ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory ,Computer Science ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,16. Peace & justice - Abstract
International audience; The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.
- Published
- 2014
16. Modular Focused Proof Systems for Intuitionistic Modal Logics
- Author
-
Chaudhuri, Kaustuv, Marin, Sonia, Chaudhuri, Kaustuv, and Marin, Sonia
- Abstract
Focusing is a general technique for syntactically compartmentalizing the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing is usually specified as a restriction of the sequent calculus, the technique has not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some of the logics of the modal cube. We have recently extended the focusing technique to classical nested sequents, a generalization of ordinary sequents. In this work we further extend focusing to intuitionistic nested sequents, which can capture all the logics of the intuitionistic S5 cube in a modular fashion. We present an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.
- Published
- 2016
- Full Text
- View/download PDF
17. Modular Focused Proof Systems for Intuitionistic Modal Logics
- Author
-
Kaustuv Chaudhuri and Sonia Marin and Lutz Straßburger, Chaudhuri, Kaustuv, Marin, Sonia, Straßburger, Lutz, Kaustuv Chaudhuri and Sonia Marin and Lutz Straßburger, Chaudhuri, Kaustuv, Marin, Sonia, and Straßburger, Lutz
- Abstract
Focusing is a general technique for syntactically compartmentalizing the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing is usually specified as a restriction of the sequent calculus, the technique has not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some of the logics of the modal cube. We have recently extended the focusing technique to classical nested sequents, a generalization of ordinary sequents. In this work we further extend focusing to intuitionistic nested sequents, which can capture all the logics of the intuitionistic S5 cube in a modular fashion. We present an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.
- Published
- 2016
- Full Text
- View/download PDF
18. A Hybrid Linear Logic for Constrained Transition Systems
- Author
-
Despeyroux, Joelle, Chaudhuri, Kaustuv, Usage-centered design, analysis and improvement of information systems (AxIS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria), Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), LIPIcs, and Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France
- Subjects
FOS: Computer and information sciences ,adequacy ,focusing ,ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES ,Computer Science - Logic in Computer Science ,000 Computer science, knowledge, general works ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,ACM: G.: Mathematics of Computing ,Logic in Computer Science (cs.LO) ,ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.2: Modes of Computation/F.1.2.3: Parallelism and concurrency ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,linear logic ,Computer Science::Logic in Computer Science ,Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,hybrid logic ,stochastic pi-calculus - Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus., Comment: LIPIcs. TYPES'2013, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014. arXiv admin note: substantial text overlap with arXiv:1310.4310
- Published
- 2014
- Full Text
- View/download PDF
19. A Proof-theoretic Characterization of Independence in Type Theory
- Author
-
Wang, Yuting, Chaudhuri, Kaustuv, Wang, Yuting, and Chaudhuri, Kaustuv
- Published
- 2015
- Full Text
- View/download PDF
20. A Proof-theoretic Characterization of Independence in Type Theory
- Author
-
Yuting Wang and Kaustuv Chaudhuri, Wang, Yuting, Chaudhuri, Kaustuv, Yuting Wang and Kaustuv Chaudhuri, Wang, Yuting, and Chaudhuri, Kaustuv
- Abstract
For lambda-terms constructed freely from a type signature in a type theory such as LF, there is a simple inductive subordination relation that is used to control type-formation. There is a related—but not precisely complementary—notion of independence that asserts that the inhabitants of the function space tau_1 --> tau_2 depend vacuously on their arguments. Independence has many practical reasoning applications in logical frameworks, such as pruning variable dependencies or transporting theorems and proofs between type signatures. However, independence is usually not given a formal interpretation. Instead, it is generally implemented in an ad hoc and uncertified fashion. We propose a formal definition of independence and give a proof-theoretic characterization of it by: (1) representing the inference rules of a given type theory and a closed type signature as a theory of intuitionistic predicate logic, (2) showing that typing derivations in this signature are adequately represented by a focused sequent calculus for this logic, and (3) defining independence in terms of strengthening for intuitionistic sequents. This scheme is then formalized in a meta-logic, called G, that can represent the sequent calculus as an inductive definition, so the relevant strengthening lemmas can be given explicit inductive proofs. We present an algorithm for automatically deriving the strengthening lemmas and their proofs in G.
- Published
- 2015
- Full Text
- View/download PDF
21. Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice
- Author
-
Cervesato, Iliano, primary and Chaudhuri, Kaustuv, additional
- Published
- 2015
- Full Text
- View/download PDF
22. Undecidability of Multiplicative Subexponential Logic
- Author
-
Chaudhuri, Kaustuv, primary
- Published
- 2015
- Full Text
- View/download PDF
23. Abella: A System for Reasoning about Relational Specifications
- Author
-
Baelde, David; LSV, CNRS & ENS de Cachan, Chaudhuri, Kaustuv; INRIA, France., Gacek, Andrew; Rockwell Collins, USA, Miller, Dale; Inria & LIX/Ecole polytechnique, France, Nadathur, Gopalan; University of Minnesota, USA, Tiu, Alwen; Nanyang Technological University, Singapore, Wang, Yuting; University of Minnesota, Baelde, David; LSV, CNRS & ENS de Cachan, Chaudhuri, Kaustuv; INRIA, France., Gacek, Andrew; Rockwell Collins, USA, Miller, Dale; Inria & LIX/Ecole polytechnique, France, Nadathur, Gopalan; University of Minnesota, USA, Tiu, Alwen; Nanyang Technological University, Singapore, and Wang, Yuting; University of Minnesota
- Abstract
The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the λ-tree approach to treating syntax containing binders: it allows simply typed λ-terms to be used to represent such syntax and it provides higher-order (pattern) unification, the nabla quantifier, and nominal constants for reasoning about these representations. As such, it is a suitable vehicle for formalizing the meta-theory of formal systems such as logics and programming languages. This tutorial exposes Abella incrementally, starting with its capabilities at a first-order logic level and gradually presenting more sophisticated features, ending with the support it offers to the two-level logic approach to meta-theoretic reasoning. Along the way, we show how Abella can be used prove theorems involving natural numbers, lists, and automata, as well as involving typed and untyped λ-calculi and the π-calculus.
- Published
- 2014
24. A Hybrid Linear Logic for Constrained Transition Systems
- Author
-
Chaudhuri, Kaustuv and Chaudhuri, Kaustuv
- Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus.
- Published
- 2014
- Full Text
- View/download PDF
25. A Hybrid Linear Logic for Constrained Transition Systems
- Author
-
Joëlle Despeyroux and Kaustuv Chaudhuri, Despeyroux, Joëlle, Chaudhuri, Kaustuv, Joëlle Despeyroux and Kaustuv Chaudhuri, Despeyroux, Joëlle, and Chaudhuri, Kaustuv
- Abstract
Linear implication can represent state transitions, but real transition systems operate under temporal, stochastic or probabilistic constraints that are not directly representable in ordinary linear logic. We propose a general modal extension of intuitionistic linear logic where logical truth is indexed by constraints and hybrid connectives combine constraint reasoning with logical reasoning. The logic has a focused cut-free sequent calculus that can be used to internalize the rules of particular constrained transition systems; we illustrate this with an adequate encoding of the synchronous stochastic pi-calculus.
- Published
- 2014
- Full Text
- View/download PDF
26. A Two-Level Logic Approach to Reasoning About Typed Specification Languages
- Author
-
Mary Southern and Kaustuv Chaudhuri, Southern, Mary, Chaudhuri, Kaustuv, Mary Southern and Kaustuv Chaudhuri, Southern, Mary, and Chaudhuri, Kaustuv
- Abstract
The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.
- Published
- 2014
- Full Text
- View/download PDF
27. A Systematic Approach to Canonicity in the Classical Sequent Calculus
- Author
-
Chaudhuri, Kaustuv, Hetzl, Stefan, Miller, Dale, Chaudhuri, Kaustuv, Hetzl, Stefan, and Miller, Dale
- Abstract
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.
- Published
- 2012
- Full Text
- View/download PDF
28. A Systematic Approach to Canonicity in the Classical Sequent Calculus
- Author
-
Kaustuv Chaudhuri and Stefan Hetzl and Dale Miller, Chaudhuri, Kaustuv, Hetzl, Stefan, Miller, Dale, Kaustuv Chaudhuri and Stefan Hetzl and Dale Miller, Chaudhuri, Kaustuv, Hetzl, Stefan, and Miller, Dale
- Abstract
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.
- Published
- 2012
- Full Text
- View/download PDF
29. The Focused Calculus of Structures
- Author
-
Chaudhuri, Kaustuv, Guenot, Nicolas, Chaudhuri, Kaustuv, and Guenot, Nicolas
- Abstract
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.
- Published
- 2011
- Full Text
- View/download PDF
30. The Focused Calculus of Structures
- Author
-
Kaustuv Chaudhuri and Nicolas Guenot and Lutz Straßburger, Chaudhuri, Kaustuv, Guenot, Nicolas, Straßburger, Lutz, Kaustuv Chaudhuri and Nicolas Guenot and Lutz Straßburger, Chaudhuri, Kaustuv, Guenot, Nicolas, and Straßburger, Lutz
- Abstract
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.
- Published
- 2011
- Full Text
- View/download PDF
31. The Focused Inverse Method for Linear Logic
- Author
-
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE, Chaudhuri, Kaustuv, CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE, and Chaudhuri, Kaustuv
- Abstract
Linear logic presents a unified framework for describing and reasoning about stateful systems. Because of its view of hypotheses as resources, it supports such phenomena as concurrency, external and internal choice, and state transitions that are common in such domains as protocol verification, concurrent computation, process calculi and games. It accomplishes this unifying view by providing logical connectives whose behavior is closely tied to the precise collection of resources. The interaction of the rules for multiplicative, additive and exponential connectives gives rise to a wide and expressive array of behaviors. This expressivity comes with a price: even simple fragments of the logic are highly complex or undecidable. Various approaches have been taken to produce automated reasoning systems for fragments of linear logic. This thesis addresses the need for automated reasoning for the complete set of connectives for first-order intuitionistic linear logic (circle multiply, 1,-o, &, Top, circle plus, 0, !, Universal quantifier, Existential quantifier), which removes the need for any idiomatic constructions in smaller fragments and instead allows direct logical expression. The particular theorem proving technique used is a novel combination of a variant of Maslov's inverse method using Andreoli's focused derivations in the sequent calculus as the underlying framework. The goal of this thesis is to establish the focused inverse method as the premier means of automated reasoning in linear logic. To this end, the technical claims are substantiated with an implementation of a competitive first-order theorem prover for linear logic as of this writing, the only one of its kind.
- Published
- 2006
32. Abella: A System for Reasoning about Relational Specifications.
- Author
-
BAELDE, DAVID, GACEK, ANDREW, NADATHUR, GOPALAN, YUTING WANG, CHAUDHURI, KAUSTUV, MILLER, DALE, and ALWEN TIU
- Subjects
REASONING ,MATHEMATICS theorems ,SYNTAX (Grammar) ,UNIFICATION grammar ,METATHEORY - Abstract
The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the λ-tree approach to treating syntax containing binders: it allows simply typed λ-terms to be used to represent such syntax and it provides higher-order (pattern) unification, the ∇ quantier, and nominal constants for reasoning about these representations. As such, it is a suitable vehicle for formalizing the meta-theory of formal systems such as logics and programming languages. This tutorial exposes Abella incrementally, starting with its capabilities at a first-order logic level and gradually presenting more sophisticated features, ending with the support it o ers to the two-level logic approach to meta- theoretic reasoning. Along the way, we show how Abella can be used prove theorems involving natural numbers, lists, and automata, as well as involving typed and untyped λ-calculi and the π-calculus. [ABSTRACT FROM AUTHOR]
- Published
- 2014
33. A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
- Author
-
PARSIFAL (INRIA Saclay - Ile de France) ; CNRS - INRIA - Polytechnique - X, Indiana University, Xavier Leroy and Alwen Tiu, European Project : 291592, ERC, ERC-2011-ADG_20110209, PROOFCERT(2012), Chaudhuri, Kaustuv, Cimini, Matteo, Miller, Dale, PARSIFAL (INRIA Saclay - Ile de France) ; CNRS - INRIA - Polytechnique - X, Indiana University, Xavier Leroy and Alwen Tiu, European Project : 291592, ERC, ERC-2011-ADG_20110209, PROOFCERT(2012), Chaudhuri, Kaustuv, Cimini, Matteo, and Miller, Dale
- Abstract
International audience, Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the under-lying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the π-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports λ-tree syntax and generic reasoning using the ∇-quantifier, our treatment of the π-calculus is both direct and natural.
34. Proof-Relevant π-Calculus
- Author
-
Perera, Roly, Cheney, James, Cervesato, Iliano, and Chaudhuri, Kaustuv
- Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS - Abstract
Formalising the π-calculus is an illuminating test of the expressiveness of logical frameworks and\ud mechanised metatheory systems, because of the presence of name binding, labelled transitions with\ud name extrusion, bisimulation, and structural congruence. Formalisations have been undertaken in\ud a variety of systems, primarily focusing on well-studied (and challenging) properties such as the\ud theory of process bisimulation. We present a formalisation in Agda that instead explores the theory\ud of concurrent transitions, residuation, and causal equivalence of traces, which has not previously\ud been formalised for the π-calculus. Our formalisation employs de Bruijn indices and dependentlytyped\ud syntax, and aligns the “proved transitions” proposed by Boudol and Castellani in the context\ud of CCS with the proof terms naturally present in Agda’s representation of the labelled transition\ud relation. Our main contributions are proofs of the “diamond lemma” for residuation of concurrent\ud transitions and a formal definition of equivalence of traces up to permutation of transitions.
- Published
- 2015
35. A Multi-Focused Proof System Isomorphic to Expansion Proofs
- Author
-
Stefan Hetzl, Kaustuv Chaudhuri, Dale Miller, Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), European Project: 291592,EC:FP7:ERC,ERC-2011-ADG_20110209,PROOFCERT(2012), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Chaudhuri, Kaustuv, and ProofCert: Broad Spectrum Proof Certificates - PROOFCERT - - EC:FP7:ERC2012-01-01 - 2016-12-31 - 291592 - VALID
- Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ,Logic ,Cut-elimination theorem ,ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory ,0102 computer and information sciences ,01 natural sciences ,Theoretical Computer Science ,Arts and Humanities (miscellaneous) ,Proof calculus ,Computer Science::Logic in Computer Science ,Calculus ,Structural proof theory ,Sequent ,0101 mathematics ,Mathematics ,Geometry of interaction ,Discrete mathematics ,Natural deduction ,Proof complexity ,010102 general mathematics ,Noncommutative logic ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Hardware and Architecture ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Software - Abstract
International audience; 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 for abstracting away low-level details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that collect together all possible parallel foci are canonical. Moreover, if we start with a certain focused sequent proof system, such proofs are isomorphic to expansion proofs---a well known, minimalistic, and parallel generalization of Herbrand disjunctions---for classical first-order logic. This technique appears to be a systematic way to recover the "essence of proof" from within sequent calculus proofs.
- Published
- 2014
Catalog
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.