Title | ||
---|---|---|
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs |
Abstract | ||
---|---|---|
This paper presents the major design features of a new theorem-proving system currently being implemented. In it the authors describe the data structures of an existing program with which much experience has been obtained and discuss their significance for major theorem-proving algorithms such as subsumption, demodulation, resolution, and paramodulation. A new architecture for the large-scale design of theorem proving programs, which provides flexible tools for experimentation, is also presented. |
Year | DOI | Venue |
---|---|---|
1980 | 10.1007/3-540-10009-1_19 | CADE |
Keywords | Field | DocType |
theorem-proving programs,data structures,control architectures,theorem proving,data structure | Data architecture,Data structure,Demodulation,Architecture,Computer science,Automated theorem proving,Theoretical computer science | Conference |
ISBN | Citations | PageRank |
3-540-10009-1 | 10 | 3.32 |
References | Authors | |
5 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ross A. Overbeek | 1 | 760 | 234.40 |
Ewing L. Lusk | 2 | 3080 | 472.23 |