First Experiments with Rue Automated Deduction

Vincent J. Digricoli

RUE resolution represents a reformulation of binary resolution so that the basic rules of inference (RUE and NRF) incorporate the axioms of equality. A RUE theorem prover has been implemented and experimental results indicate that this method represents a significant advance in the handling of equality in resolution.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.