Birkhoff Completeness in Institutions

Mihai Codescu; Daniel Găină

In: Logica Universalis, Vol. 2, No. 2, Pages 277-309, Birkhäuser Basel, 2008.


We develop an abstract proof calculus for logics whose sentences are "Horn sentences" of the form: $$(\forall X)H \Rightarrow c$$ and prove an institutional generalization of Birkhoff completeness theorem. This result is then applied to the particular cases of Horn clauses logic, the "Horn fragment" of preorder algebras, order-sorted algebras and partial algebras and their infinitary variants.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence