Decidability and structure
For a class of structures and let resp. denote the lattices of -congruences resp. -congruences of , cf. Weaver [25]. Let where is the operator of forming isomorphic copies, and . For an ordered algebra the lattice of order congruences of is denoted by , and let if is a class of ordered algebras. The operators of forming subdirect squares and direct products are denoted by and , respectively. Let be a lattice identity and let be a set of lattice identities. Let denote...
We present a formal scheme which whenever satisfied by relations of a given relational lattice containing only reflexive and transitive relations ensures distributivity of .