Many-Sorted Hybrid Modal Languages

TL;DR

This paper explores a hybrid multi-sorted modal logic system that enhances expressivity for programming language semantics, offers a sound and complete fragment, and translates into first-order logic, balancing power and computational efficiency.

Contribution

It introduces a new fragment of hybrid multi-sorted logic with proven soundness and completeness, capable of representing programs and semantics uniformly, and provides a translation to first-order logic.

Findings

Identified a powerful yet computationally manageable logic fragment.

Proved soundness and completeness for the fragment.

Established a translation to first-order logic.

Abstract

We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of the full logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an uniform way. Although weaker than other hybrid systems previously developed, this system is expected to have better computational properties. Finally, we provide a standard translation from full hybrid many-sorted logic to first-order logic.