4.5 基于归结的自动程序综合

　　此内容不作课内要求，作为扩展内容自学。