TY - JOUR AU - Hintermeier, Claus AU - Kirchner, Hélene AU - Mosses, Peter D. PY - 1996/06/21 Y2 - 2024/03/28 TI - Rn and Gn Logics JF - BRICS Report Series JA - BRICS VL - 3 IS - 51 SE - Articles DO - 10.7146/brics.v3i51.20054 UR - https://tidsskrift.dk/brics/article/view/20054 SP - AB - This paper proposes a simple, set-theoretic framework providing<br />expressive typing, higher-order functions and initial models at<br />the same time. Building upon Russell's ramified theory of types, we develop<br />the theory of Rn-logics, which are axiomatisable by an order-sorted<br />equational Horn logic with a membership predicate, and of Gn-logics,<br />that provide in addition partial functions. The latter are therefore more<br />adapted to the use in the program specification domain, while sharing<br /> interesting properties, like existence of an initial model, with Rn-logics.<br /> Operational semantics of Rn-/Gn-logics presentations is obtained through<br />order-sorted conditional rewriting. ER -