In Automated Theorem Proving, what is the 'Herbrand Universe' H(S) of a set of First-Order Logic clauses S?
Jacques Herbrand defined the Herbrand universe as the set of all ground terms constructible purely from constants and function symbols present in the clause set S.
Why is the 'Occurs Check' an essential verification step during First-Order Logic unification?
The occurs check ensures a variable does not appear inside the term it is being bound to; omitting it allows unsound cyclic proofs like x = f(x).
How does Resolution Refutation prove that a knowledge base KB entails a query sentence alpha?
Resolution refutation is refutation-complete: if KB entails alpha, then KB ^ ~alpha is unsatisfiable, which resolution exposes by deriving the empty clause (contradiction).
In logic programming languages like Prolog, which inference strategy is used to resolve queries against Horn clause databases?
Prolog evaluates Horn clauses using SLD resolution, working backward from query subgoals via depth-first search and backtracking.
What fundamental monotonicity property holds in classical deductive logic but fails in Non-Monotonic Logic?
Monotonicity means adding information never shrinks the set of entailed conclusions: if KB |= alpha, then (KB ^ beta) |= alpha. Non-monotonic logic (e.g. default logic) allows retracting conclusions when new evidence arrives.