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 (8)

  1. First-order resolution
  2. Resolution
  3. Proof theory
  4. Mathematical logic
  5. Foundations of mathematics
  6. Area of mathematics
  7. Mathematics
  8. Home

Incoming links (2)

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