Logics of First-Order Constraints -- A Category Independent Approach
This work provides a foundational framework for unifying various first-order constraint logics, which is significant for researchers and practitioners working with formal methods and model-driven engineering.
The paper introduces a general, category-independent approach to Logics of First-Order Constraints (LFOC), drawing from experiences in Algebraic Specifications, Abstract Model Theory, Graph Transformations, and Model Driven Software Engineering. The key finding is that any selection of six specified parameters yields a corresponding "institution of constraints," where presentations can be characterized as "first-order sketches."
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.