Abstract
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 6 such that C10 £ 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.
Recommended Citation
Heydtmann, Dirk and Wilkerson, Ralph W., "Subsumption in Modal Logic" (1993). Computer Science Technical Reports. 63.
https://scholarsmine.mst.edu/comsci_techreports/63
Department(s)
Computer Science
Report Number
CSC-93-33
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1993 University of Missouri--Rolla, All rights reserved.
Publication Date
01 Dec 1993
Comments
This report is substantially the M. S. thesis of the first author, completed December 1993