The most popular are natural deduction, sequent calculi (i.e., Gentzen-type systems), Hilbert systems, and semantic tableaux or trees.
A proof procedure for a logic is complete if it produces a proof for each provable statement.
The theorems of logical systems are typically recursively enumerable, which implies the existence of a complete but usually extremely inefficient proof procedure; however, a proof procedure is only of interest if it is reasonably efficient.
Faced with an unprovable statement, a complete proof procedure may sometimes succeed in detecting and signalling its unprovability.
In the general case, where provability is only a semidecidable property, this is not possible, and instead the procedure will diverge (not terminate).