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)
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:unisa/oai:umkn-dsp01.int.unisa.ac.za:10500/16280 |
| Date | 11 1900 |
| Creators | Van der Vyver, Thelma |
| Contributors | Meyer, Thomas Andreas |
| Source Sets | South African National ETD Portal |
| Language | English |
| Detected Language | English |
| Type | Dissertation |
| Format | 1 online resource (175 leaves) |
Page generated in 0.0025 seconds