词条 | Ground expression |
释义 |
In mathematical logic, a ground term of a formal system is a term that does not contain any free variables. Similarly, a ground formula is a formula that does not contain any free variables. In first-order logic with identity, the sentence {{all}} x (x=x) is a ground formula. A ground expression is a ground term or ground formula. ExamplesConsider the following expressions from first order logic over a signature containing a constant symbol 0 for the number 0, a unary function symbol s for the successor function and a binary function symbol + for addition.
Formal definitionWhat 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 (individual) variables, the set of functional operators, and the set of predicate symbols. Ground termsGround terms are terms that contain no variables. They may be defined by logical recursion (formula-recursion):
Roughly speaking, the Herbrand universe is the set of all ground terms. Ground atomA ground predicate or ground atom or ground literal is an atomic formula all of whose argument terms are ground terms. If p∈P is an n-ary predicate symbol and α1, α2, ..., αn are ground terms, then p(α1, α2, ..., αn) 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. Ground formulaA ground formula or ground clause is a formula without free variables. Formulas with free variables may be defined by syntactic recursion as follows:
References
| title = Handbook of discrete and combinatorial mathematics | contribution = Logic-based computer programming paradigms | year = 2000 | editor1-last = Rosen | editor1-first = K.H. | editor2-last = Michaels | editor2-first = J.G. | last = Dalal | first = M. | page = 68 }}
2 : Mathematical logic|Logical expressions |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。