|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
Regular Derivations in Basic Superposition-Based Calculi
Aleksic, Vladimir and Degtyarev, Anatoli (2005) Regular Derivations in Basic Superposition-Based Calculi. In: Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005.
We prove the completeness of the regular strategy of derivations for superposition-based calculi. The regular strategy was pioneered by Kanger in [Kan63], who proposed that all equality inferences take place before all other steps in the proof. We show that the strategy is complete with the elimination of tautologies. The implication of our result is the completeness of non-standard selection functions by which in non-relational clauses only equality literals (and all of them) are selected.
Repository Staff Only: item control page