A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.

Revisiting McKinsey's 'Syntactical' Construction of Modality

In 1945 J.C.C. McKinsey produced a ‘semantics’ for modal logic based on necessity defined in terms of validity. The present papers looks at how to update F.R. Drake’s completeness proof for McKinsey’s semantics by comparing McKinsey ‘models’ with the now standard Kripke models. It also looks at the motivation behind the system McKinsey called S4.1, but which we now call S4M; and use this motivation to produce a McKinsey semantics for that system. One lesson which emerges from this work is an appreciation of the superiority of the current possible worlds semantics based on frames and models, both in terms of an intuitive understanding of modality, and also in terms of the ease of working with particular systems.

FIRST-ORDER POSSIBILITY MODELS AND FINITARY COMPLETENESS PROOFS

This article builds on Humberstone’s idea of defining models of propositional modal logic where total possible worlds are replaced by partial possibilities. We follow a suggestion of Humberstone by introducing possibility models for quantified modal logic. We show that a simple quantified modal logic is sound and complete for our semantics. Although Holliday showed that for many propositional modal logics, it is possible to give a completeness proof using a canonical model construction where every possibility consists of finitely many formulas, we show that this is impossible to do in the first-order case. However, one can still construct a canonical model where every possibility consists of a computable set of formulas and thus still of finitely much information.

Proof theory for quantified monotone modal logics

This paper provides a proof-theoretic study of quantified non-normal modal logics (NNML). It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames. In particular, the completeness proof constructs a formal derivation for derivable sequents and a countermodel for non-derivable ones, and gives a semantic proof of the admissibility of cut.

A 2-approximation algorithm for the contig-based genomic scaffold filling problem

The genomic scaffold filling problem has attracted a lot of attention recently. The problem is on filling an incomplete sequence (scaffold) [Formula: see text] into [Formula: see text], with respect to a complete reference genome [Formula: see text], such that the number of common/shared adjacencies between [Formula: see text] and [Formula: see text] is maximized. The problem is NP-complete, and admits a constant-factor approximation. However, the sequence input [Formula: see text] is not quite practical and does not fit most of the real datasets (where a scaffold is more often given as a list of contigs). In this paper, we revisit the genomic scaffold filling problem by considering this important case when a scaffold [Formula: see text] is given, the missing genes can only be inserted in between the contigs, and the objective is to maximize the number of common adjacencies between [Formula: see text] and the filled genome [Formula: see text]. For this problem, we present a simple NP-completeness proof, we then present a factor-2 approximation algorithm.

Mechanizing proofs with logical relations – Kripke-style

Proofs with logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe two case studies using the proof environmentBeluga: First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs inBelugarelies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage ofBeluga's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploitBeluga's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate thatBelugaprovides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments.