Does it only exist in statically typed languages? And is it only there when the language is not strongly typed (i.e. does Java have one)? Also, where does it belong - in the compilation phase assuming it's a compiled language?
In general, are the rules when the type is ambiguous dictated by the language specification or left up to the implementation?
A type inferencer determines what type a variable is from the context. It relies on strong typing to do so. For example, functional languages are very strongly, statically typed but completely rely on type inference.
C# and VB.Net are other examples of statically typed languages with type inference (they provide it to make generics usable, and it is required for queries in LINQ, specifically to support projections).
Dynamic languages do not infer type, it is discovered at runtime.
Type inferencing is a bit of a compromise found in some static languages. You can declare variables without specifying the type, provided that the type can be inferred at compile time. It doesn't offer the flexibility of latent typing, but you do get type safety and you don't have to write as much.
Type inference is a feature of some statically-typed languages. It is done by the compiler to assign types to entities that otherwise lack any type annotations. The compiler effectively just 'fills in' the static type information on behalf of the programmer.
Type inference tends to work more poorly in languages with many implicit coercions and ambiguities, so most type inferenced languages are functional languages with little in the way of coercions, overloading, etc.
Type inference is part of the language specification, for the example the F# spec goes into great detail about the type inference algorithm and rules, as this effectively determines 'what is a legal program'.
Though some (most?) languages support some limited forms of type inference (e.g. 'var' in C#), for the most part people use 'type inference' to refer to languages where the vast majority of types are inferred rather than explicit (e.g. in F#, function and method signatures, in addition to local variables, are typically inferred; contrast to C# where 'var' allows inference of local variables but method declarations require full type information).
A type inferencer is anything which deduces types statically, using a type inference algorithm. As such, it is not just a feature of static languages.
You may build a static analysis tool for dynamic languages, or those with unsafe or implicit type conversions, and type inference will be a major part of its job. However, type inference for languages with unsafe or dynamic type systems, or which include implicit conversions, can not be used to prove the type safety of a program in the general case.
As such type inference is used: