–
Room P3.10, Mathematics Building
Abstract algebraic logic approach to behavioral reasoning
We investigate the behavioral proof theory of a general class of equational specification logics, the hidden equational logics (HELs). We point out the strict relationship between Abstract Algebraic Logic and the study of the Behavioral Equivalence in HELs by generalizing some concepts and tools of Abstract Algebraic Logic to Specification Theory. Among other results we characterize the behaviorally valid conditional equations of a HEL as those conditional equations which, in a natural sense, do not increase the deductive power of the logic when they are added as new rules of inference. We also characterize the HELs whose behavior is specifiable by a (non-hidden) equational logic in terms of a special class of equivalential logics.