Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template :: Thesis :: Schmidt, Renate A.


Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit


Author
Author(s)*:Schmidt, Renate A.
BibTeX citekey*:Schmidt97d
Language:English

Title, School
Title*:Optimised Modal Translation and Resolution
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation
Month:November
Year:1997


Note, Abstract, Copyright
LaTeX 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.
Keywords:automated theorem proving, correspondence problem, E-resolution, graded modal logic, modal logics, optimised functional translation, ordered resolution, quantifier elimination, resolution decision procedures, theorem proving for non-classical logics, theory resolution, translation methods, E-unification
HyperLinks / References / URLs:http://www.mpi-sb.mpg.de/~schmidt/publications/PhD.ps.gz

Referees, Status, Dates
1. Referee:Ohlbach, Hans Jürgen
2. Referee:Ganzinger, Harald
Supervisor:Ohlbach, Hans Jürgen
Status:Completed
Date Kolloquium:11 March 1997
Chair Kolloquium:Wilhelm, Reinhard

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:experts only
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat

BibTeX Entry:

@PHDTHESIS{Schmidt97d,
AUTHOR = {Schmidt, Renate A.},
TITLE = {Optimised Modal Translation and Resolution},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {1997},
TYPE = {Doctoral dissertation}
MONTH = {November},
}



Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Renate A. Schmidt
Created
11/24/1997 04:55:20 PM
Revisions
14.
13.
12.
11.
10.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Renate A. Schmidt
Renate A. Schmidt
Edit Dates
08/30/99 03:00:10 PM
08/30/99 02:59:33 PM
08/30/99 02:59:14 PM
28/10/98 11:59:25
28/10/98 11:58:51