Subsumption in modal logic

Author

Dirk Heydtmann

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 θ 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.

Advisor(s)

Wilkerson, Ralph W.

Committee Member(s)

McMillin, Bruce M.
Hilgers, Michael Gene

Department(s)

Computer Science

Degree Name

M.S. in Computer Science

Comments

A report which is substantially this thesis is available here for download.

Publisher

University of Missouri--Rolla

Publication Date

Fall 1993

Pagination

viii, 86 pages

Note about bibliography

Includes bibliographical references (pages 83-85).

Rights

© 1993 Dirk Heydtmann, All rights reserved.

Document Type

Thesis - Restricted Access

File Type

text

Language

English

Thesis Number

T 6662

Print OCLC #

30016812

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.

Recommended Citation

Heydtmann, Dirk, "Subsumption in modal logic" (1993). Masters Theses. 1186.
https://scholarsmine.mst.edu/masters_theses/1186