Resolution-Based Calculi for Modal Logics

Mohr, Erik

Datensatz

DATENSATZ AKTIONENEXPORT

DownloadE-Mail

Bitte beachten Sie, dass eine neuere Version dieses Datensatzes verfügbar ist:
https://pure.mpg.de/pubman/item/item_1331912_3

DetailsÜbersicht

Resolution-Based Calculi for Modal Logics

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

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD18-7 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-ACE5-B

Genre: Hochschulschrift

ausblenden:

Urheber:
Mohr, Erik¹, Autor

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: 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.