Paper Info
Title
A new hyperparamodulation strategy for the equality relation
Abstract
Equality is an Important relation and many theorems can be easily symbolized through it's use. A proposed Inference rule called HL-resolution is intended to have the benefits of hyper steps while controlling the application of paramodulation. It generates a resolvent by building a paramodulation and demodulation link between two terms using a pre proceased plan as a guide. The rule is complete for E-unsatisfiable Horn sets. The linking process makes use of an equality graph which is constructed once at the beginning of the run. Once a pair of candidate terms for HL-resolutlon is chosen in the search, potential linkages can be found and tested for compatibility efficiently by looking at the paths in the graph. The method was implemented on an existing theorem-proving system. A number of experiments were conducted on problems in abstract algebra and a comparison with set-of-support paramodulation was made.
Year
Venue
Keywords
1985
IJCAI
equality graph,equality relation,e-unsatisfiable horn,proposed inference rule,new hyperparamodulation strategy,hyper step,existing theorem-proving system,demodulation link,set-of-support paramodulation,candidate term,abstract algebra,important relation,inference rule
Field
DocType
ISBN
Graph,Discrete mathematics,Demodulation,Linkage (mechanical),Compatibility (mechanics),Resolvent,Computer science,Abstract algebra,Artificial intelligence,Rule of inference,Machine learning
Conference
0-934613-02-8
Citations 
PageRank 
References 
6
0.56
7
Authors
2
Name
Order
Citations
PageRank
YoungHwan Lim1218.84
Lawrence J. Henschen2478280.94