We study the connection between narrowing and a method for proof by consistency due to Bachmair, and we show that narrowing and proof by consistency may be used to simulate each other. This allows for the migration of results between the two process descriptions. We obtain decidability results for validity of equations in the initial algebra from existing results on narrowing. Furthermore we show that several results on completeness of position selection strategies for narrowing are special cases of a generalization of a result on covering sets presented by Bachmair.
CITATION STYLE
Lysne, O. (1994). On the connection between narrowing and proof by consistency. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 814 LNAI, pp. 133–147). Springer Verlag. https://doi.org/10.1007/3-540-58156-1_10
Mendeley helps you to discover research relevant for your work.