Difference between statically and dynamically typed languages
The question is subtle and simple at the same time, hence deep. Let me give you
a simplifying answer.

First you need to realise there there three somewhat orthogonal distinctions which are often mixed up, leading to confusion:


Typed vs untyped languages  
Type-checking vs type-inference 
Static vs dynamic typing


Types are simply an algorithmic technique to define and decide
language subsets (think: if a program is typable, it's in the
subset). Typically subset decided by types are somehow well-behaved, and we consider programs not in the subset to be somehow bad
or in error, think programs like "hello" * 17 are rejected).
The essence of this algorithmic technique is that you have a second language (that of types) which gives a second version on the program in question. Typically the language of types is  simpler than the ambient programming language.

Type-checking vs type-inference is about a detail of this algorithmic technique: in
type-checking a program is compared against user-specified types: are
the two in 'harmony', while in type-inference the internal consistency
of a program with itself is checked. In practise no programming
language is fully type-checked, instead at least some parts of programs are
 inferred, e.g. you don't have  to write

((3 : int) (+ : (int, int) -&gt; int) (4 : int)) : int


or some monstrosity like this, instead,
you can get away with

3 + 4


even in Java. 

Finally statically vs dynamically typed is about when programs are
accepted or rejected.  With dynamic typing that happens during
execution. With static typing, there is a distinct phase (sometime called semantic analysis) before
execution, typically during compilation. If the program fails semantic analysis, compilation or interpretation is abandoned, hence no execution.