وسائل تشكيل الصورة للموت والحياة عند جبران خليل جبران

The concept of imagery plays an important role in literacy, critical and rhetorical studies. Different research studies describe the reality of imagery its role and methods of its formulation in literary work. Imageries are among those literary tools, through which writers share their experiences. The writer uses different literary tools to formulate imagery and to share their feelings with readers. These tools are simile, metaphor, sensuousness, personification and oxymoron etc. Khalil Jubran was among those writers who frequently used imagery in his work to reflect his inner feelings in a better way. This research study was focused only on the use of imagery tools in his work for the formulation of life and death.

Formalization of Transform Methods Using Higher-Order-Logic Theorem Proving

Transform methods, such as the Laplace and the Fourier transforms, are widely used for analyzing the differential equations modeling the continuous dynamics of the engineering and physical systems. Traditionally, the transform methods based analysis is performed using paper-and-pencil proof and computer-based simulation techniques, such as sym bolic and numerical methods. However, due to their inherent limitations, such as the human-error proneness of paper-and-pencil proof methods and the presence of unverified symbolic algorithms, discretization and numerical errors in the simulations methods, these techniques cannot provide accurate results. The incomplete and inaccurate analysis poses a serious threat to the safety-critical domain, such as medicine and transportation, of engineering systems. To overcome these limitations, we propose to use higher-order-logic theorem proving to reason about the continuous dynamics of the engineering and physical systems using transform methods. The main advantages of this approach are the high expressiveness of the higher-order logic and the soundness of theorem provers, which provide absolute accu racy of the analysis. In particular, this thesis presents a higher-order-logic formalization of the Laplace and the Fourier transforms, which includes their formal definitions and the formal verification of their classical properties. The considered properties include integra bility, linearity, time shifting, frequency shifting, modulation, time scaling, time reversal, integration in time domain, differentiation in time domain, the Laplace and the Fourier transforms of a n-order differential equation and uniqueness. The formal reasoning about these properties involves multivariable calculus theories, i.e., the differential, integration, transcendental, topological, complex numbers, Lp spaces and vectors theories. Based on the availability of these theories in the HOL Light theorem prover, we chose it for our work. This thesis also provides the formal verification of a relationship between various transfor methods, i.e., the relationship between the Laplace and the Fourier transforms, and the relationship between the Fourier transform and the Fourier Cosine and Sine transforms. The proposed formalization plays a vital role in formally verifying the solutions of differential equations in both the time and the frequency domain and thus facilitates formal dynamical analysis of these systems. To illustrate the practical utilization and effectiveness, we use our proposed formalization for formally analyzing a 4-π soft error crosstalk model for Integrated Circuits (ICs), an audio equalizer, an Unmanned Free swimming Submersible (UFSS) vehicle and a platoon of automated vehicles using HOL Light.