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.
Original language | English (US) |
---|---|
Pages (from-to) | 308-314 |
Number of pages | 7 |
Journal | Communications of the ACM |
Volume | 17 |
Issue number | 6 |
DOIs | |
State | Published - Jun 1 1974 |
Keywords
- factoring
- paramodulation
- programming languages
- resolution
- theorem proving
ASJC Scopus subject areas
- General Computer Science