Proof systems for propositional modal logic

Van der Vyver, Thelma

dc.contributor.advisor	Meyer, Thomas Andreas
dc.contributor.author	Van der Vyver, Thelma
dc.date.accessioned	2015-01-23T04:24:24Z
dc.date.available	2015-01-23T04:24:24Z
dc.date.issued	1997-11
dc.identifier.citation	Van der Vyver, Thelma (1997) Proof systems for propositional modal logic, University of South Africa, Pretoria, <http://hdl.handle.net/10500/16280>	en
dc.identifier.uri	http://hdl.handle.net/10500/16280
dc.description.abstract	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.	en
dc.format.extent	1 online resource (175 leaves)	en
dc.language.iso	en
dc.subject	Classical propositional logic	en
dc.subject	Propositional modal logic	en
dc.subject	Resolution proof systems	en
dc.subject	Tableau proof systems	en
dc.subject	Local logical entailment	en
dc.subject	Global logical entailment	en
dc.subject.ddc	006.3
dc.subject.lcsh	Logic, Symbolic and mathematical	en
dc.subject.lcsh	Modality (Logic)	en
dc.subject.lcsh	Proof theory	en
dc.subject.lcsh	Proposition logic	en
dc.subject.lcsh	Automatic theorem proving	en
dc.subject.lcsh	Artificial intelligence	en
dc.title	Proof systems for propositional modal logic	en
dc.type	Dissertation
dc.description.department	Computing
dc.description.degree	M. Sc. (Computer Science)