Proving semantical equivalence of data specifications (Q678825)

The paper deals with the problem of determining whether two given data specifications are equivalent. The equivalence is defined by the equivalence of the corresponding categories of finite models. The equivalence problem is undecidable because finite satisfiability in model theory can be reduced to it. There is a stronger concept of equivalence of data specifications which is given by the equivalence of the categories of all (also infinite) models. The authors reduce the strong equivalence problem (via sketches and their theories) to a deduction problem for essentially algebraic specification. Finally, they present a deduction system for these specifications which is claimed to be very suitable for an automated theorem prover. The paper seems to be an interesting application of category theory to computer science.