Return to search

Proof systems for propositional modal logic

In classical propositional logic (CPL) logical reasoning is formalised as logical entailment and can be computed by means of tableau and resolution proof procedures. Unfortunately CPL is not expressive enough and using first order logic (FOL) does not solve the problem either since proof procedures for these logics are not decidable. Modal propositional logics (MPL) on the other hand are both decidable and more expressive than CPL. It therefore seems reasonable to apply tableau and resolution proof systems to MPL in order to compute logical entailment in MPL. Although some of the principles in CPL are present in MPL, there are complexities in MPL that are not present in CPL. Tableau and resolution proof systems which address these issues and others will be surveyed here. In particular the work of Abadi & Manna (1986), Chan (1987), del Cerro & Herzig (1988), Fitting (1983, 1990) and
Gore (1995) will be reviewed. / Computing / M. Sc. (Computer Science)

Identiferoai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:unisa/oai:umkn-dsp01.int.unisa.ac.za:10500/16280
Date11 1900
CreatorsVan der Vyver, Thelma
ContributorsMeyer, Thomas Andreas
Source SetsSouth African National ETD Portal
LanguageEnglish
Detected LanguageEnglish
TypeDissertation
Format1 online resource (175 leaves)

Page generated in 0.0021 seconds