Name
Abstract | ||
|---|---|---|
Because of the large number of strategies and inference rules presently under consideration in automated theorem proving, there is a need for developing a language especially oriented toward automated theorem proving. This paper discusses some of the features and instructions of this language. The use of this language permits easy extension of automated theorem-proving programs to include new strategies and/or new inference rules. Such extendability will permit general experimentation with the various alternative systems. |
Year | DOI | Venue |
|---|---|---|
1974 | 10.1145/355616.361017 | Commun. ACM |
Keywords | Field | DocType |
theorem proving,factoring,resolution,inference rule,programming language,automated theorem proving,programming languages | HOL,Programming language,Computer science,Automated theorem proving,Automated proof checking,Theoretical computer science,Object language,Rule of inference,Factoring | Journal |
Volume | Issue | ISSN |
17 | 6 | 0001-0782 |
Citations | PageRank | References |
0 | 0.34 | 4 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Lawrence J. Henschen | 1 | 478 | 280.94 |
| Ross A. Overbeek | 2 | 760 | 234.40 |
| Larry Wos | 3 | 450 | 92.39 |