What is the formalism behind ?- (query) in Prolog?

Question

I am in general interested in a more formal (better be logical, as in related to mathematical logic) definition of a query. As an example, there's Prolog operator ?- which takes as its argument a sentence in first order logic + meta-logical operators specific to Prolog and produces an "answer".

I'm interested to know what kind of logic deals with this (kind of) operator.

Answer 1

Prolog embodies the idea of computation as proof search. That is: a program is a formula which we would like to satisfy, the computation is the proof search, and the result is the witness for the formula.

To make this idea work we need to reformulate the rules of first-order logic so that they can be read as instructions for execution of a proof search. We may have to give up certain essentially non-computational parts of logic, such as excluded middle. We may further have to restrict the formulas that are allowed to appear, or else we will get something that looks like a general theorem prover insetad of a programming language.

I recommend chapter 8 of Frank Pfenning's notes on Computation and Deduction where these ideas are explained in detail.

Answer 2

Prolog deals with a formal system which is a small fragment of first order logic: it uses a logic of definite clauses, which are disjunctions of atoms and negated atoms, with the resolution rule as only inference rule.

If you're not completely familiar to formal (logic) systems you just need to know that they are basically sets of rules:

1. rules that describe how to build formulas from some basic symbols (the alphabeth)
2. rules that describe how to build proofs, i.e. sequences of formulas in which every element of the sequence is either an assumption, or an axiom of the logic system, or is obtained by previously derived formulas using inference rules (which can be thought as basic operations to compute new formulas from a set of initial formulas, the assumptions).

From this perspective formal systems are similar to primary school's arithmetic that is presented as

1. a set of rules to build well formed arithmetic expressions
2. a set of (equational) rules that describe how to reduce/rewrite/transform these expressions (the computational rules).

In this case the arithmetic expressions play the role of logic formulas, the rewrite rules correspond to inference rules and computations are simply sequences of arithmetic expressions obtained one from other through the application of the equations, so they correspond to proofs.

Of course as you have no eval operator in arithmetic you have no eval operator in formal logic, so ?- does no correspond to any logical symbol. The reason is that these operators are commands for an interpreter that have the effect to start execution. Logic systems are systems that represent knowledge (via formulas) and static descriptions of computations (the proofs), they are not abstract machine based model of computations.

Notheless you can model computations in formal logic: the reason for that is that you can regard every computation as a proof (for instance a computation of an arithmetic expression can be seen as a proof of an equality between the expression you want to compute and a value, the result of the computation), on the other end every proof is a computation obtained by some basic expressions (the axioms and the assumptions) applying the rules of inference, that are the basic operations of this model of computation.

Now back to prolog, prolog represent informations via Horn clauses, which are a special kind of definite clauses, these information are feed into the interpreter through a logic program, then the interpreter wait for a query, an instruction of the form ?- A_1,...,A_n. The effect of this query is to add the formula $\neg A_1 \lor \dots \lor \neg A_n$ as an assumption the clauses of the logic program and to start a search of a refutation of the goal of the query: using the program clauses and the clause and the clause of the query it infers new goal (clauses) until it can no longer apply the inference rule. While performing this proof-search the interpreter keeps track of variables'instantiation performed while applies resolution rule. When a computation/search stops there are two possible outcome:

1. the interpreter has reached the empty formula, instantiating the variables with a substitution $\sigma$, and so it can no longer infer anything else: in this case the interpreter has proven that from the Horn clauses of the program and the definite clause $\neg \sigma(A_1) \lor \dots \lor \neg \sigma(A_n)$ you can prove the absurd $\bot$, and so itin first order logic the clauses in the program entail the formula $\sigma(A_1) \land \dots \land \sigma(A_n)$;
2. the computation stop while having not reach the empty formula: in this case the interpreter can no longer continue because it has no other information to infer anything else, and so it means that the formula $\neg A_1 \lor \dots \lor \neg A_n$ can not be refutated and so it doesn't have enough informations to carry out the computation.

That's a quite long answer on how prolog works, anyway there's a lot more that could be said, but I prefer to refer to classical reference Lloyd's Foundation of logic programming to any additional information.

Hope this helps.