Why can a positive-looking query correspond to a negative clause?

The refutation procedure adds the negation of the proposition it aims to prove.

Does one failed branch mean the goal is unprovable?

No. Other clauses or substitutions may succeed, and an incomplete search may not explore them.

AI Glossary / Graphs and symbolic AI / Intermediate

Goal clauses

Definition

Goal clauses are clauses with no positive literals, used in Horn-clause logic and resolution-based reasoning to represent goals to be proved by refutation. A typical goal clause is not P or not Q, often written procedurally as an instruction to establish P and Q. Its negative logical form and its positive-looking query notation describe two views of the same proof task.

What it means

A clause is a disjunction of literals, where a literal is an atomic statement or its negation. A Horn clause has at most one positive literal. A definite clause has exactly one; a goal clause has none.
The terminology can initially sound backwards. To prove P and Q from a program, a refutation approach adds the negation of that conjunction. By De Morgan's law, the added clause is not P or not Q. Deriving a contradiction shows that the program cannot coexist with denial of the requested conjunction. Operationally, the remaining positive atoms are treated as subgoals to establish.

How it works

In SLD-style reasoning, select an atom from the current goal and match it, through unification, with the head of a definite program clause. Replace that selected subgoal with the clause's body, applying the substitution consistently to the other subgoals. A fact has an empty body and can discharge a matching subgoal.
The process continues until no subgoals remain, producing a successful empty-goal state, or a branch cannot proceed. Other rule choices can be explored by backtracking. The logical calculus and the program's search strategy are distinct: an unfortunate depth-first ordering may loop even when a proof exists elsewhere.

Three practical examples

A logic-programming exercise asks whether a named item is both available and compatible using facts and definite rules.
A theorem-proving demonstration negates a desired conjunction and traces resolution steps to the empty clause.
A symbolic query includes variables and returns substitutions that make all of its subgoals provable together.

Think of it this way

Think of a checklist whose items can be replaced by smaller supporting tasks until the list is empty. This captures operational subgoal reduction. The analogy is limited because a goal clause has a precise negative logical interpretation, and substitutions must remain consistent across all items rather than treating each checklist entry as an unrelated request.

Worked example

Use the fictional facts Available(book7) and Catalogued(book7), plus the rule Available(x) and Catalogued(x) imply Ready(x). Ask whether Ready(book7) follows.
The refutation starts with the goal clause not Ready(book7). Resolve it with the rule, represented as not Available(x) or not Catalogued(x) or Ready(x), using substitution x = book7. The new goal clause is not Available(book7) or not Catalogued(book7).
Resolving with Available(book7) leaves not Catalogued(book7). Resolving that with Catalogued(book7) yields the empty clause. Thus the attempted denial is inconsistent with the facts and rule, establishing Ready(book7).
In procedural notation, the same trace replaces the goal Ready(book7) with the two subgoals Available(book7) and Catalogued(book7), then discharges both. If the cataloged fact were absent, this particular proof would not complete; that absence alone would not be a classical proof of not Catalogued(book7).

Illustrative case study

In a fictional tutoring session, the Fir team writes a query requiring an item to be tagged and checked. It initially solves the two conditions with different item identifiers and treats that as success for a shared variable.
The tutor demonstrates that the substitution chosen for the first subgoal must also apply to the second. The team corrects the trace and shows only answers for which the same item satisfies both conditions. This invented case illustrates variable consistency in goal reduction, without claiming that a specific language implementation automatically avoids every modeling mistake.

Common misconceptions and mistakes

A goal clause is not any sentence containing the everyday word “goal.” It is a syntactic category in a specified logic. It also differs from a definite clause, which contains a positive head.
Do not interpret the negative literals as a request to make all the corresponding positive atoms false. In refutation, their disjunction denies the conjunction being proved. Do not confuse the empty clause, which denotes contradiction, with an ordinary true fact. Finally, failure or nontermination of one procedural search is not automatically a complete logical answer to the original query.

Business use

The term is useful for understanding explanations from rule-based systems and logic programs. A trace of changing goal clauses can show which facts and rules support an answer and which unresolved subgoal blocks a proof.
For application design, keep the query, rule base, and control strategy distinguishable. Document variable bindings and whether an unsuccessful query means finite failure, timeout, or unavailable information. This prevents an operational outcome from being presented as a stronger statement about real-world truth than the reasoning process established.

Check your understanding

What clause represents the denial of P and Q in propositional refutation?

Answer: Not P or not Q. It is a goal clause because both literals are negative. It is not the same as not P and not Q, which would deny both statements separately.

Related terms

Learn next

Learn next about SLD resolution. Add a second rule for Ready(x) to the worked example and draw the alternative proof branches. Track the substitution for x through each branch, distinguishing an unsuccessful branch from a completed search over all alternatives.

Resolution

Sources

Lawrence C. Paulson, original Logic and Proof notes, first-order resolution and Prolog: https://www.cl.cam.ac.uk/teaching/1112/LogicProof/logic-notes.pdf SWI-Prolog official glossary, clauses and resolution terminology: https://www.swi-prolog.org/pldoc/man?section=glossary

Previous: Goal Next: Goal-directed reasoning