Ground expression
（重定向自Ground clause）
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 ![\forall](/Images/godic/202501/16/d4d49bead125261b226eaa867bd016ce5318.png")
x (x=x) is a ground formula.