Electronic Resource
Springer
International journal of parallel programming
3 (1974), S. 105-122
ISSN:
1573-7640
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract In this paper a system termed the Maryland refutation proof procedure system (MRPPS) is described. MRPPS is an interactive system which gives the user the ability to create and maintain a core-bound data base and to input queries either as well-formed formulas in the first-order predicate calculus or as clauses. MRPPS consists of three basic components: (1) a set of inference rules for making logical deductions, many of which are based on the resolution principle; (2) a search strategy for heuristically determining the sequence in which to select base clauses and to perform deductions on clauses already generated; and (3) a base clause selection strategy that uses heuristic and semantic information for determining which data axioms and general axioms are to be brought to bear on the problem. These three components are described and MRPPS is compared to related work.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00976637
Permalink
|
Location |
Call Number |
Expected |
Availability |