2 papers
cs.LO2003
Ground Canonicity
Nachum Dershowitz
We explore how different proof orderings induce different notions of saturation. We relate completion, paramodulation, saturation, redundancy elimination, and rewrite system reduct…
cs.PL2000
Automatic Termination Analysis of Programs Containing Arithmetic Predicates
Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv +1
For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the…