Logics of First-Order Constraints -- A Category Independent Approach

TL;DR

This paper introduces a category-independent framework for Logics of First-Order Constraints (LFOC), unifying various logic systems through the concept of institutions and first-order sketches, enhancing expressiveness with sketch rules.

Contribution

It presents a novel, general approach to LFOC using institutions, allowing flexible parameter choices and the integration of sketch rules for increased expressive power.

Findings

Unified framework for various first-order logics

Characterization of constraints as first-order sketches

Introduction of sketch rules for enhanced expressiveness

Abstract

Reflecting our experiences in areas, like Algebraic Specifications, Abstract Model Theory, Graph Transformations, and Model Driven Software Engineering (MDSE), we present a general, category independent approach to Logics of First-Order Constraints (LFOC). Traditional First-Order Logic, Description Logic and the sketch framework are discussed as examples. We use the concept of institution [Diaconescu08,GoguenBurstall92] as a guideline to describe LFOC's. The main result states that any choice of the six parameters, we are going to describe, gives us a corresponding "institution of constraints" at hand. The "presentations" for an institution of constraints can be characterized as "first-order sketches". As a corresponding variant of the "sketch-entailments" in [Makkai97], we finally introduce "sketch rules" to equip LFOC's with the necessary expressive power.