If, for instance, I type help(bagof). into the Prolog REPL, a window pops up with some documentation, the first line of which reads bagof(+Template, :Goal, -Bag).
Are the arguments Template, Goal and Bag just names, or are they formal types that can be systematically researched? (In the first case I would have to rely on the documentation of bagof to make sense of them; in the latter case I would be able to refer to some other document.)
Where can I find documentation for those bits of punctuation preceding the arguments? (In this case the punctuation includes the symbols +, : and -, but I've seen others.)
Template, Goal etc. are simply names of these arguments. Sometimes, they give some indication about the expected type of the respective argument. For example, Goal typically indicates an argument of type callable. A name like List typically indicates a list, and so on.
+, : etc. are mode indicators and denote the expected instantiation patterns:
Quoting from http://eu.swi-prolog.org/pldoc/man?section=modes:
++ Argument is ground at call-time, i.e., the argument does not contain a variable anywhere. + Argument is fully instantiated at call-time, to a term that satisfies the type. etc. - Argument is an output argument. etc. -- Argument is unbound at call-time. etc. ? Argument is bound to a partial term of the indicated type at call-time. etc. : Argument is a meta-argument. Implies +. etc.
The most commonly used mode indicators are +, - and ?.
Note also that there are different conventions and slight variations for documenting such properties of predicates that are also used in the literature and in the documentation of some systems.