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. Overbeek1760234.40
Ewing L. Lusk23080472.23