The linked inference principle. I: The formal treatment (Q1189727)

The article presents the formal treatment of the linked inference principle. This principle permits to obtain formulations of various linked inference rules. A linked inference rule is a type of reasoning that combines a number of smaller steps into a single larger one. The linked inference rule is a way of reasoning that gives the user control over various parameters, such as the size of the reasoning steps, the breath of the search that the program is allowed to make and the semantic nature of the conclusion. The use of linked inference rules permits a more natural representation of problems. The objective of linked inference rules is to select a set \(S\) of clause inferences and find and apply a unifier in such a way that literals are paired, unified and cancelled. Clauses from \(S\) can be partitioned into disjoint sets: the nucleus, the satellites and the links (if the set of links is empty we obtain a standard inference rule). Linking clauses share properties with both the nucleus and the satellites. A number of linked inference rules are presented: linked \(UR\)-resolution, linked hyperresolution, linked binary resolution, each of which generalizes the corresponding and well-known standard inference rule. Experimental results and numerous examples are presented.