automated thoerem proving - natural deduction

[minhnhat93]

Hello, i have to make an automated thoerem prover using natural
deduction method and express the proof in a human-friendly style. i've
been searching google but most of the materials there are about
resolution method. Can anyone give me some books/hints/algorithm about
this please? Thanks.

example show how to display the proof:
http://nv2.upanh.com...67502.resol.png