max planck institut

informatik

informatik

**MPI-I-94-223**. June** **1994, 465 pages. | Status:** **available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

Traditional logics manipulate formulas.

The message of this book is to manipulate pairs;

formulas and labels. The labels annotate the formulas. This sounds very simple

but it turned out to be a big step, which makes a serious difference, like the

difference between using one hand only or allowing for the coordinated use of

two hands. Of course the idea has to be made precise, and its advantages and

limitations clearly demonstrated. `Precise' means a good mathematical

definition and `advantages demonstrated' means case studies and applications in

pure logic and in AI.

To achieve that we need to address the following:

\begin{enumerate}

\item Define the notion of {\em LDS}, its proof theory and semantics and relate

it to traditional logics.

\item Explain what form the traditional concepts of cut elimination, deduction

theorem, negation, inconsistency, update, etc.\ take in {\em LDS}.

\item Formulate major known logics in {\em LDS}. For example, modal and

temporal logics, substructural logics, default, nonmonotonic logics, etc.

\item Show new results and solve long-standing problems using {\em LDS}.

\item Demonstrate practical applications.

\end{enumerate}

This is what I am trying to do in this book. Part I of the book is an

intuitive presentation of {\em LDS} in the context of traditional current views

of monotonic and nonmonotonic logics. It is less oriented towards the pure

logician and more towards the practical consumer of logic. It has two tasks,

addressed in two chapters.

These are:

\begin{itemlist}{Chapter 1:}

\item [Chapter1:] Formally motivate {\em LDS} by starting from the traditional

notion of `What is a logical system' and slowly adding features to it until it

becomes essentially an {\em LDS}.

\item [Chapter 2:] Intuitively motivate {\em LDS} by showing many examples

where labels are used, as well as some case studies of familiar logics (e.g.\

modal logic) formulated as an {\em LDS}.

\end{itemlist}

The second part of the book presents the formal theory of {\em LDS} for the

formal logician. I have tried to avoid the style of definition-lemma-theorem

and put in some explanations. What is basically needed here is the formulation

of the mathematical machinery capable of doing the following.

\begin{itemize}

\item Define {\em LDS} algebra, proof theory and semantics.

\item Show how an arbitrary (or fairly general) logic, presented traditionally,

say as a Hilbert system or as a Gentzen system, can be turned into an {\em LDS} formulation.

\item Show how to obtain a traditional formulations (e.g.\ Hilbert) for an

arbitrary {\em LDS} presented logic.

\item Define and study major logical concepts intrinsic to {\em LDS} formalisms.

\item Give detailed study of the {\em LDS} formulation of some major known logics (e.g.\

modal logics, resource logics) and demonstrate its advantages.

\item Translate {\em LDS} into classical logic (reduce the `new' to the `old'),

and explain {\em LDS} in the context of classical logic (two sorted logic,

metalevel aspects, etc).

\end{itemize}

\begin{itemlist}{Chapter 1:}

\item [Chapter 3:] Give fairly general definitions of some basic concepts of {\em

LDS} theory, mainly to cater for the needs of the practical consumer of logic

who may wish to apply it, with a detailed study of the metabox system.

The presentation of Chapter 3 is a bit tricky. It may be too formal for the

intuitive reader, but not sufficiently clear and elegant for the mathematical

logician. I would be very grateful for comments from the readers for the next

draft.

\item [Chapter 4:] Presents the basic notions of algebraic {\em LDS}. The

reader may wonder how come we introduce algebraic {\em LDS} in chapter 3 and

then again in chapter 4. Our aim in chapter 3 is to give a general definition

and formal machinery for the applied consumer of logic. Chapter 4 on the other

hand studies {\em LDS} as formal logics. It turns out that to formulate an

arbitrary logic as an {\em LDS} one needs some specific labelling algebras and

these need to be studied in detail (chapter 4). For general applications it is

more convenient to have general labelling algebras and possibly mathematically

redundant formulations (chapter 3). In a sense chapter 4 continues the topic of the

second section of chapter 3.

\item [Chapter 5:] Present the full theory of {\em LDS} where labels can be

databases from possibly another {\em LDS}. It also presents Fibred Semantics for

{\em LDS}.

\item [Chapter 6:] Presents a theory of quantifers for {\em LDS}. The material

for this chapter is still under research.

\item [Chapter 7:] Studies structured consequence relations. These are logical

system swhere the structure is not described through labels but through some

geometry like lists, multisets, trees, etc. Thus the label of a wff $A$ is

implicit, given by the place of $A$ in the structure.

\item [Chapter 8:] Deals with metalevel features of {\em LDS} and its

translation into two sorted classical logic.

\end{itemlist}

Parts 3 and 4 of the book deals in detail with some specific families of logics.

Chapters 9--11 essentailly deal with substructural logics and their variants.

\begin{itemlist}{Chapter10:}

\item [Chapter 9:] Studies resource and substructural logics in general.

\item [Chapter 10:] Develops detailed proof theory for some systems as well as

studying particular features such as negation.

\item [Chapter 11:] Deals with many valued logics.

\item [Chapter 12:] Studies the Curry Howard formula as type view and how it

compres with labelling.

\item [Chapter 13:] Deals with modal and temporal logics.

\end{itemlist}

Part 5 of the book deals with {\em LDS} metatheory.

\begin{itemlist}{Chapter15:}

\item [Chapter 14:] Deals with labelled tableaux.

\item [Chapter 15:] Deals with combining logics.

\item [Chapter 16:] Deals with abduction.

\end{itemlist}

Acknowledgement:** **

References to related material:

To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
---|---|

MPI-I-94-223.pdf | 1942 KBytes; 1804 KBytes |

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView |