| Summary: | A formalism and calculus is presented for the treatment of a normal modal logic with two principal operators: 'necessarily next' and 'necessarily prior'. The formalism is proposed as an efficient means of representing classes of game configurations for a broad range of finite games. As part of this treatment a system of context-free, strongly normalizing rewrite rules is given, which identifies logically equivalent formulae and is itself adequate for K, the weakest normal propositional logic with one (principal) operator. Deduction (and deducibility), with respect to a given theory, is introduced and its soundness is shown via standard models. The canonical model construction is given, yielding completeness and, through filtrations, decidability. Finally, a mechanism, using decidability (and some properties of the rewrite system) is given for obtaining a (logically equivalent) reduced form of formulae, modulo a finite theory. Throughout the thesis, a score of smaller results and ideas are also presented.
|
|---|
