This page describes the notion of a faithful mapping from a candidate language into the RIF condition language. The candidate languages considered here include FOL or rule bodies of various rule languages, such as query parts of production rules, reactive rules, and LP rules.
Dialects of RIF Condition Language and their models. We consider only the first-order dialect, the dialect where Naf is interpreted using the stable model/answer set semantics, and the dialect where Naf is interpreted using the well-founded semantics. An interpretation in the first case is any standard first order semantic structure. In the second case, interpretations are 2-valued Herbrand interpretations. In case of the well-founded semantics, an interpretation is a 3-valued Herbrand interpretation (as defined in the well-founded semantics theory), as described in A.6_Semantics. In the last two cases, it is useful to augment the domain with an infinite number of constants and function symbols of any arity.
A mapping from a candidate language to a dialect of RIF Condition Language generally has two components: a syntactic mapping at the level of languages and a mapping of the interpretations. The latter is typically an identity (when the candidate language and the dialect of the condition language use the same kinds of interpretations). When the interpretations are different---for instance, when mapping FOL into the dialect based on the well-founded semantics---then the mapping between interpretations may be non-trivial. Other situations when interpretations might have to be mapped arise when one of the languages uses non-standard model theory (e.g., HiLog or F-logic). We will write such mappings as (M,M'), where M maps formulas and M' maps interpretations.
Faithful mappings. A mapping (M,M') from a candidate language L to a dialect D of the RIF Condition Language is said to be faithful if the following condition holds:
For every formula φ in L, an interpretation I, and a variable assignment v, Iv(φ) = M'(I)v(M(φ)).