arXiv subjects

Didier Galmiche

Publications and source records attributed to Didier Galmiche.

4 recordsLinked to original sources

arXiv2025

Bifurcation Logic: Separation Through Ordering

We introduce Bifurcation Logic, BL, which combines a basic classical modality with separating conjunction * together with its naturally associated multiplicative implication, that is defined using the modal ordering. Specifically, a formula A*B is true at a world w if and only if each of A,B holds at worlds that are each above w, on separate branches of the order, and have no common upper bound. We provide a labelled tableaux calculus for BL and establish soundness and completeness relative to its relational semantics. The standard finite model property fails for BL. However, we show that, in the absence of multiplicative implication, but in the presence of *, every model has an equivalent finite representation and that this is sufficient to obtain decidability. We illustrate the use of BL through an example of modelling multi-agent access control that is quite generic in its form, suggesting many applications.

cs.LO↗

arXiv2024

Minimalistic System Modelling: Behaviours, Interfaces, and Local Reasoning

The infrastructure upon which the functioning of society depends is composed of complex ecosystems of systems. Consequently, we must reason about the properties of such ecosystems, which requires that we construct models of them. There are very many approaches to systems modelling, typically building on complex structural and dynamic frameworks. Our purpose here is to explore a modelling framework based on minimal assumptions, starting from a primitive notion of behaviour, and to show that such an approach allows the recovery of the key ideas, including a generalized CAP theorem, required for effective modelling of and reasoning about ecosystems of systems. We establish a logic of behaviours and use it to express local reasoning principles for the compositional structure of systems.

cs.LO↗

arXiv2023

Internal and External Calculi: Ordering the Jungle without Being Lost in Translations

This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively straightforward while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi.' We discuss the ambiguities involved in the informal definitions of these categories, and we critically assess the properties that (calculi from) these classes are purported to possess.

cs.LO↗

arXiv2019

A Substructural Epistemic Resource Logic: Theory and Modelling Applications

We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI's resource semantics --- we introduce BI and its resource semantics at some length --- with epistemic agency. We illustrate the use of the logic in systems modelling by discussing some examples about access control, including semaphores, using resource tokens. We also give a labelled tableaux calculus and establish soundness and completeness with respect to the resource semantics.

cs.LO↗