[PhD position 2021] Semantics, Proofs and Refutations in Resource Logics.

Keywords: semantics, proof theory, proof transformations, refutations, resource logics.

Contact

Didier GALMICHE (galmiche@loria.fr)

Daniel MERY (dmery@loria.fr)

Summary

In this PhD, we focus on extensions and variants of BI, the logic of Bunched Implications, which is a combination of intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BBI, the Boolean variant of BI, is the logical kernel upon which spatial and separation logics are built.
We shall:
– study proof transformations between labelled and label-free calculi for the resource logics of the BI family,
– propose new resource semantics,
– devise effective algorithms for solving reachability constraints in resource graphs,
– define new refutation systems.

Scientific Context

Modern computer systems have become highly complex and involve a multitude of interactions between a wide variety of heterogeous components that can be viewed as resources. As such systems gain more control on many aspects of human life (e.g., airline traffic, banking and social networks), it also becomes more important to ensure their correctness, either a priori by design, or a posteriori by verification.

The notion of resource is a basic one in many fields, including economics, engineering and psychology, but it is perhaps most clearly illuminated in computer science. Resources can be physical (like a printer or CPU) or abstract (like a program or a mathematical function), they can be static (like a token in a Petri net) or dynamic (i.e., evolving by themselves like a process or a thread).

Addressing the problems raised by the resources and their management in a well defined formal settings is the goal of resource logics and their associated resource semantics. For instance, linear logics deal with aspects related to resource production and consumption, while separation logics deal with aspects related to resource sharing and separation.
Modal and ambiant logics are well suited for problems involving temporal and spatial distributions of resources and their mobility.

Subject and Goals

In this PhD, we focus on extensions and variants of BI, the logic of Bunched Implications [9], which is a combination of intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BBI, the Boolean variant of BI [4], is the logical kernel upon which spatial and separation logics are built.

There exist various calculi for BI. The most remarkable ones are the purely syntactic bunched sequent calculus LBI [9] and the labelled tableau/sequent calculi TBI/GBI [3,6]. The translation from LBI proofs to TBI/GBI proofs is well known. Surprisingly, the translation of TBI/GBI proofs to LBI proofs is far from trivial and is currently still an open problem, although there have been recent advances for a small subclass of single-conclusioned GBI proofs (sGBI proofs) satisfying a very specific tree property [6].

A first goal of this PhD is to extend the previous results to multi-conclusioned GBI proofs (mGBI proofs) and study whether any arbitrary mGBI proofs can be normalized to a mGBI proofs satisfying the tree-property.

Even in the more basic case of IL, translating labelled proofs to label-free sequent proofs remains a non-trivial problem requiring an intermediate translation to bi-intuitionistic logic (BiInt) [8]. Bi-intuitionistic logic [1] is an extension of IL in which a new connective called co-implication is added. BiInt can be viewed as a combination of IL, which favors the notion of constructive verification (i.e., provability), with dual intuitionistic logic (DualInt), which favors the notion of constructive falsification (i.e., refutability). The proof/refutation duality has been successfully captured in Lorenzen dialog games where one player tries to prove a formula while the other tries to disprove it [2].

A second goal of this PhD is to devise a bi-intuitionistic extension of BI and determine whether such an extension could serve as an intermediate step for more general translations of GBI proofs to LBI proofs.

In our works on labelled calculi for BI [3] and BiInt [8] we have emphasized the importance of structures, called resource graphs, that capture the validity of a formula as reachability constraints between labels. Resource graphs are used both as a way to guide the proof search process and as a way to extract counter-models [3] in case of non-provability. Counter-model construction is central in our approach since it is essential in everydays practice to quickly understand why a specification fails when it fails. Currently, we only have effective constraint solving algorithms for BiInt resource graphs [5], where labels are atomic and may contain free variables, and for BI resource graphs, where labels are strings of letters without free variables.

A third goal of this PhD is to devise and implement effective constraint solving algorithms for more general classes of resource graphs built from non-atomic labels that might contain free variables.

A counter-model is a semantic object witnessing the non-validity of a formula in a given semantics, whereas a refutation is a syntactic object witnessing the non-provability of a formula in a given proof system. For instance, CRIP is a refutation system for IL [7]. In absence of a completeness theorem, refutations and counter-models do not necessarily coincide. Moreover, a counter-model might be difficult to construct and even more difficult to interpret (which greatly reduces its practical usefulness) when the underlying semantics is too abstract or too elaborated (like, for instance, the Grothendieck topological semantics of BI). In such a situation, building a refutation instead of a counter-model seems preferable. Currently, there exists no refutation system for resource logics built upon the BI logical kernel.

A fourth goal of this PhD is therefore to investigate the question and propose refutation systems for the family of resource logics based on BI.

References

[1] T. Crolard. Subtractive logic. In Theoretical Computer Science, 254(1-2):151–185, 2001.

[2] W. Felscher. Dialogues, strategies, and intuitionistic provability. In Annals of Pure and Applied Logic, 28(3):217–254, 1985.

[3] D. Galmiche, D. Méry, and D. Pym. The semantics of BI and Resource Tableaux. Mathematical Structures in Computer Science, 15(6):1033–1088, 2005.

[4] D. Galmiche and D. Larchey-Wendling. Expressivity properties of Boolean BI through relational models. In Int. Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2006, LNCS 4337, pages 357–368, Kolkata, India, 2006.

[5] D. Galmiche and D. Méry. A connection-based characterization of bi-intuitionistic validity. In Int. Conference on Automated Deduction, CADE 23, LNCS 6803, pages 268–282, Wroclaw, Poland, 2011.

[6] D. Galmiche, M. Marti and D. Méry.
Relating labelled and label-free bunched calculi in BI logic. In 28th Int. Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, LNCS 11714, pages 130–146, London, United Kingdom, 2019.

[7] L. Pinto and R. Dyckhoff. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana, Conference A, pages 226–232, 1995.

[8] L. Pinto and T. Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In 3rd Workshop on Classical Logic and Compution, CL&C 2010, EPTCS 47, pages 57–72, Brno, Czech Republic, 2010.

[9] D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series. Kluwer Academic Publishers, 2002.

Hosting team

The PhD position is proposed by the TYPES of LORIA research lab.

Skills and profile

  • Required qualification: Master in Computer Science (or equivalent)
  • Knowledge in the following fields will be appreciated: logic, proof theory, semantics, programming (C, CAML, Java, Python)

Additional information

Duration: 3 years

Starting date: between Oct. 1st 2021 and Dec. 1st 2021

How to apply

Send the following documents to galmiche@loria.fr and dmery@loria.fr

  • a CV
  • a motivation letter
  • your degree certificates and transcripts for Bachelor and Master (or equivalent)

Logo d'Inria