In this dissertation we prove the Completeness, Soundness and Compactness of the Monadic Hybrid Calculus MHC and we prove its expressive equivalence to the Monadic Predicate Calculus MPC. The Monadic Hybrid Calculus MHC is a new system that is based on the (propositional) modal logic S5. It is “Hybrid” in the sense that it includes quantifier free MPC and therefore, unlike S5, allows free individual constants. The main innovation in this system is the elimination of bound variables. In MHC, upper case letters denote properties and lower case letters denote individuals. Universal quantification is represented by square brackets, [], and existential quantification is represented by angled brackets, 〈〉. Thus, All Athenians are Greek and mortal is formalized as [A](G∧M), Some mortal Greeks are Athenians as 〈M∧G〉A, and Socrates is mortal and Athenian as s(M∧A). We give the formal syntax and the formal semantics of [MHC] and give Beth-style Tableau Rules (Inference Rules). In these rules, if [P]Q is on the right then we select a new constant [v] and we add [vP] on left, vQ on the right, and we cancel the formula. If [P]Q is on the left then we select a pre-used constant p and split the tree. We add pP on the right of one branch and pQ on the left of the other branch. We treat 〈P〉Q similarly. Our Completeness proof uses induction on formulas down a path in the proof tree. Our Soundness proof uses induction up a path. To prove that MPC is logically equivalent to the Monadic Predicate Calculus, we present algorithms that transform formulas back and forth between these two systems. Compactness follows immediately. Finally, we examine the pragmatic usage of the Monadic Hybrid Calculus and we compare it with the Monadic Predicate Calculus using natural language examples. We also examine the novel notions of the Hybrid Predicate Calculus along with their pragmatic implications. / Graduate / 0800 / 0984

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)

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)