natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A Horn theory is a theory in which every axiom has a certain special form.
Let be a signature. A term of is an expression built out of variables and function symbols. (For example, is a term in the language of groups.) An atomic formula relative to is a formula that consists of a relation symbol of (including equality) applied to terms.
A Horn clause is a logical expression of the form
where each and is atomic. A (universal) Horn theory is a theory in which every axiom is a Horn clause.
Last revised on February 23, 2024 at 19:53:19. See the history of this page for a list of all contributions to it.