Rules that are admissible can be used in any derivations in any axiomatic system of a logic . In this thesis we studied a method for checking the admissibility of rules in the modal logic S4 . this method is based on a standard semantic ground tableau approach . In particular , reduced rule admissibility in S4 to satisfiability of a formula in a logic that extends S4 . The extended logic is characterised by a 0cm 0cm 0pt" that satisfy a variant of the co-cover property . The 0cm 0cm 0pt" order specification . also , a method has been introduced for synthesising tableau calculi . If $ S_{L} $ is not already normalised we ?rst normalise it . Thus assume $ S_{L}=S_{L}^{+}\\cup S_{L}^{-}\\cup S_{L}^{b} $ . Next we take a positive speci?cation $ \\xi_{L}^{+}\\in S_{L}^{+} $ . Eliminating existential quanti?ers using Skolemisation and Essentially , the antecedent of the implication has become the main premise in the numerator and the succedent is turned into the denominators of the rule . Analogously , we generate a tableau rule for each negative speci?cation $ \\xi_{L}^{-}\\in S_{L}^{-} $.\\\\ In summary , the generated tableau calculus consists of these rules.\\\\ $ a)~~ ~ $ The decomposition rules $ \\rho_{+}^{\\sigma}(\\xi) $ and $ \\rho_{-}^{\\sigma}(\\xi^{'}) $ corresponding to all positive speci?cations $ \\xi\\in S_{L}^{+} $ and all negative speci?cations $ \\xi^{'})\\in S_{L}^{-} $.\\\\ $ b)~~ ~ $ The theory rules $ \\rho(\\xi) $ corresponding to all sentences $ \\xi $ in the background theory $ S_{L}^{b} $.\\\\ $ c)~~ ~ $ The equality rules.\\\\ $ d)~~ ~ $ The closure rules.\\\\ The method introduced in this thesis automatically produces a sound and constructively complete tableau calculus from the semantic ?rst-order speci?cation of a many-sorted logic . In this thesis , The method for has been shown $ S4 $ . Soundness and Constructive Completeness has been proven of calculus $ T_{S4} $ synthesised from a normalised semantic speci?cation $ S_{S4} $.\\\\ Then $ S4 $ has been extended to $ S4^{u,+} $ using co-cover property . It has been shown that the logic admit ?nite ?ltration with respect to a well-de?ned ?rst-order semantics then added a general blocking mechanism provides a terminating tableau calculus . The process of generating tableau rules can be completely automated and produces , together with the blocking mechanism , an automated procedure for generating tableau decision procedures . For illustration has been shown the workability of the approach for a description logic with transitive roles and propositional intuitionistic logic . finally a method has been presented for synthesising tableau decision procedures this can be turned into a sound , complete and terminating tableau calculus for the extended logic , and gives a tableau based method for determining the admissibility of rules .