使用等式替换策略的广义归结

本文将Robinson及Wos1969年提出的等式替换策略应用于王湘浩及刘叙华1982年提出的广义归结中,使广义归结中处理等式更自然、简单,而且,广义归结中引入等式替换策略消除等式公理后,仍然是完备的。