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.

Apuntes sobre clasicismo y modernidad

Mª José García Soler ( editora).Anejos de VELEIA. Serie Minor nº 17

Variation in size of yellowfin tuna (Thunnus albacares) within individual purse-seine sets

ENGLISH:Length-frequency samples of yellowfin tuna from 276 individual purse-seine sets were examined. Evidence of schooling by size is presented. Yellowfin schooled with skipjack are smaller and more homogeneous in length than are yellowfin from pure schools. Yellowfin in schools associated with porpoise appear to be more variable in size than yellowfin from other types of schools. No relationship was found between the tonnage of yellowfin in a school and the mean length of the yellowfin. Despite the tendency to school by size, the size variation within individual schools was judged to be enough to complicate greatly any program of regulation aimed at maximizing the yield-per-recruit through increasing the minimum size of yellowfin at first capture. SPANISH: Fueron examinadas las muestras frecuencia-longitud de atún aleta amarilla, de 276 lances individuales de redes de cerco. Se presenta la evidencia de agrupación por tamaños. Los atunes aleta amarilla agrupados con barrilete, son más pequeños y más homogéneos en longitud, que los atunes aleta amarilla de cardúmenes puros. El atún aleta amarilla en cardúmenes asociados con delfines parece ser más variable en tamaño, que el atún aleta amarilla proveniente de otros tipos de cardúmenes. No se encontró relac¡'ón entre el tonelaje del atún aleta amarilla en un cardumen y la longitud media de esta especie. A pesar de la tendencia a agruparse por tamaño, se juzgó, que la variación de tamaño en cardúmenes individuales, sería suficiente para complicar grandemente cualquier programa de reglamentación, dirigido a obtener el máximo del rendimiento por recluta a través del incremento del tamaño mínimo del atún aleta amarilla en la primera captura.

Modelling rail corrugation with specific track parameters focusing on ballasted track and slab track

The objective of this paper is to compare 3 types of track (high performance ballasted track, STEDEF and AFTRAV) from the corrugation growth point of view. This work has considered different vehicle speeds and track radii, and the results have taken into account the four wheels of a bogie. These tracks have been studied using Finite Elements with Nastran-Patran and RACING, a tool developed in Matlab by the authors which estimates the corrugation growth tendency. The tracks are studied using the Finite Strip Method and the Periodic Structure Theory. Lateral and vertical receptances for track and vehicle have been obtained, as well as the corrugation growth functions. In the paper the tracks are ranked according to corrugation development.

Relaciones amorosas de pareja en las trayectorias vitales de las mujeres encarceladas

[ES]La tesis doctoral analiza las experiencias amorosas de pareja de mujeres encarceladas, con el doble objetivo de visibilizar a las mujeres presas en el ámbito de las ciencias sociales y de introducir las especificidades de las mujeres encarceladas en los debates sociológicos y feministas acerca del amor. Las escasas aproximaciones al amor entre las mujeres presas han tendido a explicar sus relaciones de pareja desde el concepto de “dependencia emocional”, que, como se muestra en la tesis, presenta dos debilidades básicas, de un lado la tendencia a la psicologización y patologización de cuestiones de claro sustrato social; de otro la homogeneización de experiencias que presentan gran diversidad. Otra debilidad de ciertos análisis sobre las mujeres presas y aquellas excluidas socialmente, es que se han basado en concepciones sexistas acerca de las mujeres transgresoras como “malas mujeres”, por considerar que no cumplen con las expectativas culturales y sociales asociadas a los supuestos atributos de género. Esta tesis doctoral adopta una epistemología basada en la crítica feminista que busca modelos analíticos alejados de los estereotipos y la estigmatización de las mujeres transgresoras. Desde una perspectiva metodológica cualitativa, el trabajo de campo fue desarrollado en la cárcel de Nanclares de Oca (País Vasco) durante el 2008. Desarrollé un trabajo etnográfico de observación participante y entrevistas en profundidad semiestructuradas que elaboraban información sobre aspectos relativos a sus trayectorias de vida (familia de origen, vivienda, empleo, nivel educativo, situación penal y penitenciaria, estado de salud, etc.) y sus experiencias amorosas de pareja. En mi análisis, he rastreado la diversidad y variabilidad de las experiencias amorosas de las mujeres presas, el impacto del encarcelamiento en sus trayectorias amorosas y en la configuración de su intimidad, los elementos que hacen para estas mujeres del amor un “cautiverio”, y al mismo tiempo, las estrategias “liberadoras” que despliegan en sus desarrollos afectivos. El amor puede constituir un cautiverio para las mujeres ya que favorece la acomodación a unos roles de género que definen a las mujeres como dependientes y carentes de libertad. Al mismo tiempo, el amor se puede entender como una “estrategia emocional”, una forma de superar las consecuencias del encierro y de lograr ciertos estándares de “normalización” social, en un contexto en que se encuentran excluidas socialmente y fuertemente estigmatizadas.

An Algebraic Preservation Theorem for Aleph-Zero Categorical Quantified Constraint Satisfaction

23 p. -- An extended abstract of this work appears in the proceedings of the 2012 ACM/IEEE Symposium on Logic in Computer Science

Role of G protein coupled inwardly rectifier K+ channels (GIRK) on the neurobiology depression

353 págs.

On the impact of independence of irrelevant alternatives: the case of two-person NTU games

On several classes of n-person NTU games that have at least one Shapley NTU value, Aumann characterized this solution by six axioms: Non-emptiness, efficiency, unanimity, scale covariance, conditional additivity, and independence of irrelevant alternatives (IIA). Each of the first five axioms is logically independent of the remaining axioms, and the logical independence of IIA is an open problem. We show that for n = 2 the first five axioms already characterize the Shapley NTU value, provided that the class of games is not further restricted. Moreover, we present an example of a solution that satisfies the first five axioms and violates IIA for two-person NTU games (N, V) with uniformly p-smooth V(N).

Multi-agent modelling for the simulation of a simple smart microgrid

The smart grid is a highly complex system that is being formed from the traditional power grid, adding new and sophisticated communication and control devices. This will enable integrating new elements for distributed power generation and also achieving an increasingly automated operation so for actions of the utilities as for customers. In order to model such systems a bottom-up method is followed, using only a few basic elements which are structured into two layers: a physical layer for the electrical power transmission, and one logical layer for element communication. A simple case study is presented to analyse the possibilities of simulation. It shows a microgrid model with dynamic load management and an integrated approach that can process both electrical and communication flows.

Horizontale Trennblätter in Trawls zur Verringerung von Discards in der Ostsee

A primary objective of the Common Fishery Policy of the European Union is the reduction of discards and unwanted by-catches in the fishery. In principle this could be achieved if the catching methods were optimised for this. Still high numbers of undersized flatfish are caught in the bottom trawls. Although EU regulations make the use of the BACOMA codend mandatory in the Baltic Sea cod areable to escape through square mesh escape window of the BACOMA net the whereas flatfish still remain in the cod-end. Gear experiments have been carried out with the aim to better separate cod from the flatfish fraction already when entering the rear belly, making use of the natural behaviour of the fish, i. e. the preferred swimming distance from the bottom of the net in the funnel. As cod have a natural tendency to keep a relativly great distance from the bottom, flatfish tend to stay close to it. It was attempted to separate both fractions by splitting the funnel into an upper and lower part with a horizontal panel. This wastested for two different nets, a cod trawl to separate cod from flatfish, and an eel-trawl to separate cod and flatfish from eel. Cod and flatfish separation is best at a panel distance of 50 cm from the bottom. Thus, 74 % of the cod were found in the upper panel, whereas 75 % of the flounder were in the lower section. A separation of eel from cod was however not possible, since eel tend to rise to the upper part of the net, together with cod.

Netzmaterial und Selektivität in der Ostseedorschfischerei

Since some time fishing gear scientists express their concern over an observed tendency of the commercial fishery to proceed from codend netting yarns of 3 to 4 mm to higher values or to switch to the use of double instead of single yarn. A recent large EU-financed project collected statistical evidence on the detrimental effect of such behaviour on the selectivity of the codends. In this context data on cod are very scarce. German-Polish experiments in the Baltic from 1999 to 2001 aimed at filling this gap. The investigations prove a clear evidence of a negativ ecorrelation between netting yarn diameter and selectivity factor and/or L50. In addition they demonstrate a clear negative effect on selectivity when switching from single to double yarn The effects are of an order of magnitude that counteracting effects as catch size are masked and support the decision of the IBSFC to define maximum yarn diameters both for single and double yarn netting. A measuring instrument for the enforcement of these new regulations was introduced right in time.

Die Lage der Fischbestände in Nordostatlantik, Nord- und Ostsee. Einschätzungen des Internationalen Rates für Meeresforschung im Frühjahr 2001

The spring session of ACFM gave advice for a number of stocks in the North Atlantic, North Sea and Baltic. The present assessment of the situation is given here for stocks of importance for the German fishery. These are: Blue Whiting: the stock size is rapidly decreasing due to high catches; ICES recommends a closure of the fishery. Herring (Atlanto-Scandian, Norwegian spring spawner): Stock is within save biological limits, weak recruitment of the recent years will lead to a further reduction of biomass. Herring (North Sea): revision of the assessment led to a different perception of the stock: SSB was in 2000 below Blim. Excellent recruitment will lead to an increase of SSB over Blim within this year, but ICES recommends to reduce fishing mortality on adults significantly. Herring (Baltic spring spawner in 22–24, IIIa): Still no increasing tendency is detectable. Herring (VIaNorth): stable. Redfish: generally further decreasing tendency observed, a reduction of the fishery is recommended. Signs of recovery visible only for two units. Greenland Halibut: State of the stock not quite clear, but slightly positive tendencies. The present fishing intensity should be reduced. Cod (Kattegat): Weak recruitment, outside safe biological limits. ICES recommends a closure of the fishery. Cod (22–24, Western Baltic): Stock situation unclear due to extensive migrations. F should be reduced by at least 10%.

Die lage der Fischbestände in Nordostatlantik, Nord- und Ostsee. Einschätzungen des Internationalen Rates für Meeresforschung im Frühjahr 2000

The spring session of ACFM gave advice for a number of stocks in the North Atlantic, North Sea and Baltic. The present assessment of the situation is given here for stocks of higher importance for the German fishery. These are: Blue Whiting: the stock is still relatively high, this, however, will not last very long, due to too intense fishing. Cod in Kattegat: stock is outside safe biological limits. No immediate recovery in sight. Cod in 22–24 (Baltic): stock is inside save biological limits. F, however, is above the recommendation of the IBSFC. Greenland Halibut: state of the stock not quite clear. The present fishing intensity seems to be sustainable. Herring (Atlanto- scandian, Norwegian spring spawner): stock is within safe biological limits, weak recruitment of the recent years will lead to a reduction of biomass. Herring: for Baltic spring spawner in 22–24 and IIIa still no increasing tendency detectable. North Sea Herring: further increasing tendency, with 900 000 t over B lim, good recruitment. Herring in VIa: stable. Redfish: generally decreasing tendency observed, a reduction of the fishery is recommended. Signs of recovery, however, visible for some units

Beurteilung der Fischbestände in Nordatlantik, Nord- und Ostsee. Einschätzung durch den Internationalen Rat für Meeresforschung vom Mai 1999

The spring session of ACFM gave advice for a number of stocks in the North Atlantic, North Sea and Baltic. The situation is given here for stocks of higher importance for the German fishery. These are: Blue Whiting: A short term upwards trend is observed, which, however, will not last very long, due to too intense fishing. Cod in Kattegat: Stock is outside safe biological limits. No immediate recovery in sight. Cod in Sub. Div. 22– 24 (Baltic): Stock is outside safe biological limits. Due to weak recruitment not immediate recovery in prospect. Greenland Halibut: Stock outside safe biological limits and still in downward trend. Herring (atlanto-scandian, Norw. spring spawner): Stock inside safe biological limits, weak recruitment of the past 5 years will, however, lead to a reduction of the biomass. Redfish: Generally decreasing tendency observed, a reduction of the fishery is recommended.

Generating artificial homologous proteins according to the representative family character in molecular mechanics properties - an attempt in validating an underlying rule of protein evolution

The molecular mechanics property is the foundation of many characters of proteins. Based on intramolecular hydrophobic force network, the representative family character underlying a protein’s mechanics property is described by a simple two-letter scheme. The tendency of a sequence to become a member of a protein family is scored according to this mathematical representation. Remote homologs of the WW-domain family could be easily designed using such a mechanistic signature of protein homology. Experimental validation showed that nearly all artificial homologs have the representative folding and bioactivity of their assigned family. Since the molecular mechanics property is the only consideration in this study, the results indicate its possible role in the generation of new members of a protein family during evolution.