A family of labelled deductive systems called Modal Labelled Deductive Systems (MLDS) is described. Modal theories are here defined as (possibly singleton) structures of local actual worlds, called ``configurations''. A model-theoretical semantics is given (based on first-order logic) and its equivalence to Kripke semantics for normal modal logic is shown whenever the initial configuration is a single actual world. A natural deduction style proof system is defined for a wide family of propositional MLDS and its soundness and completeness proved with respect to the given semantics. Finally, an extension to the predicate case is sketched in terms of some natural deduction rules for quantifiers showing also how this approach could solve problems associated with the nesting of quantifiers within the scope of modal operators.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.