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:
- rules that describe how to build formulas from some basic symbols (the alphabeth)
- 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
- a set of rules to build well formed arithmetic expressions
- 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:
- 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)$;
- 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.