A rule that combines first-order clauses by unifying complementary first-order literals and retaining the other literals under the resulting first-order substitution. Completeness requires the appropriate calculus and search conditions.
A family of resolution calculi for first-order Horn clauses. A selection function chooses either the positive head atom alone or a nonempty set of body atoms. Permitted inferences respect those choices; fair saturation is refutationally complete. Function symbols need not be excluded, so completeness does not by itself guarantee termination. [ref]

Ancestors (7)

  1. Resolution
  2. Proof theory
  3. Mathematical logic
  4. Foundations of mathematics
  5. Area of mathematics
  6. Mathematics
  7. Home

Incoming links (1)

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version