Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Ground expression
Résumé
In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables.
In first-order logic with identity with constant symbols and , the sentence is a ground formula. A ground expression is a ground term or ground formula.
Consider the following expressions in first order logic over a signature containing the constant symbols and for the numbers 0 and 1, respectively, a unary function symbol for the successor function and a binary function symbol for addition.
are ground terms;
are ground terms;
are ground terms;
and are terms, but not ground terms;
and are ground formulae.
What follows is a formal definition for first-order languages. Let a first-order language be given, with the set of constant symbols, the set of functional operators, and the set of predicate symbols.
A is a term that contains no variables. Ground terms may be defined by logical recursion (formula-recursion):
Elements of are ground terms;
If is an -ary function symbol and are ground terms, then is a ground term.
Every ground term can be given by a finite application of the above two rules (there are no other ground terms; in particular, predicates cannot be ground terms).
Roughly speaking, the Herbrand universe is the set of all ground terms.
A , or is an atomic formula all of whose argument terms are ground terms.
If is an -ary predicate symbol and are ground terms, then is a ground predicate or ground atom.
Roughly speaking, the Herbrand base is the set of all ground atoms, while a Herbrand interpretation assigns a truth value to each ground atom in the base.
A or is a formula without variables.
Ground formulas may be defined by syntactic recursion as follows:
A ground atom is a ground formula.
If and are ground formulas, then , , and are ground formulas.
Ground formulas are a particular kind of closed formulas.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.