Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
Screen decoration graphicsLogo

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.

[img]PDF - Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


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.

Item Type:Conference or Workshop Item (Paper)
ID Code:840
Deposited By:Dr Anatoli Degtyarev
Deposited On:04 Nov 2007 13:16
Last Modified:04 Nov 2007 13:17

Repository Staff Only: item control page