Paper Info
Title
Boyer-Moore Automation for the HOL System
Abstract
Boyer and Moore's heuristics for their first-order logic without quantifiers have been re-implemented in the HOL system. They have been adapted to behave as an automatic prover for the subset of higher-order logic that roughly corresponds to the Boyer-Moore logic. This paper describes the modifications required and presents some initial results and conclusions from the exercise.
Year
DOI
Venue
1992
10.1016/B978-0-444-89880-7.50015-2
TPHOLs
Keywords
Field
DocType
boyer-moore automation,hol system
HOL,Programming language,Computer science,Algorithm,Automation,Theoretical computer science,Heuristics,Gas meter prover,Boyer–Moore string search algorithm
Conference
Volume
ISSN
ISBN
20
0926-5473
0-444-89880-8
Citations 
PageRank 
References 
5
0.53
2
Authors
1
Name
Order
Citations
PageRank
Richard J. Boulton125523.64