The PCS proof method (BB 2000) aims at generating "natural" proofs.
Roughly, the PCS prover proceeds by iteratively going through the following three phases:
The P-phase ("Proving" phase)
The C-phase ("Computing" phase)
The S-phase ("Solving" phase)
It reduces proving of formulae with "alternating quantifiers" to solving.