Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Term (logic)
Summary
In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact.
A first-order term is recursively constructed from constant symbols, variables and function symbols.
An expression formed by applying a predicate symbol to an appropriate number of terms is called an atomic formula, which evaluates to true or false in bivalent logics, given an interpretation.
For example, (x+1)*(x+1) is a term built from the constant 1, the variable x, and the binary function symbols + and ; it is part of the atomic formula (x+1)(x+1) \ge 0 which evaluates to true for each real-numbered value of x.
Besides in logic, terms play important roles in universal algebra, and rewriting systems.
Given a set V of variable symbols, a set C of constant symbols and sets Fn of n-ary function symbols, also called operator symbols, for each natural number n ≥ 1, the set of (unsorted first-order) terms T is recursively defined to be the smallest set with the following properties:
every variable symbol is a term: V ⊆ T,
every constant symbol is a term: C ⊆ T,
from every n terms t1,...,tn, and every n-ary function symbol f ∈ Fn, a larger term f(t1, ..., tn) can be built.
Using an intuitive, pseudo-grammatical notation, this is sometimes written as:
t ::= x | c | f(t1, ..., tn).
The signature of the term language describes which function symbol sets Fn are inhabited. Well-known examples are the unary function symbols sin, cos ∈ F1, and the binary function symbols +, −, ⋅, / ∈ F2. Ternary operations and higher-arity functions are possible but uncommon in practice. Many authors consider constant symbols as 0-ary function symbols F0, thus needing no special syntactic class for them.
A term denotes a mathematical object from the domain of discourse. A constant c denotes a named object from that domain, a variable x ranges over the objects in that domain, and an n-ary function f maps n-tuples of objects to objects.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.