"Subsumption has long been known as a technique to detect redundant clauses in the search space of automated deduction systems for classical first order logic. In recent years several automated deduction methods for non-classical modal logics have been developed. This thesis explores, how subsumption can be made to work in the context of these modal logic deduction methods.
Many modern modal logic deduction methods follow an indirect approach. They translate the modal sentences into some other target language, and then determine whether there exists a proof in that language, rather than doing deduction in the modal language itself. Consequently, subsumption then needs to focus on the target language, in which the actual proof is done.
World Path Logic (WPL) is introduced as a possible target language. Deduction in WPL works very much like in ordinary logic, the only significant difference is the need for a special purpose unification, which unifies world paths under an equational theory (E-unification). Relating WPL to a well understood first order logic of restricted quantification, the properties of WPL, that make deduction work, are examined. The obtained theoretical results are the basis for the following treatment of subsumption in WPL.
Subsumption is analyzed treating a clause as a scheme standing for the set of its ground instances. Although the notion of ground instances in WPL is different from ordinary logic, it turns out that -- just like in ordinary logic -- a clause Cl subsumes another clause C2, if there exists a substitution θ such that C1θ ⊆ C2. Once the special purpose unification has been implemented into a theorem prover to allow for deduction in WPL, existing subsumption tests then work without any further changes.
Wilkerson, Ralph W.
McMillin, Bruce M.
Hilgers, Michael Gene
M.S. in Computer Science
University of Missouri--Rolla
viii, 86 pages
© 1993 Dirk Heydtmann, All rights reserved.
Thesis - Restricted Access
Print OCLC #
Link to Catalog Record
Electronic access to the full-text of this document is restricted to Missouri S&T users. Otherwise, request this publication directly from Missouri S&T Library or contact your local library.http://merlin.lib.umsystem.edu/record=b2520048~S5
Heydtmann, Dirk, "Subsumption in modal logic" (1993). Masters Theses. 1186.
Share My Thesis If you are the author of this work and would like to grant permission to make it openly accessible to all, please click the button above.