English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This document provides a formal proof of Birkhoff's completeness theorem formulti-sorted algebras which states that any equational entailment valid in allmodels is also provable in the equational theory.  More precisely, if a certain equation is valid in all models that validate afixed set of equations, then this equation is derivable from that set using theproof rules for a congruence.  The proof has been formalized in Agda version 2.6.2 with the Agda StandardLibrary version 1.7 and this document reproduces the commented Agda code.

Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda