一句话：研究带普通复合与 demonic 格运算的关系半群，揭示其表示类的有限公理化与可判定性边界。
关系代数及其归约（reducts）可用来推理非确定性程序的部分正确性；demonic calculus 通过将非确定性视为恶魔控制，把此类推理扩展到全正确性。本文用带普通复合（ordinary composition）和 demonic 格运算的半群，形式化非确定性程序全正确性的关系推理框架。作者研究若干表示类：证明可表示 demonic 并半群类不可有限公理化；demonic 交半群表示类对其有限成员不具备有限表示性质。对于同时含复合、demonic 并与 demonic 交的格半群，证明有限代数的表示问题不可判定，有限表示问题亦不可判定，从而推出表示类不可有限公理化且有限表示性质失败。
Relation algebra and its reducts provide us with a strong tool for reasoning about nondeterministic programs and their partial correctness. Demonic calculus, introduced to model the behaviour of a machine where the demon is in control of nondeterminism, has also provided us with an extension of that reasoning to total correctness. We formalise the framework for relational reasoning about total correctness in nondeterministic programs using semigroups with ordinary composition and demonic lattice operations. We show that the class of representable demonic join semigroups is not finitely axiomatisable and that the representation class of demonic meet semigroups does not have the finite representation property for its finite members. For lattice semigroups (with composition, demonic join and demonic meet) we show that the representation problem for finite algebras is undecidable, moreover the finite representation problem is also undecidable. It follows that the representation class is not finitely axiomatisable, furthermore the finite representation property fails.