Term Algebra Information
In universal algebra and mathematical logic, a term algebra or Herbrand universe is a freely generated algebraic structure. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X.
Term algebras play a role in the semantics of abstract data types, where an abstract data type declaration provides the signature of a multi-sorted algebraic structure and the term algebra is a concrete model of the abstract declaration.
The Herbrand base is analogous to the Herbrand universe, but consists of formulas. It is the set of all ground atoms.
Contents |
Decidability of term algebras
Term algebras can be shown decidable using quantifier elimination. The complexity of the decision problem is in NONELEMENTARY.[1]
Herbrand base
The Herbrand base of signature σ consists of all ground atoms of σ: of all formulas of the form R(t1, …, tn), where t1, …, tn are terms containing no variables (i.e. elements of the Herbrand universe) and R is an n-ary relation symbol. In the case of logic with equality, it also contains all equations of the form t1=t2, where t1 and t2 contain no variables.
See also
References
- ^ Jeanne Ferrante, Charles W. Rackoff: The computational complexity of logical theories, Springer (1979)
- Anatolii Ivanovic Mal'cev: "The Metamathematics of Algebraic Systems". North-Holland, 1971. (Studies in Logic and The Foundations of Mathematics, Volume 66)
- Weisstein, Eric W., "Herbrand Universe" from MathWorld.
External links
| This logic-related article is a stub. You can help Wikipedia by expanding it. · · |
Categories: Universal algebra | Mathematical logic |
|