تركيب منطق هاي زماني ساختي با فراسازگاري

چكيده انگليسي :

Combining Linear Time Temporal Logic with Constructiveness and Paraconsistency Kobra Salehi k salehy80@yahoo com January 10 2012 Master of Science Thesis Department of Mathematical Science Isfahan University of Technology Isfahan 84156 83111 IranSupervisors Dr Mojtaba Aghaei aghaei@cc iut ac ir 2000 MSC 03B53 o3B44 Key word Uunbounded Temporal logic Paraconsistent Constructive Completeness Cut elimination Abstract It is known that linear time temporal logic LTL which is an extension of classical logic is usefulfor expressing temporal reasoning as investigated in computer science and for verifying andspecifying concurrent systems In this thesis two constructive and bounded versions of LTL whichare extensions of intuitionistic logic or Nelson s paraconsistent logic are introduced as Gentzen typesequent calculi These logics IB l and PB l are intended to provide a useful theoretical basis forrepresenting not only temporal linear time but also constructive and paraconsistent inconsistency tolerant reasoning Although the standard LTL has an infinite unbounded time domain the timedomain of the proposed logics is bounded by a fixed positive integer Despite the restriction on thetime domain the logics can derive almost all the typical temporal axioms of LTL As a merit ofbounding time faithful embeddings into intuitionistic logic and Nelson s paraconsistent logic areshown for IB l and PB l respectively Completeness with respect to Kripke semantics cut elimination normalization with respect to natural deduction and decidability theorems for thenewly defined logics are proved as the main results of this thesis Display sequent calculi IB l forIB l and PB l for PB l are introduced also sound and complete for these logics are presented Such a theoretical merit may not be obtained for an unbounded and intuitionistic version of LTL because the unbounded time domain requires some infinite inference rules Such infinite inferencerules are neither familiar to nor welcomed by researchers who study automated reasoning since theserules cannot be implemented efficiently Indeed the replacement of such infinite rules of certain proofsystems by finitary rules is known as an important issue It is also known that to restrict the timedomain is a technique that may be applied to obtain a decidable or efficient fragment of LTL IB l and PB l may provide a good proof theoretical basis for such practical applications as well as a goodtool for automated reasoning with bounded linear time formalisms Information represented by classical logic is complete information every formula is either true ornot true in a model Representing only complete information is plausible in classical mathematics which is a discipline handling eternal truth and falsehood The statements of classical mathematics donot change their truth value in the course of time and the classical mathematician may assume everysituation to support either the truth or the falsity of such a statement The assumption of completeinformation is however inadequate when it comes to representing the information available to realworld agents It is desirable inconsistent as well as incomplete information since some real systemssuch as software systems need to ensure inconsistency tolerance and then it is desirable to avail of alogic which is paracomplete in the sense of not validating the law of excluded middle The presentthesis s approach is based on N4 since N4 is known as a very useful paraconsistent logic inphilosophical logic computer science and because N4 is based on positive intuitionistic logic

صالحي، كبري

تركيب منطق هاي زماني ساختي با فراسازگاري

استنتاج طبيعي , سلامت , تماميت , نرمال سازي و حذف برش