Resolution-Based Calculi for Modal Logics

Mohr, Erik

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Thesis

Resolution-Based Calculi for Modal Logics

MPS-Authors

/persons/resource/persons45060

Mohr, Erik
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Mohr, E. (1995). Resolution-Based Calculi for Modal Logics. Diploma Thesis, Universität des Saarlandes, Saarbrücken.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AD18-7

Abstract

Based on different translation approaches from first-order modal logic into
first-order predicate logic we develop several kinds of resolution-based calculi
with additional theory clauses, inference rules or special unification
algorithms.
Especially the methods presented for the semi-functional and functional
approaches
lead to limited branching in the proof search tree and therefore to smaller sets
of generated clauses. In all cases soundness and (refutation) completeness
proofs
for these calculi are provided. The methods have been applied to serial modal
logics (i.e. modal logics containing the so-called axiom D) with constant, (and
partially) varying, increasing and decreasing domain structures and any
combination of the following modal logic axioms: T, B, 4 and 5.