Horn equational theories and paramodulation (Q1824409)

Robinson's pioneering work on mechanizing mathematical logic quite immediately raised the problem ``How can equality axioms be incorporated into resolution machinery ?'' At the same time much effort has been spent on looking for efficient refutationally complete strategies for decidable subclasses of first-order logic. It was then the Prolog language together with Horn clause logic, input and unit resolution were invented giving rise to Logic programming paradigm. A direct proof for the completeness of paramodulation for Horn equality logic (the language of equational logic programs) is presented. The declarative and fixpoint semantics of this language are then investigated, for the operational semantics the inference rules paramodulation and reflection are proven to be sound and complete w.r.t. the fixpoint semantics. It is well-known that automatic theorem provers based on paramodulation are far from being efficient, since they have to explore a search space containing many irrelevant derivations, since paramodulation can be applied both from left to right and from right to left. The commonly used techniques for Logic programming restricting the search space are discussed and demonstrated. Among them are directed paramodulation, conditional term rewriting systems and narrowing. The paper gives a clear and precise vision of the problems, progress and success achieved in the field of equational Logic programming.