Collection

Tag: boyer-moore

ACL2 and the Industrialization of Automated Theorem Proving

ACL2 turned the Boyer-Moore tradition of automated inductive theorem proving into an executable Common Lisp-based logic that could model and verify commercial hardware and software systems.

↗

Robert Boyer and J Strother Moore: Searching Text by Skipping Ahead

Robert Boyer and J Strother Moore reversed the usual direction of pattern comparison, using mismatches near the end of a pattern to skip large sections of text during exact search.

↗