294 research outputs found
A Generic Framework for Higher-Order Generalizations
No full textWe consider a generic framework for anti-unification of simply typed lambda terms. It helps to compute generalizations which contain maximally common top part of the input expressions, without nesting generalization variables. The rules of the corresponding anti-unification algorithm are formulated, and their soundness and termination are proved. The algorithm depends on a parameter which decides how to choose terms under generalization variables. Changing the particular values of the parameter, we obtained four new unitary variants of higher-order anti-unification and also showed how the already known pattern generalization fits into the schema
Unital Anti-Unification: Type and Algorithms
No full textUnital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete, and return tree grammars from which the set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions
Higher-Order Equational Pattern Anti-Unification [Preprint]
No full textWe consider anti-unification for simply typed lambda terms in associative,
commutative, and associative-commutative theories and develop a sound and
complete algorithm which takes two lambda terms and computes their
generalizations in the form of higher-order patterns. The problem is finitary:
the minimal complete set of generalizations contains finitely many elements. We
define the notion of optimal solution and investigate special fragments of the
problem for which the optimal solution can be computed in linear or polynomial
time.Comment: Submitted to FSCD 201
Role of the long non-coding RNA PVT1 in the dysregulation of the ceRNA-ceRNA network in human breast cancer
No full textRecent findings have identified competing endogenous RNAs (ceRNAs) as the drivers in many disease conditions, including cancers. The ceRNAs indirectly regulate each other by reducing the amount of microRNAs (miRNAs) available to target messenger RNAs (mRNAs). The ceRNA interactions mediated by miRNAs are modulated by a titration mechanism, i.e. large changes in the ceRNA expression levels either overcome, or relieve, the miRNA repression on competing RNAs; similarly, a very large miRNA overexpression may abolish competition. The ceRNAs are also called miRNA decoys or miRNA sponges and encompass different RNAs competing with each other to attract miRNAs for interactions: mRNA, long non-coding RNAs (lncRNAs), pseudogenes, or circular RNAs. Recently, we developed a computational method for identifying ceRNA-ceRNA interactions in breast invasive carcinoma. We were interested in unveiling which lncRNAs could exert the ceRNA activity. We found a drastic rewiring in the cross-talks between ceRNAs from the physiological to the pathological condition. The main actor of this dysregulated lncRNA-associated ceRNA network was the lncRNA PVT1, which revealed a net biding preference towards the miR-200 family members in normal breast tissues. Despite its up-regulation in breast cancer tissues, mimicked by the miR-200 family members, PVT1 stops working as ceRNA in the cancerous state. The specific conditions required for a ceRNA landscape to occur are still far from being determined. Here, we emphasized the importance of the relative concentration of the ceRNAs, and their related miRNAs. In particular, we focused on the withdrawal in breast cancer tissues of the PVT1 ceRNA activity and performed a gene expression and sequence analysis of its multiple isoforms. We found that the PVT1 isoform harbouring the binding site for a representative miRNA of the miR-200 family shows a drastic decrease in its relative concentration with respect to the miRNA abundance in breast cancer tissues, providing a plausibility argument to the breakdown of the sponge program orchestrated by the oncogene PVT1. © 2017 Conte et al. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited
Automated proof-checking of the Rose-Rosser's proof of completeness of Łukasiewicz propositional logic
No full textTato práce se zabývá formalizací základů Łukasiewiczovy logiky a strojovým ověřením větší části prvního známého důkazu její úplnosti, t.j. za prvé ověřením celkem 23 lemmat s rozsáhlými syntaktickými důkazy, za druhé formalizací pojmu polynomické formule a ověřením s tímto pojem spojených 16 vět. Práce popisuje hlavní body této formalizace- jedná se především o základní definice, obecné věty (např. pravidlo řezu) a implementace vlastních taktik pro automatické dokazování, např. taktiky pro automatické ověřování dlouhých syntaktických důkazů zmíněných lemmat. Formalizace je provedena v programovacím jazyce Lean a tento text je doprovázen ukázkami jak originálního kódu, tak někdy výhodnějšího pseudokódu.This thesis addresses formalisation of the basics of Łukasiewicz logic and automated verification of majority of the first known proof of its completeness, i.e. first verification of 23 lemmas with extensive syntactic proofs, second formalisation of the notion of polynomial formula and with verification of 16 theorems connected to this term. The text describes key moments of the formalisation - mainly basic definitions, general lemmas (e.g. cut rule) and implementation of own tactics for automated proving, e.g. a tactic for automated verification of long syntactic proofs of said lemmas. The formalisation is implemented in the Lean programming language. In this text it is demonstrated by pieces of original code as well as sometimes more useful pseudocode
Evaluation of cyclic behavior of dense sands under multidirectional loading using centrifuge tests
No full textThe seismic performance of nuclear power plant (NPP) structures constructed on compacted, coarse-grained soil depends on the soil’s cyclic shear stress – shear strain – volumetric strain response. NPPs founded on a thick deposit of dense coarse-grained soil may experience nontrivial settlements due to small, but accumulated volumetric strains during an earthquake. Studies that have investigated the seismic response of granular are primarily limited to unidirectional loading. However, since seismic events are multidirectional in nature, design based on unidirectional studies may lead to underestimation of vertical strains, and nontrivial settlements that can impact structures. While correlations to estimate vertical strains from drained and undrained cyclic element tests are available, they do not all explicitly incorporate multidirectional shaking. Moreover, typical drainage conditions in the field may be partially drained while shaking-induced vertical strains accumulate. This work forms a unique database of dynamic centrifuge “case-histories” that provide insight into the shear and volumetric response of dense coarse-grained soils under unidirectional and bidirectional loading under partially drained conditions. Dynamic centrifuge tests were performed on thick (up to 20m) layers of saturated dense Ottawa sand (D = 95%) with models representing both free-field and a soil-structure (near field) system excited using unidirectional and bidirectional historical broadband motions.
Free-field centrifuge experiments highlight that shear response in each orthogonal direction is not affected by multidirectionality. Thus, site shear response can be estimated for use in one-dimensional non-linear site response analysis. In contrast, centrifuge tests illustrated that volumetric strains (v) and excess porewater pressures (evaluated in terms of excess porewater pressure ratio, ru) are affected by multidirectionality irrespective of density, with the ratios of bidirectional to unidirectional v and ru ranging from 1 to 4. Consequently, multidirectional factors relationships for v and ru are proposed as a function of FSliq. Furthermore, Energy-based intensity measures (Arias and Housner intensities) provided nearly unique estimates of excess PWP and (v) for both 1D and 2D motions, indicating that they capture multi-directionality effects, while vectored peak accelerations and velocities (PGA and PGV) yielded different relationships for 1D and 2D motions.
A semi-empirical hyperbolic (GQ/H), simplified model based on ground motion intensity parameters (e.g., Housner Intensity), and shear wave velocity (Vs) is proposed to estimate vertical strains in dense coarse-grained soils under free field conditions. Comparison of GQ/H model predictions and estimates based on undrained cyclic shear tests indicated that the latter consistently overpredicts the measured settlements in the dense sand profiles. In contrast, the approach based on drained cyclic shear tests reasonably agrees with both measured settlements and GQ/H-v model. Further comparison of recorded near field settlements from centrifuge test data indicate that the (GQ/H) simplified free model underestimates settlements beneath the structures tested here.
Lastly, a semi-empirical near field model to estimate vertical strains beneath structures is proposed. This model also includes ground motion intensity measures to account for duration (e.g., Housner intensity) in conjunction with a rocking stiffness parameter (originally proposed by Gazetas 1991) derived from shear wave velocity Vs. The vertical strain model requires estimates of Housner Intensity by means of nonlinear site response analysis. The proposed vertical strain models reasonably capture free field and near field settlements on dense sands recorded in dynamic centrifuge tests.
The aforementioned two semi-empirical models are used in conjunction to estimate settlements of structures founded primarily on dense sands during shaking.Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2020-05-01The student, Alfonso Cerna Diaz, accepted the attached license on 2018-04-17 at 14:57.The student, Alfonso Cerna Diaz, submitted this Dissertation for approval on 2018-04-17 at 15:02.This Dissertation was approved for publication on 2018-04-20 at 08:15.DSpace SAF Submission Ingestion Package generated from Vireo submission #12217 on 2018-08-31 at 17:27:46Made available in DSpace on 2018-09-04T20:47:11Z (GMT). No. of bitstreams: 2
CERNADIAZ-DISSERTATION-2018.pdf: 400424153 bytes, checksum: 51a3c637a92352093c0bd8ee96814f70 (MD5)
LICENSE.txt: 4215 bytes, checksum: ad45976d421b042f624c488e2d34df7c (MD5)
Previous issue date: 2018-04-20Embargo set by: Seth Robbins for item 107391
Lift date: 2020-09-04T20:47:38Z
Reason: Author requested closed access (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 107391
Lift date: 2020-09-04T20:50:11Z
Reason: Author requested closed access (OA after 2yrs) in Vireo ETD systemLimited Restriction Lifted for Item 107391 on 2020-09-05T09:15:20Z
New town hall for the district Brno-North
No full textThe building is situated into new urban structure with a simple grid of regular blocks and streets in Cerna Pole, Brno Sever. It is designed as a solitaire which enters the park with a half of his platform. The house is sunk into the ground and his parter is interestingly and playfully communicating surrounding. House was created from a modified block as inversion of its mass. The house can be entered from both sides. From the north side and from the south side. Matter is 21m high and has a and spans 42 x 49.5 m. The key element of the plan and the communication is hinged open staircase in the hall
New town hall for the district Brno-North
No full textThe building is situated into new urban structure with a simple grid of regular blocks and streets in Cerna Pole, Brno Sever. It is designed as a solitaire which enters the park with a half of his platform. The house is sunk into the ground and his parter is interestingly and playfully communicating surrounding. House was created from a modified block as inversion of its mass. The house can be entered from both sides. From the north side and from the south side. Matter is 21m high and has a and spans 42 x 49.5 m. The key element of the plan and the communication is hinged open staircase in the hall
Evaluación de las patologías del concreto del cerco perimétrico de la Institución Educativa Fe y Alegría N° 16, Chimbote – 2021
No full textEl problema de esta investigación fue: ¿Cuál es el resultado de la evaluación de las
patologías del concreto del cerco perimétrico de la Institución Educativa Fe y Alegría
N° 16, Chimbote - 2021?, para resolver esto nos planteamos como objetivo general,
Evaluar las patologías del concreto del cerco perimétrico de la Institución Educativa N°
16, Chimbote – 2021. La metodología de trabajo es del tipo aplicada, descriptivo de
diseño no experimental y explicativo. El Universo está dado por la delimitación
Geográfica de la Institución Educativa, con un área total de 18000.07 m². Así mismo
para la población y muestra está compuesta por una longitud total de 562.76 ml,
obteniendo 25 unidades de muestra. Teniendo como variable las patologías del
concreto, utilizando la técnica de la observación y de análisis documental, se empleará
fichas técnicas para la recolección de datos y de laboratorio. Se logró obtener como
resultados el porcentaje total del área afectada en las unidades de muestra, siendo
311.60 m2 (16.22%) el porcentaje de afectación total y 1609.77 m2 (83.78%) el
porcentaje total sin afectación, con la presencia de elementos estructurales como los
muros 293.07 m2 (17.98%), las columnas 13.95 m2 (10.19%), las vigas 4.58 m2
(2.97%) de afectación
What drives innovation in nuclear reactors technologies? An empirical study based on patent counts.
No full textThis paper examines the evolution of innovation in nuclear power reactors between 1974 and 2008 in twelve OECD countries and assesses to what extent nuclear innovation has been driven by economic incentives, political decisions and safety regulation considerations. We use priority patent applications related to Nuclear Power Plants (NPPs) as a proxy for innovating activity. Our results highlight that nuclear innovation is partly driven by the conventional paradigm where both demandpull, measured by NPPs constructions in the innovating country and in the rest of the world, and technology-push, measured by Research and Development (R&D) expenditures specific to NPPs, have a positive and significant impact on innovation. Our results also evidence that the impact of public R&D expenditures and national NPPs construction on innovation is stronger when the quality of innovation, measured by forward patent citations, is taken into account, and have a long run positive impact on innovation through the stock of knowledge available to innovators. In contrast, we show that political decisions following the Three Miles Island and Chernobyl nuclear accidents, measured by NPPs cancellations, have a negative impact on nuclear innovation. Finally, we find that the nuclear safety authority has an ambivalent effect on innovation. On one hand, regulatory inspections have a positive impact on innovation, one the other hand, regulatory decisions to temporarily close a NPP have an adverse impact on innovation.Innovation; nuclear reactors; nuclear safety regulation; nuclear development
- …
