Axiomatizability of representable domain algebras

The family of domain algebras provide an elegant formal system for automated reasoning about programme verification. Their primary models are algebras of relations, viz. representable domain algebras. We prove that, even for the minimal signature consisting of the domain and composition operations, the class of representable domain algebras is not finitely axiomatizable. Then we show similar results for extended similarity types of domain algebras.

• Type: Journal
• Year: 2011
• Where: JLP
• Authors: Robin Hirsch, Szabolcs Mikulás
• Keywords: Automated Reasoning, Domain Algebras, JLP 2011, Representable Domain Algebras