Optimised Modal Translation and Resolution

Schmidt, Renate A.

Local TagsRelease HistoryDetailsSummary

Optimised Modal Translation and Resolution

Schmidt, R. A. (1997). Optimised Modal Translation and Resolution. PhD Thesis, Universität des Saarlandes, Saarbrücken.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-38C0-8 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-AD00-7

Genre: Thesis

Files

show Files

Locators

show

Creators

show

hide

Creators:
Schmidt, Renate A.¹, Author

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

Content

show

hide

Free keywords: -

Abstract: This thesis studies the optimised functional translation of propositional modal logics to first-order logic, and first-order resolution as a means for realising modal reasoning. The optimised functional translation maps modal logics to a lattice of clausal logics, called path logics. The general apparatus of inference for path logics is theory resolution. We show that satisfiability in basic path logic and certain extensions can be decided by resolution and condensing without requiring additional refinement strategies. We propose an improved theory unification algorithm for \textit{S4}, and we present a calculus of ordered $E$-resolution with normalisation. We show also that some essentially second-order modal logics convert to path logics, which can be exploited for accomodating inference for modal logics with numerical quantifiers in a calculus of resolution and simple arithmetic.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Accepted: 1997-03-11Date issued: 1997

Publication Status: Issued

Pages: -

Publishing info: Saarbrücken : Universität des Saarlandes

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 519590
Other: Local-ID: C1256104005ECAFC-B051B4AF36990D1EC1256559005776F7-Schmidt97d

Degree: PhD

Event

show

Legal Case

show

Project information

show

Source

show