1,397 research outputs found
A First Order Theory of Diagram Chasing
No full textThis paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers
Detection of Wet Riparian Areas using Very High Resolution Multispectral UAS Imagery Based on a Feature-based Machine Learning Algorithm
No full textUnmanned Aerial System (UAS) imagery has
enabled very high-resolution multispectral image
acquisition. Detection of wet areas and classification of
land cover based on these images using the Machine
Learning (ML) algorithm named Random Forest (RF) is
our main purpose in this paper. Very high-resolution UAS
images have been used as inputs for a machine learner to
access the capability of different spectral bands and
spectral vegetation indices, elevation, and texture features
in the classification of land cover and detection of the wet
riparian area in the case study in two different epochs.
There are many existing methods for the classification of
land cover based on UAS images, but very high-resolution
centimeter-level data are of main importance in this
analysis. Outstanding results have been produced in both
epochs considering three extremely accurate performance
analysers. Additionally, in this research, the most decisive
and effective features have been discovered to
compromise accuracy and the number of effectual
features
Gardening with the Pythia A Model of Continuity in a Dependent Setting
No full textWe generalize to a rich dependent type theory a proof originally developed by Escardó that all System functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (ℕ → ℕ) → ℕ is externally continuous
Provenance of the Oligo-Miocene Zivah Formation, NW Iran, assessed using heavy mineral assemblage, detrital clinopyroxene and detrital apatite geochemistry
No full textHeavy mineral analysis and geochemical analysis of detrital clinopyroxene and apatite have been used to determine provenance and tectonic setting of the Oligocene-Miocene Zivah Formation, in three outcrop sections from the Moghan area in northwest Iran. The composition of assemblages from the Zivah sandstones have a majority of clinopyroxene, apatite, biotite and opaque minerals with
minor amounts of hornblende, zircon, garnet and epidote. The abundance of a mafic heavy-mineral suite such as clinopyroxene relative to metamorphic and felsic heavy mineral suites such as epidote, garnet and zircon indicates a convergent tectonic setting. Geochemistry of detrital clinopyroxenes from the Zivah Formation also indicates that these detrital grains probably crystallized from calk-alkaline magmas. They also show orogenic tectonic setting at the time of Zivah deposition. This is consistent with the derivation of these sediments from areas with
calc-alkaline volcanic rocks like Talysh and Lesser Caucasus as a result of Caucasus orogeny. Compositions of detrital apatites of the Zivah Formation are also consistent with the widespread distribution of unfractionated (mafic / intermediate) volcanic rocks of both alkaline and calc-alkaline composition in the Lesser Caucasus and Talysh
Melissa officinalis and rosmarinic acid in management of memory functions and Alzheimer disease
No full textAlzheimer disease (AD) as worldwide progressive neurodegenerative disease is prevalent disease among elderly population. Due to limitation in chemical drugs along with their adverse effects of these treatments, research for finding more effective natural drugs, is one of interesting subjects among the scientists. Melissa officinalis (M. officinalis) has a long history of use in treatment of nervous system diseases. This review article evaluates the potency of M. officinalis in treatment of AD by review of experimental and clinical documents on the efficacy, safety and its mechanisms of action in management of AD. The information is extracted from electronic resources (PubMed, Wiley, Springer and Science Direct), English and Persian scientific books. In spite of different scientific and non-scientific reports on the use of M. officinalis and its main component of rosmarinic acid in neurodegenerative diseases, there is only one clinical trial on the efficacy of M. officinalis ethanol extract in management of AD. Different mechanisms of action for M. officinalis, including inhibitory effects against amyloid beta, reactive oxygen species, and acetylcholine esterase, are involved. Larger clinical trials are recommended to confirm the efficacy and safety of M. officinalis extracts in treatment of AD patients
Machine-Checked Categorical Diagrammatic Reasoning
No full textThis paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature
Programming and certifying a CAD algorithm in the Coq system
No full textInternational audienceA. Tarski has shown in 1948 that one can perform quantifier elimination in the theory of real closed fields. The introduction of the Cylindrical Algebraic Decomposition (CAD) method has later allowed to design rather feasible algorithms. Our aim is to program a reflectional decision procedure for the Coq system, using the CAD, to decide whether a (possibly multivariate) system of polynomial inequalities with rational coefficients has a solution or not. We have therefore implemented various computer algebra tools like gcd computations, subresultant polynomial or Bernstein polynomials
Genetic analysis of novel resistance sources and genome-wide association mapping identified novel QTLs for resistance to Zymoseptoria tritici, the causal agent of septoria tritici blotch in wheat
No full textSeptoria tritici blotch (STB) caused by Zymoseptoria tritici is one of the most important foliar diseases of wheat causing significant yield losses worldwide. In this study, a panel of bread wheat genotypes comprised 185 globally diverse genotypes were tested against 10 Z. tritici isolates at the seedling stage. Genome-wide association study (GWAS) using high-throughput DArTseq markers was performed and further gene expression analysis of significant markers trait association (MTAs) associated with resistance to STB was analyzed. Disease severity level showed significant differences among wheat genotypes for resistance to different Z. tritici isolates. We found novel landrace genotypes that showed highly resistance spectra to all tested isolates. GWAS analysis resulted in 19 quantitative trait loci (QTLs) for resistance to STB that were located on 14 chromosomes. Overall, 14 QTLs were overlapped with previously known QTLs or resistance genes, as well as five potentially novel QTLs on chromosomes 1A, 4A, 5B, 5D, and 6D. Identified novel resistance sources and also novel QTLs for resistance to different Z. tritici isolates can be used for gene pyramiding and development of durable resistance cultivars in future wheat breeding programs
Microfiltration and ultrafiltration as efficient, sustainable pretreatment technologies for resource recovery
No full textUn approccio ecologico all'interazione fra nativi e islamici in una realtà del Sud
No full textIl lavoro ha avuto lo scopo di evidenziare gli aspetti che contribuiscono a mantenere le difficoltà e le dimensioni che sono di ostacolo o di risorsa nel processo di interazione tra italiani e immigrati entro specifici contesti di vita sociale e politica al fine di comprendere l'orientamento al riconoscimento reciproco e dunque all'azione integrativa.In relazione a tali obiettivi si è fatto riferimento al modello ecologico che dà rilievo all'interazione tra i diversi fattori e livelli che costituiscono la realtà sociale entro la quale si costruiscono i significati delle azioni individuali, di gruppo e collettive (Brofenbrenner, 1979;Prilleltensky, 2008; Christens & Perkins, 2008). In tal senso il processo di integrazione nella comunità locale è il risultato dell'influenza del contesto, delle reti sociali e delle caratteristiche personali e di gruppo oltre che delle effettive risorse relazionali e materiali usufruibili da parte dei soggetti facenti parte di una comunità (Garcia, 2007; Nelson & Prilleltensky, 2005). Pertanto situazioni di marginalizzazione, di separazione dalla propria cultura di origine diviene la risposta di possibile benessere (Luque-Ribelles et al., 2008). Attraverso tale prospettiva presentiamo uno studio volto a cogliere le dinamiche di reciproco riconoscimento tra residenti e migranti marocchini in una comunità territoriale ove vi è la presenza di immigrati marocchini e di contesti associativi entro i quali è possibile l'interazione tra italiani e marocchini. A tal fine è stato avviata una ricerca partecipata per cogliere i significati attribuiti alle esperienze dei singoli nel confronto con un'analisi strutturale, relazionale, culturale e socioeconomica della specifica realtà territoriale. Sono stati condotti gruppi di lavoro, effettuata l'analisi di comunità ed interviste semistrutturate con italiani e marocchini residenti nella stessa area. I risultati dell'analisi del materiale testuale e dei dati rilevati saranno discussi ponendo attenzione su alcuni aspetti, apparentemente impliciti del lavoro di ricerca sul campo, che sono invece i punti di forza di un approccio qualitativo allo studio dell'integrazione in specifici contesti sociali
- …
