Birkhoff Completeness in Institutions

Mihai Codescu, Daniel Găină

In: Logica Universalis 2 2 Seiten 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