Institutional Repository

Proof systems for propositional modal logic

Show simple item record

dc.contributor.advisor Meyer, Thomas Andreas Van der Vyver, Thelma 2015-01-23T04:24:24Z 2015-01-23T04:24:24Z 1997-11
dc.identifier.citation Van der Vyver, Thelma (1997) Proof systems for propositional modal logic, University of South Africa, Pretoria, <> en
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 M. Sc. (Computer Science)

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UnisaIR


My Account