2
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ I do not know what you are trying to ask. ?- is just a syntactic element in Prolog signifying queries, and I do not know in which sense you think that it is an operator in logic. $\endgroup$ – Tsuyoshi Ito Jan 9 '15 at 5:28
  • $\begingroup$ @TsuyoshiIto well, it's not just a syntactic element (as in "decoration"), because what happens after you use it can't be (or can it be?) described by means of other syntactic elements of the language. I was thinking it must be something similar to eval or, maybe ||= (in a sense that model ||= statement means "model proves statement", where printing of the ways variables in the statement may be grounded is a side effect (or not?)). $\endgroup$ – wvxvw Jan 9 '15 at 6:56
  • $\begingroup$ I know that ?- is not a syntax sugar, and I never claimed it was. If you just want to know the definition of ?- in Prolog, check the language specification or some books which explain the language in detail, and it is not appropriate on cstheory.stackexchange.com. I am not sure if this is the case, but I cannot tell what else you are trying to ask. $\endgroup$ – Tsuyoshi Ito Jan 9 '15 at 8:20
  • $\begingroup$ @TsuyoshiIto I recently finished reading The Art of Prolog, and I know what ?- does (in the sense that I know what it is used for). What I do not know is why it does what it does. If you allow me this analogy: regular expressions, when embedded in other languages have their "own" language plus the ability to match, replace, some times split etc. The meaning of matching or replacing isn't part of regular expression language, but it also has some theoretical basis. So, I was wondering if querying (not necessary in Prolog) has such basis too. $\endgroup$ – wvxvw Jan 9 '15 at 9:13
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I will need to read the linked material, but before that: I have no argument against what you say, but I think that my question was more specific than asking in general what Prolog does. I'm only interested in what querying does. If you will, think, of it this way: you have a language, which has no querying mechanism, say, Java; what do you need to do to add querying to Java? I don't think it's limited to logic programming, databases are a good candidate too. $\endgroup$ – wvxvw Jan 11 '15 at 7:11
  • $\begingroup$ Ah, sorry about that. A query is a goal that Prolog tries to solve. It is the equivalent of a program to be executed in Java, or a query in SQL. If you want queries in Java you'll have to implement something: a database, a search engine. There are languages which combine proof search with other aspects of computation, for instance $\lambda$-prolog. $\endgroup$ – Andrej Bauer Jan 11 '15 at 8:46
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.