Title: Shu li luo ji yin lun yu gui jie yuan li
Subjects: Automatic theorem proving, Symbolic and mathematical Logic