Tactics for mechanized reasoning: a commentary on Milner (1984) 'The use of machines to assist in rigorous proof'.
Ontology highlight
ABSTRACT:
SUBMITTER: Gordon MJ
PROVIDER: S-EPMC4360087 | biostudies-other | 2015 Apr
REPOSITORIES: biostudies-other
Similar Datasets
Project description:The history of science is filled with examples of key discoveries and breakthroughs that have been published as landmark texts or journal papers, and to which one can trace the origins of whole disciplines. Such paradigm-shifting publications include Copernicus' De revolutionibus orbium coelestium (1543), Isaac Newton's Philosophiæ Naturalis Principia Mathematica (1687) and Albert Einstein's papers on relativity (1905 and 1915). Michael Faraday's 1832 paper on electromagnetic induction sits proudly among these works and in a sense can be regarded as having an almost immediate effect in transforming our world in a very real sense more than any of the others listed. Here we review the status of the subject-the relationship between magnetism and electricity both before and after Faraday's paper and delve into the details of the key experiments he carried out at the Royal Institution outlining clearly how he discovered the process of electromagnetic induction, whereby an electric current could be induced to flow through a conductor that experiences a changing magnetic field. His ideas would not only enable Maxwell's later development of his theory of classical electromagnetism, but would directly lead to the development of the electric dynamo and electric motor, two technological advances that are the very foundations of the modern world. This commentary was written to celebrate the 350th anniversary of the journal Philosophical Transactions of the Royal Society.
| S-EPMC4360079 | biostudies-other
Project description:Accumulation of aggregation-prone misfolded proteins disrupts normal cellular function and promotes ageing and disease. Bacteria, fungi and plants counteract this by solubilizing and refolding aggregated proteins via a powerful cytosolic ATP-dependent bichaperone system, comprising the AAA+ disaggregase Hsp100 and the Hsp70-Hsp40 system. Metazoa, however, lack Hsp100 disaggregases. We show that instead the Hsp110 member of the Hsp70 superfamily remodels the human Hsp70-Hsp40 system to efficiently disaggregate and refold aggregates of heat and chemically denatured proteins in vitro and in cell extracts. This Hsp110 effect relies on nucleotide exchange, not on ATPase activity, implying ATP-driven chaperoning is not required. Knock-down of nematode Caenorhabditis elegans Hsp110, but not an unrelated nucleotide exchange factor, compromises dissolution of heat-induced protein aggregates and severely shortens lifespan after heat shock. We conclude that in metazoa, Hsp70-Hsp40 powered by Hsp110 nucleotide exchange represents the crucial disaggregation machinery that reestablishes protein homeostasis to counteract protein unfolding stress.
| S-EPMC3492728 | biostudies-literature
Project description:Approximately 1.5 million neonates receive general anesthesia each year for a surgical procedure. Despite this being an essential practice, a number of recent studies now indicate that anesthetic exposure could cause toxicity and neuronal apoptosis in the developing brain. This could potentially influence long-term neurodevelopmental outcome, especially premature infants in need of multiple surgical procedures. Most anesthetic drugs routinely administered to neonates have not been adequately tested for safety or efficacy. Given the number of confounders, dosing is often extrapolated from adults. This is concerning since many different drugs can be administered concurrently, with few of these agents actually approved for use by the Food and Drug Administration. Since 1997, legislation has been passed in the United States and abroad encouraging more drug investigation in infants and children. This has resulted in over 500 labeling changes to products regarding safety and efficacy in various pediatric age groups. However, only three drugs routinely used as anesthetic agents in newborn infants have had any updated labeling (none in very premature infants). This "off-label" use without adequate testing must be addressed. Therefore, more clinical trials of common anesthetic agents used alone and in combination in neonates are urgently needed.
| S-EPMC4471569 | biostudies-other
Project description: Not available
| S-EPMC8311498 | biostudies-literature
Project description:IntroductionUromodulin (UMOD) is a glycoprotein expressed by the epithelial cells of the thick ascending limb of Henle's loop in the kidney. Research has shown that increased uromodulin expression may be associated with lower risk of cardiovascular disease in adults. Utilizing the Blood and Clot Thrombectomy Registry and Collaboration (BACTRAC) (clinicaltrials.gov NCT03153683), a continuously enrolling tissue bank, we aimed to examine the associations between serum uromodulin, age, and high BMI (BMI>25) and its relationship to stroke in patients.MethodsArterial blood distal and proximal to the thrombus was collected during a thrombectomy procedure using the BACTRAC protocol and sent to Olink (Boston, MA) to determine proteomic expression via proximity extension assay. Uromodulin expression was recorded and analyzed using two tailed T-tests and linear regressions.ResultsThe relationship between systemic and intracranial uromodulin, age, high BMI and hypertension were assessed. Systemic and intracranial uromodulin decreased with age (p<0.0001 and r2=0.343, p=0.0416 and r2=0.102) respectively. Systemic uromodulin expression increased with BMI>25 (p=0.014). Presence of hypertension decreased uromodulin's expression systemically (p=0.018) and intracranially (p=0.007).ConclusionsUromodulin was increased significantly in overweight patients, decreased significantly in older patients, and decreased in patients with hypertension. The increase in uromodulin in people with high BMI could be a protective reaction of the kidney to worsening conditions that make ischemic stroke more likely, with a goal of delaying dangerous outcomes. The decreased expression of uromodulin in older adults could be associated with the decline of general kidney function that accompanies aging. Hypertension can contribute to an AKI by decreasing perfusion to the kidney, therefore decreasing kidney function and uromodulin production. Further analyses are needed to understand the role of uromodulin following ischemic stroke.
| S-EPMC7990290 | biostudies-literature
Project description: Not available
| S-EPMC10689906 | biostudies-literature
Project description:Classifications and phylogenetic inferences of organismal groups change in light of new insights. Over time these changes can result in an imperfect tracking of taxonomic perspectives through the re-/use of Code-compliant or informal names. To mitigate these limitations, we introduce a novel approach for aligning taxonomies through the interaction of human experts and logic reasoners. We explore the performance of this approach with the Perelleschus use case of Franz & Cardona-Duque (2013). The use case includes six taxonomies published from 1936 to 2013, 54 taxonomic concepts (i.e., circumscriptions of names individuated according to their respective source publications), and 75 expert-asserted Region Connection Calculus articulations (e.g., congruence, proper inclusion, overlap, or exclusion). An Open Source reasoning toolkit is used to analyze 13 paired Perelleschus taxonomy alignments under heterogeneous constraints and interpretations. The reasoning workflow optimizes the logical consistency and expressiveness of the input and infers the set of maximally informative relations among the entailed taxonomic concepts. The latter are then used to produce merge visualizations that represent all congruent and non-congruent taxonomic elements among the aligned input trees. In this small use case with 6-53 input concepts per alignment, the information gained through the reasoning process is on average one order of magnitude greater than in the input. The approach offers scalable solutions for tracking provenance among succeeding taxonomic perspectives that may have differential biases in naming conventions, phylogenetic resolution, ingroup and outgroup sampling, or ostensive (member-referencing) versus intensional (property-referencing) concepts and articulations.
| S-EPMC4336294 | biostudies-literature
Project description:China's fast economic growth contributes to the rapid development of its urbanization process, and also renders a series of industrial accidents, which often cause loss of life, damage to property and environment, thus requiring the associated risk analysis and safety control measures to be implemented in advance. However, incompleteness of historical failure data before the occurrence of accidents makes it difficult to use traditional risk analysis approaches such as probabilistic risk analysis in many cases. This paper aims to develop a new methodology capable of assessing regional industrial safety (RIS) in an uncertain environment. A hierarchical structure for modelling the risks influencing RIS is first constructed. The hybrid of evidential reasoning (ER) and Analytical Hierarchy Process (AHP) is then used to assess the risks in a complementary way, in which AHP is hired to evaluate the weight of each risk factor and ER is employed to synthesise the safety evaluations of the investigated region(s) against the risk factors from the bottom to the top level in the hierarchy. The successful application of the hybrid approach in a real case analysis of RIS in several major districts of Beijing (capital of China) demonstrates its feasibility as well as provides risk analysts and safety engineers with useful insights on effective solutions to comprehensive risk assessment of RIS in metropolitan cities. The contribution of this paper is made by the findings on the comparison of risk levels of RIS at different regions against various risk factors so that best practices from the good performer(s) can be used to improve the safety of the others.
| S-EPMC5993124 | biostudies-literature
Project description:BackgroundA recent commentary has been published on our meta-analysis, which investigated substrate oxidation during exercise matched for relative intensities in hypoxia compared with normoxia. Within this commentary, the authors proposed that exercise matched for absolute intensities in hypoxia compared with normoxia, should have been included within the analysis, as this model provides a more suitable experimental design when considering nutritional interventions in hypoxia.Main bodyWithin this response, we provide a rationale for the use of exercise matched for relative intensities in hypoxia compared with normoxia. Specifically, we argue that this model provides a physiological stimulus replicable of real world situations, by reducing the absolute workload undertaken in hypoxia. Further, the use of exercise matched for relative intensities isolates the metabolic response to hypoxia, rather than the increased relative exercise intensity experienced in hypoxia when utilising exercise matched for absolute intensities. In addition, we also report previously unpublished data analysed at the time of the original meta-analysis, assessing substrate oxidation during exercise matched for absolute intensities in hypoxia compared with normoxia.ConclusionAn increased reliance on carbohydrate oxidation was observed during exercise matched for absolute intensities in hypoxia compared with normoxia. These data now provide a comparable dataset for the use of researchers and practitioners alike in the design of nutritional interventions for relevant populations.
| S-EPMC6924012 | biostudies-literature
Project description:BackgroundEmerging reports suggest the potential for adverse health effects from exposure to emissions from some additive manufacturing (AM) processes. There is a paucity of real-world data on emissions from AM machines in industrial workplaces and personal exposures among AM operators.MethodsAirborne particle and organic chemical emissions and personal exposures were characterized using real-time and time-integrated sampling techniques in four manufacturing facilities using industrial-scale material extrusion and material jetting AM processes.ResultsUsing a condensation nuclei counter, number-based particle emission rates (ERs) (number/min) from material extrusion AM machines ranged from 4.1 × 1010 (Ultem filament) to 2.2 × 1011 [acrylonitrile butadiene styrene and polycarbonate filaments). For these same machines, total volatile organic compound ERs (μg/min) ranged from 1.9 × 104 (acrylonitrile butadiene styrene and polycarbonate) to 9.4 × 104 (Ultem). For the material jetting machines, the number-based particle ER was higher when the lid was open (2.3 × 1010 number/min) than when the lid was closed (1.5-5.5 × 109 number/min); total volatile organic compound ERs were similar regardless of the lid position. Low levels of acetone, benzene, toluene, and m,p-xylene were common to both AM processes. Carbonyl compounds were detected; however, none were specifically attributed to the AM processes. Personal exposures to metals (aluminum and iron) and eight volatile organic compounds were all below National Institute for Occupational Safety and Health (NIOSH)-recommended exposure levels.ConclusionIndustrial-scale AM machines using thermoplastics and resins released particles and organic vapors into workplace air. More research is needed to understand factors influencing real-world industrial-scale AM process emissions and exposures.
| S-EPMC6598813 | biostudies-literature