Investigations On Normal Forms In Intermediate Logics

Intermediate logics are an extensive class of propositional logics which have recently received significant attention in computer science. Normal form plays an important role in logic and related research areas, especially in automated theorem proving, automated reasoning and logic programming. The purposes of the thesis are to discover some useful normal forms for these areas in intermediate logics; to obtain the existence results for these normal forms in intermediate logics; and to devise some algorithms to reduce an arbitrary formula to the above normal forms.In this thesis we carry a thorough investigation into normal forms in intermediate logics. Six kinds of normal forms are focused, including implicational normal form, extended conjunctive and disjunctive normal forms, and weak conjunctive, disjunctive and implicational normal forms. The weakest intermediate logic with implicational normal form is proved to be the logic of here and there, and the existence of three kinds of weak normal forms in Go|¨del logics is also investigated. To reduce a formula to every normal form mentioned above, two kinds of reduction methods axe presented, one of which is based on model-characterizing formulas and the other on rewriting systems. As byproducts of these investigations, four kinds of model-characterizing formulas are obtained; a concept of elementary implication between two Kripke models are introduced; and the suffice and necessary condition of elementary implication between linear Kripke models is also given. In the end, we study the complexities of reductions to these normal forms.