What is the formalism behind ?- (query) in Prolog? 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.
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.