A semantic middleware to enhance current multimedia retrieval systems with content-based functionalities

210 p. : graf.

Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

Semi-automatic generation of learning domain modules for technology supported learning systems

In a time when Technology Supported Learning Systems are being widely used, there is a lack of tools that allows their development in an automatic or semi-automatic way. Technology Supported Learning Systems require an appropriate Domain Module, ie. the pedagogical representation of the domain to be mastered, in order to be effective. However, content authoring is a time and effort consuming task, therefore, efforts in automatising the Domain Module acquisition are necessary.Traditionally, textbooks have been used as the main mechanism to maintain and transmit the knowledge of a certain subject or domain. Textbooks have been authored by domain experts who have organised the contents in a means that facilitate understanding and learning, considering pedagogical issues.Given that textbooks are appropriate sources of information, they can be used to facilitate the development of the Domain Module allowing the identification of the topics to be mastered and the pedagogical relationships among them, as well as the extraction of Learning Objects, ie. meaningful fragments of the textbook with educational purpose.Consequently, in this work DOM-Sortze, a framework for the semi-automatic construction of Domain Modules from electronic textbooks, has been developed. DOM-Sortze uses NLP techniques, heuristic reasoning and ontologies to fulfill its work. DOM-Sortze has been designed and developed with the aim of automatising the development of the Domain Module, regardless of the subject, promoting the knowledge reuse and facilitating the collaboration of the users during the process.

Modelling the Effect of Climate Change on Environmental Pollution Losses from Dairy Systems in the UK

21 p.

Advanced Reaction Systems for Hydrogen Production

[EN] This PhD work started in March 2010 with the support of the University of the Basque Country (UPV/EHU) under the program named “Formación de Personal Investigador” at the Chemical and Environmental Engineering Department in the Faculty of Engineering of Bilbao. The major part of the Thesis work was carried out in the mentioned department, as a member of the Sustainable Process Engineering (SuPrEn) research group. In addition, this PhD Thesis includes the research work developed during a period of 6 months at the Institut für Mikrotechnik Mainz GmbH, IMM, in Germany. During the four years of the Thesis, conventional and microreactor systems were tested for several feedstocks renewable and non-renewable, gases and liquids through several reforming processes in order to produce hydrogen. For this purpose, new catalytic formulations which showed high activity, selectivity and stability were design. As a consequence, the PhD work performed allowed the publication of seven scientific articles in peer-reviewed journals. This PhD Thesis is divided into the following six chapters described below. The opportunity of this work is established on the basis of the transition period needed for moving from a petroleum based energy system to a renewable based new one. Consequently, the present global energy scenario was detailed in Chapter 1, and the role of hydrogen as a real alternative in the future energy system was justified based on several outlooks. Therefore, renewable and non-renewable hydrogen production routes were presented, explaining the corresponding benefits and drawbacks. Then, the raw materials used in this Thesis work were described and the most important issues regarding the processes and the characteristics of the catalytic formulations were explained. The introduction chapter finishes by introducing the concepts of decentralized production and process intensification with the use of microreactors. In addition, a small description of these innovative reaction systems and the benefits that entailed their use were also mentioned. In Chapter 2 the main objectives of this Thesis work are summarized. The development of advanced reaction systems for hydrogen rich mixtures production is the main objective. In addition, the use and comparison between two different reaction systems, (fixed bed reactor (FBR) and microreactor), the processing of renewable raw materials, the development of new, active, selective and stable catalytic formulations, and the optimization of the operating conditions were also established as additional partial objectives. Methane and natural gas (NG) steam reforming experimental results obtained when operated with microreactor and FBR systems are presented in Chapter 3. For these experiments nickel-based (Ni/Al2O3 and Ni/MgO) and noble metal-based (Pd/Al2O3 and Pt/Al2O3) catalysts were prepared by wet impregnation and their catalytic activity was measured at several temperatures, from 973 to 1073 K, different S/C ratios, from 1.0 to 2.0, and atmospheric pressure. The Weight Hourly Space Velocity (WHSV) was maintained constant in order to compare the catalytic activity in both reaction systems. The results obtained showed a better performance of the catalysts operating in microreactors. The Ni/MgO catalyst reached the highest hydrogen production yield at 1073 K and steam-to-carbon ratio (S/C) of 1.5 under Steam methane Reforming (SMR) conditions. In addition, this catalyst also showed good activity and stability under NG reforming at S/C=1.0 and 2.0. The Ni/Al2O3 catalyst also showed high activity and good stability and it was the catalyst reaching the highest methane conversion (72.9 %) and H2out/CH4in ratio (2.4) under SMR conditions at 1073 K and S/C=1.0. However, this catalyst suffered from deactivation when it was tested under NG reforming conditions. Regarding the activity measurements carried out with the noble metal-based catalysts in the microreactor systems, they suffered a very quick deactivation, probably because of the effects attributed to carbon deposition, which was detected by Scanning Electron Microscope (SEM). When the FBR was used no catalytic activity was measured with the catalysts under investigation, probably because they were operated at the same WHSV than the microreactors and these WHSVs were too high for FBR system. In Chapter 4 biogas reforming processes were studied. This chapter starts with an introduction explaining the properties of the biogas and the main production routes. Then, the experimental procedure carried out is detailed giving concrete information about the experimental set-up, defining the parameters measured, specifying the characteristics of the reactors used and describing the characterization techniques utilized. Each following section describes the results obtained from activity testing with the different catalysts prepared, which is subsequently summarized: Section 4.3: Biogas reforming processes using γ-Al2O3 based catalysts The activity results obtained by several Ni-based catalysts and a bimetallic Rh-Ni catalyst supported on magnesia or alumina modified with oxides like CeO2 and ZrO2 are presented in this section. In addition, an alumina-based commercial catalyst was tested in order to compare the activity results measured. Four different biogas reforming processes were studied using a FBR: dry reforming (DR), biogas steam reforming (BSR), biogas oxidative reforming (BOR) and tri-reforming (TR). For the BSR process different steam to carbon ratios (S/C) from 1.0 to 3.0, were tested. In the case of BOR process the oxygen-to-methane (O2/CH4) ratio was varied from 0.125 to 0.50. Finally, for TR processes different S/C ratios from 1.0 to 3.0, and O2/CH4 ratios of 0.25 and 0.50 were studied. Then, the catalysts which achieved high activity and stability were impregnated in a microreactor to explore the viability of process intensification. The operation with microreactors was carried out under the best experimental conditions measured in the FBR. In addition, the physicochemical characterization of the fresh and spent catalysts was carried out by Inductively Coupled Plasma Atomic Emission Spectroscopy (ICP-AES), N2 physisorption, H2 chemisorption, Temperature Programmed Reduction (TPR), SEM, X-ray Photoelectron Spectroscopy (XPS) and X-ray powder Diffraction (XRD). Operating with the FBR, conversions close to the ones predicted by thermodynamic calculations were obtained by most of the catalysts tested. The Rh-Ni/Ce-Al2O3 catalyst obtained the highest hydrogen production yield in DR. In BSR process, the Ni/Ce-Al2O3 catalyst achieved the best activity results operating at S/C=1.0. In the case of BOR process, the Ni/Ce-Zr-Al2O3 catalyst showed the highest reactants conversion values operating at O2/CH4=0.25. Finally, in the TR process the Rh-Ni/Ce-Al2O3 catalyst obtained the best results operating at S/C=1.0 and O2/CH4=0.25. Therefore, these three catalysts were selected to be coated onto microchannels in order to test its performance under BOR and TR processes conditions. Although the operation using microreactors was carried out under considerably higher WHSV, similar conversions and yields as the ones measured in FBR were measured. Furthermore, attending to other measurements like Turnover Frequency (TOF) and Hydrogen Productivity (PROD), the values calculated for the catalysts tested in microreactors were one order of magnitude higher. Thus, due to the low dispersion degree measured by H2-chemisorption, the Ni/Ce-Al2O3 catalyst reached the highest TOF and PROD values. Section 4.4: Biogas reforming processes using Zeolites L based catalysts In this section three type of L zeolites, with different morphology and size, were synthesized and used as catalyst support. Then, for each type of L zeolite three nickel monometallic and their homologous Rh-Ni bimetallic catalysts were prepared by the wetness impregnation method. These catalysts were tested using the FBR under DR process and different conditions of BSR (S/C ratio of 1.0 and 2.0), BOR (O2/CH4 ratio of 0.25 and 0.50) and TR processes (at S/C=1.0 and O2/CH4=0.25). The characterization of these catalysts was also carried out by using the same techniques mentioned in the previous section. Very high methane and carbon dioxide conversion values were measured for almost all the catalysts under investigation. The experimental results evidenced the better catalytic behavior of the bimetallic catalysts as compared to the monometallic ones. Comparing the catalysts behavior with regards to their morphology, for the BSR process the Disc catalysts were the most active ones at the lowest S/C ratio tested. On the contrary, the Cylindrical (30–60 nm) catalysts were more active under BOR conditions at O2/CH4=0.25 and TR processes. By the contrary, the Cylindrical (1–3 µm) catalysts showed the worst activity results for both processes. Section 4.5: Biogas reforming processes using Na+ and Cs+ doped Zeolites LTL based catalysts A method for the synthesis of Linde Type L (LTL) zeolite under microwave-assisted hydrothermal conditions and its behavior as a support for heterogeneously catalyzed hydrogen production is described in this section. Then, rhodium and nickel-based bimetallic catalysts were prepared in order to be tested by DR process and BOR process at O2/CH4=0.25. Moreover, the characterization of the catalysts under investigation was also carried out. Higher activities were achieved by the catalysts prepared from the non-doped zeolites, Rh-Ni/D and Rh-Ni/N, as compared to the ones supported on Na+ and Cs+ exchanged supports. However, the differences between them were not very significant. In addition, the Na+ and Cs+ incorporation affected mainly to the Disc catalysts. Comparing the results obtained by these catalysts with the ones studied in the section 4.4, in general worst results were achieved under DR conditions and almost the same results when operated under BOR conditions. In Chapter 5 the ethylene glycol (EG) as feed for syngas production by steam reforming (SR) and oxidative steam reforming (OSR) was studied by using microchannel reactors. The product composition was determined at a S/C of 4.0, reaction temperatures between 625°C and 725°C, atmospheric pressure and Volume Hourly Space Velocities (VHSV) between 100 and 300 NL/(gcath). This work was divided in two sections. The first one corresponds to the introduction of the main and most promising EG production routes. Then, the new experimental procedure is detailed and the information about the experimental set-up and the measured parameters is described. The characterization was carried out using the same techniques as for the previous chapter. Then, the next sections correspond to the catalytic activity and catalysts characterization results. Section 5.3: xRh-cm and xRh-np catalysts for ethylene glycol reforming Initially, catalysts with different rhodium loading, from 1.0 to 5.0 wt. %, and supported on α-Al2O3 were prepared by two different preparation methods (conventional impregnation and separate nanoparticle synthesis). Then, the catalysts were compared regarding their measured activity and selectivity, as well as the characterization results obtained before and after the activity tests carried out. The samples prepared by a conventional impregnation method showed generally higher activity compared to catalysts prepared from Rh nanoparticles. By-product formation of species such as acetaldehyde, ethane and ethylene was detected, regardless if oxygen was added to the feed or not. Among the catalysts tested, the 2.5Rh-cm catalyst was considered the best one. Section 5.4: 2.5Rh-cm catalyst support modification with CeO2 and La2O3 In this part of the Chapter 5, the catalyst showing the best performance in the previous section, the 2.5Rh-Al2O3 catalyst, was selected in order to be improved. Therefore, new Rh based catalysts were designed using α-Al2O3 and being modified this support with different contents of CeO2 or La2O3 oxides. All the catalysts containing additives showed complete conversion and selectivities close to the equilibrium in both SR and OSR processes. In addition, for these catalysts the concentrations measured for the C2H4, CH4, CH3CHO and C2H6 by-products were very low. Finally, the 2.5Rh-20Ce catalyst was selected according to its catalytic activity and characterization results in order to run a stability test, which lasted more than 115 hours under stable operation. The last chapter, Chapter 6, summarizes the main conclusions achieved throughout this Thesis work. Although very high reactant conversions and rich hydrogen mixtures were obtained using a fixed bed reaction system, the use of microreactors improves the key issues, heat and mass transfer limitations, through which the reforming reactions are intensified. Therefore, they seem to be a very interesting and promising alternative for process intensification and decentralized production for remote application.

Solutions for New Terrestrial Broadcasting Systems Offering Simultaneously Stationary and Mobile Services

221 p.

Hyers-Ulam-Rassias Stability of Functional Differential Systems with Point and Distributed Delays

This paper investigates stability and asymptotic properties of the error with respect to its nominal version of a nonlinear time-varying perturbed functional differential system subject to point, finite-distributed, and Volterra-type distributed delays associated with linear dynamics together with a class of nonlinear delayed dynamics. The boundedness of the error and its asymptotic convergence to zero are investigated with the results being obtained based on the Hyers-Ulam-Rassias analysis.

On Nonnegative Solutions of Fractional q-Linear Time-Varying Dynamic Systems with Delayed Dynamics

This paper is devoted to the investigation of nonnegative solutions and the stability and asymptotic properties of the solutions of fractional differential dynamic linear time-varying systems involving delayed dynamics with delays. The dynamic systems are described based on q-calculus and Caputo fractional derivatives on any order.

New generation of two-dimensional spintronic systems realized by coupling of Rashba and Dirac fermions

Intriguing phenomena and novel physics predicted for two-dimensional (2D) systems formed by electrons in Dirac or Rashba states motivate an active search for new materials or combinations of the already revealed ones. Being very promising ingredients in themselves, interplaying Dirac and Rashba systems can provide a base for next generation of spintronics devices, to a considerable extent, by mixing their striking properties or by improving technically significant characteristics of each other. Here, we demonstrate that in BiTeI@PbSb2Te4 composed of a BiTeI trilayer on top of the topological insulator (TI) PbSb2Te4 weakly- and strongly-coupled Dirac-Rashba hybrid systems are realized. The coupling strength depends on both interface hexagonal stacking and trilayer-stacking order. The weakly-coupled system can serve as a prototype to examine, e.g., plasmonic excitations, frictional drag, spin-polarized transport, and charge-spin separation effect in multilayer helical metals. In the strongly-coupled regime, within similar to 100 meV energy interval of the bulk TI projected bandgap a helical state substituting for the TI surface state appears. This new state is characterized by a larger momentum, similar velocity, and strong localization within BiTeI. We anticipate that our findings pave the way for designing a new type of spintronics devices based on Rashba-Dirac coupled systems.

Eurobalise-Train communication modelling to assess interferences in railway control signalling systems

The evolution of the railway sector depends, to a great extent, on the deployment of advanced railway signalling systems. These signalling systems are based on communication architectures that must cope with complex electromagnetical environments. This paper is outlined in the context of developing the necessary tools to allow the quick deployment of these signalling systems by contributing to an easier analysis of their behaviour under the effect of electromagnetical interferences. Specifically, this paper presents the modelling of the Eurobalise-train communication flow in a general purpose simulation tool. It is critical to guarantee this communication link since any lack of communication may lead to a stop of the train and availability problems. In order to model precisely this communication link we used real measurements done in a laboratory equipped with elements defined in the suitable subsets. Through the simulation study carried out, we obtained performance indicators of the physical layer such as the received power, SNR and BER. The modelling presented in this paper is a required step to be able to provide quality of service indicators related to perturbed scenarios.