Sharif Digital Repository

Order reduction is a very important issue in Control Theory. A growing need for order reduction models in different fields such as simulation, identification, and design of control system shows this significance. Actually, a high-order system makes a great deal of complexity in designing hardware of control system, debugging, and implementation. Till nowadays, many repetitive as well as nonrepetitive methods with various criteria have been introduced to find low-order models. In this research, order reduction of linear time invariant system models is analyzed. The selected criterion for measuring error between original system and reduced order system is the norm of H1 because it is not only... 

Increasing use of polymeric materials, especially in the packaging industry, besides the problems that exist in recycling these materials, has become a serious concern for the environment. The synthetic polymers are used widely in packaging industry so they have a considerable role in waste production in packaging industry. One way to solve this problem is adding a natural polymer to the synthetic polymer, as a result it becomes friendly environmentally. Starch is one of these natural polymers which is cheap and has the ability to complete degradation in the environment.using row starch in the polymeric compounds causes a severe drop in compound’s properties. For this reason, row starch must... 

Nowadays, BDI architecture is of the most well known agent’s architectures. BDI architecture or the architecture in which the system is viewed as rational agents based on the attitudes of belief, desire and intention represents an abstraction of human deliberation based on a theory of rational action in the human cognition process. BDI logic introduced by Rao and Georgeff have been widely used as the theoretical basis of specification and implementation of rational agents. BDI logic is limited to deal with crisp assertion, while the assertions encountered in real world are not precise and thus cannot be treated simply by using yes or no. Moreover, In order to obtain more human like agents we... 

Pregroups as a mathematical structure, are replacement for Lambek's type caregorial grammar which much used in Computational Linguistics. Because of computational and logical properties of pregroups, we can use them as strong tool to analyse the sentence structure of many natural languages. This kind of analysis has been done for English, French, German, Polish, Italian, Arabic and Japanese. In case of Persian language, analysis of simple and compound sentences structure with simple tense verbs and explicit subjects and objects has been studied. In this M.Sc. thesis, we will extent analysis of Persian sentence structure to sentences with compound tense verbs and implicit subjects and objects... 

Description logic is a family of knowledge representive languages which represents knowledge via propositional logic (first order logic) propositions and constructors and applies its services for reasoning and consistency checking. Nowadays description logic and its popular reasoner FaCT++ which applies tablue reasoning technique are widely used in applications such as semantic web and onthologies. Model checking is a technique for systems and models verification and to guarantee the accuracy of design. Given a model description and a specification formula, the model checker verifies the model against the specification and decides if the model satisfies the description or not. Main model... 

In logic literature, the phrase “basic logic” can refer to three different logical systems. First, basic propositional logic (BPL) that was introduced by A. Visser in 1981. This logic is a subintuitionistic logic, that can be obtained from intuitionistic logic by a weakening of modus ponens. One decade later, Wim Ruitenberg regarding philosophical critiques of logical connectives, reintroduced BPL and its first order extension, BQC. From then, different aspects of basic logic have been investigated by logicians all over the world. Another logical system with the name “basic logic” is the system that was introduced by G. Sambin and G. Battilotti in 1997. The goal of this system is to provide... 

Deontic logic is used to formalize legal reasoning. To apply this logic in law, we describe tersely some efforts to improve this logic by relativizing its operations with respect to different people and groups of society. Until now, this logic was restricted to formalize “what must be”. We extend this logic to dyadic logic to formalize “what must be done”.
In practice, legal reasoning leads to non-monotonic logics, the most applicable one in law is defeasible logic. So it is necessary to combine deontic and defeasible logics to formalize legal reasoning in a more appropriate way. To do that, we must adjust possible worlds of these two logics. In this way, we find a method for... 

In this dissertation, we study (first-order) arithmetical interpretations for propositional (modal and non-modal) logics. More precisely, the following results are included in this dissertation: an axiomatization for provability logic of Heyting Arithmetic, HA, and its self-completion HA := HA + PrHA(⌜A⌝) ! A for 1-substitutions is provided, and their arithmetical completeness theorems are proved. We also show that they are decidable. The de Jongh property for Basic Arithmetic BA, HA and HA + □ are proved  

In constructive mathematics, one has to construct a mathematical object in order to show that it exists. Consequently, some of classical theorems are not acceptable from a constructive point of view. In particular, the constructive validity of the parts of mathematics that play a role in forming physical theories is of interest. Here, we want to examine the constructive provability of some theorems related to quantum mechanics  

In this thesis, we investigate constructive measure theory in two schools of constructivism; intuitionistic mathematics and Bishop’s constructive mathematics.In this regard, first, we examine some classical propositions on measurability in both schools. Then we give a comparison between measurability in the two schools  

Epistemic algorithms are instructions and rules based on knowledge of agents. These algorithms by individual or group knowledge of agents make decisions about future behavior of systems. Epistemic gossip protocols is one of these algorithms. They are used to for spreading secrets among nodes in a network. According to individual knowledge of each node they decide who calls whom in each step. In security problems epistemic algorithms are used to detect the safety of protocols. Some epistemic notions like ignorance and contingency are used in formalization of security problems. In the thesis we study these epistemic algorithms  

In this thesis, we study proof complexity conjectures and also introduce their mathematical logic equivalents in terms of provability and unprovability in strong enough first-order arithmetical theories. One of the most important conjectures in this theory is the following conjecture. The non-existence of an optimal proof system for propositional tautologies: In general, a proof system is a computable function in polynomial time such that its range is exactly the set of tautologies. We say proof system P, polynomially simulates proof system Q if and only if there exists a polynomial h such that for all tautologies such as A and for all proofs like a, if Qpaq A, then there exists a proof...