Ordered Semantic Hyper Linking

In this paper, we present a novel first order theorem proving strategy - ordered semantic hyper linking. Ordered semantic hyper linking (OSHL) is an instance-based refutational theorem proving strategy. It is sound and complete. OSHL has an efficient propositional decision procedure. It solves first order problems by reducing them to propositional problems. It uses natural semantics of an input problem to guide its search. It also incorporates term rewriting to handle equality. The propositional efficiency, semantic guidance and equality support allow OSHL to solve problems that are difficult for many other strategies. The efficiency of OSHL is supported by experimental study as well as complexity analysis.

Authors

• David A. Plaisted Yunshan Zhu

Keywords

No keywords are indexed for this paper.