Why does an implication whose conclusion is false mean a query?

Question

In first order predicate logic, or logical programming, a query is a Horn clause without positive term, or an implication whose conclusion is false. For example, in Prolog, query ?- rainy(rochester) means false ← rainy(rochester).

What does an implication whose conclusion is false mean? Such an implication is true if and only if its assumption is false. How can it mean a query?

For example,

In most implementations of Prolog, queries are entered with a special ?- version of the implication symbol. If we were to type the following Queries

rainy(seattle).
rainy(rochester).
?- rainy(C).

the Prolog interpreter would respond with

C = seattle

Of course, C = rochester would also be a valid answer, but Prolog will find seattle first, because it comes first in the database.

How do implication false ← rainy(C) and query ?- rainy(C) mean the same?

Thanks.

Answer 1

Horn clauses are used in authomated theorem proving with the Resolution proof procedure:

Like in resolution theorem proving, intuitive meanings "show $φ$" and "assume $¬φ$" are synonymous (indirect proof); they both correspond to the same formula, viz. $¬φ$.

The proof procedure assume the negation of the formula $φ$ "to be showed" and find that the negated formula $¬φ$ is unsatisfiable.

If the procedure succeed, this means thatthe original formula $φ$ is a tautology.

Using the falsum constant $\bot$, we have that $φ \to \bot$ is equivalent to $¬φ$.

In conclusion, using "$\text {false} \leftarrow φ$" as goal cluase is equivalento to "show $φ$", i.e. to prove $φ$.

---

Goals and queries are not the same (but they are treated similarly in logical programming).

See Prolog : goals and queries : "A goal is a statement starting with a predicate and probably followed by its arguments. A goal is a statement starting with a predicate and probably followed by its arguments. This is similar to proving a hypothesis - the goal being the hypothesis, the facts being the axioms and the rules being the theorems."

"A query is a statement starting with a predicate and followed by its arguments, some of which are variables. The purpose of submitting a query is to find values to substitute into the variables in the query such that the query is satisfied. This is similar to asking a question, asking for "what values will make my statement true.""

If we express the goal : $\text ? \leftarrow \text {rainy}(c)$ as : $\bot \leftarrow \text {rainy}(c)$, i.e. as $\lnot \text {rainy}(c)$, using Unification we preform the substitution : $\lnot \text {rainy}(c)[c \leftarrow \text {seattle}]$ to get :

$\lnot \text {rainy}(\text {seattle})$

and we can conclude applying the Resolution rule with premise : $\text {rainy}(\text {seattle})$.

This means that the substitution : $c \leftarrow \text {seattle}$ will resolve the query with the set of premises, i.e. that the said substitution will give us the result of the query : "$\text ? \leftarrow \text {rainy}(c)$", which means : "is there a value for $c$ such that $\text {rainy}(c)$ holds ?"