Institutional Repository

# Proof systems for propositional modal logic

 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, 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 en Gore (1995) will be reviewed. 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)
﻿