Selected references Peter B. Andrews. Theorem proving via general mappings. Journal of the ACM, 28(2):193-214, April 1981. Wolfgang Bibel. On matrices with connections. Journal of the ACM, 28(4):633-645, October 1981.