9081

8426

كارشناسي ارشد

رياضي محض

اصفهان: دانشگاه صنعتي اصفهان، دانشكده علوم رياضي

1392

هفت،97ص.: مصور

ص.ع.به فارسي و انگليسي

مجتبي آقايي

10/4/93

رسول رمضانيان، مجيد عليزاده

رياضي

ID8426

A Tableau Method for Checking Rule Admissibility in S4 Maryam Rostami Giv m rostamigiv@math iut ac ir january 12 2014 Department of Mathematical Sciences Isfahan University of Technology Isfahan 84156 83111 Iran Supervisor Dr Mojtaba Aghaei aghaei@cc iut ac ir 2010 MSC Keywords Tableau calculus admissible rule modal logic S4 tableau synthesis framework AbstractRules that are admissible can be used in any derivations in any axiomatic system of a logic In thisthesis we studied a method for checking the admissibility of rules in the modal logic S4 this methodis based on a standard semantic ground tableau approach In particular reduced rule admissibilityin S4 to satis ability of a formula in a logic that extends S4 The extended logic is characterised by aclass of models that satisfy a variant of the co cover property The class of models can be formalisedby a well de ned rst order speci cation also a method has been introduced for synthesising tableau calculi If SL is not already normalised we rst normalise it Thus assume SL SL SL SL Next bwe take a positive speci cation L SL Eliminating existential quanti ers using Skolemisation and Essentially the antecedent of the implication has become the main premise in the numerator and thesuccedent is turned into the denominators of the rule Analogously we generate a tableau rule for each negative speci cation L SL In summary the generated tableau calculus consists of these rules The decomposition rules and corresponding to all positive speci cations SL a and all negative speci cations SL b The theory rules corresponding to all sentences in the background theory SL b The equality rules c The closure rules d The method introduced in this thesis automatically produces a sound and constructively completetableau calculus from the semantic rst order speci cation of a many sorted logic In this thesis

مجتبي آقايي

رسول رمضانيان، مجيد عليزاده