bluuebunny/crossref_metadata_2025 huggingface dataset:
Strong Tough Poly Acrylic‐co‐acrylamide Hydrogels via a Synergistic Effect of Fiber and Metal‐Ligand Bonds as Flexible Strain Sensors
Authors: Xiao Longya , Ou Chengjian , Zhang Ding , Ma Yi , Xu Zefeng , Zhou Yitong , Jiang Hongjie
Published: August 2022

Developing conductive hydrogel‐incorporated strain sensors with high gauge factor (GF) and toughness for wearable applications is challenging. Herein, a facile strategy to fabricate strong, tough polyacrylamide‐co‐acrylic acid [P(AAm‐co‐AAc)] hydrogels via the synergy of fiber and metal‐ligand bonds is proposed. Through the secondary equilibrium approach, the pristine P(AAm‐co‐AAc) gel network is reconstructed with fiber and carboxyl–Zr4+ (Zirconium ion) coordination bonds intertwined over the entire gel matrix, generating a synergistic reinforcement in mechanical properties. The resultant hydrogels display a maximum tensile strength of 8.50 MPa and a fracture energy of 2.75 kJ m−2, which is 1–2 orders of magnitude greater than the original P(AAm‐co‐AAc) gels. It is also experimentally approved that by selecting different natural fibers, multivalent metal ions, and synthetic macromolecules containing carboxyl groups, the proposed approach is effective and can be generalized to fabricate strong, tough gels. Additionally, the electrical properties of obtained gel are evaluated by fabricating it into a stretchable strain sensor for object identification or human motion detection. The results reveal a high GF of 5.07 under a strain smaller 55%. These hydrogels are expected to enable numerous applications in soft robotics or wearable healthcare.
Revisiting power messaging in service failures: Pitfalls and proposed solutions
Authors: Antonetti Paolo , Crisafulli Benedetta
Published: August 2022

Past research shows that company messaging can inflate consumers' feelings of power, which in turn alleviate the negative effects of service failures. Extant research, however, has not examined how various types of power messaging can have a differential effect on consumers, with some leading to counterproductive consequences for companies. Across five experiments, we show that power messaging stressing that consumers have power over the company can backfire by increasing manipulative intent. Power messaging communicating that consumers will obtain a power boost from the service is more acceptable and less likely to be perceived as manipulative. Furthermore, we demonstrate that messaging eliciting power from the service is most effective when (1) targeted at consumers with low levels of skepticism, (2) delivered by an underdog brand, and (3) paired with co‐created recovery. Following a service failure, messaging communicating how customers will gain a power boost from the service experience increases identification with underdog brands. Our examination of power messaging as an overt communication strategy contributes to the literature on service failure and recovery. The research advances knowledge of the potential pitfalls of power messaging while proposing strategies to overcome risks associated with this communication strategy.
Inflammatory pathways in COVID‐19: Mechanism and therapeutic interventions
Authors: Jiang Yujie , Zhao Tingmei , Zhou Xueyan , Xiang Yu , Gutierrez‐Castrellon Pedro , Ma Xuelei
Published: August 2022

The 2019 coronavirus disease (COVID‐19) pandemic has become a global crisis. In the immunopathogenesis of COVID‐19, SARS‐CoV‐2 infection induces an excessive inflammatory response in patients, causing an inflammatory cytokine storm in severe cases. Cytokine storm leads to acute respiratory distress syndrome, pulmonary and other multiorgan failure, which is an important cause of COVID‐19 progression and even death. Among them, activation of inflammatory pathways is a major factor in generating cytokine storms and causing dysregulated immune responses, which is closely related to the severity of viral infection. Therefore, elucidation of the inflammatory signaling pathway of SARS‐CoV‐2 is important in providing otential therapeutic targets and treatment strategies against COVID‐19. Here, we discuss the major inflammatory pathways in the pathogenesis of COVID‐19, including induction, function, and downstream signaling, as well as existing and potential interventions targeting these cytokines or related signaling pathways. We believe that a comprehensive understanding of the regulatory pathways of COVID‐19 immune dysregulation and inflammation will help develop better clinical therapy strategies to effectively control inflammatory diseases, such as COVID‐19.
Association of MMP1 and MMP3 haplotypes with myocardial infarction and echocardiographic parameters of the left ventricle
Authors: Djuric Tamara , Kuveljic Jovana , Djordjevic Ana , Dekleva Milica , Stankovic Goran , Stankovic Aleksandra , Zivkovic Maja
Published: August 2022

Background

Myocardial infarction (MI) leads to ischemia and afterward to left ventricular (LV) remodeling. Matrix metalloproteinase−1 (MMP1) and −3 (MMP3) belong to the family of endopeptidases and together they can dissolve most of the components of the extracellular matrix. MMP1 and MMP3 variants have been investigated solely in association with ischemic heart disease and LV dysfunction, but not in haplotype. The aims of this study were to investigate the association of haplotypes inferred from MMP1 rs1799750 (−1607 1G/2G; NC_000011.9:g.102670497del) and MMP3 rs35068180 (−1612 5A/6A; NC_000011.9:g.102715952dup) with MI and their effect on the change in echocardiographic parameters of LV structure and function in patients within 6 months after MI.

Methods

The study included 325 patients with the first MI and 283 healthy controls. Gene variants were detected by PCR‐RFLP method. Parameters of LV structure and function were assessed by conventional 2D echocardiography, 3–5 days and 6 months after the first MI, on a subgroup of 160 patients. Haplotype analysis was performed with Thesias software.

Results

Haplotypes 2G‐5A and 1G‐6A were significantly and independently associated with MI compared with the reference haplotype 2G‐6A (adjusted, p = 0.009 and p = 0.026, respectively). After Bonferroni correction for multiple testing, MMP1 and MMP3 haplotypes lost their association with the change in LV long diameter and stroke volume within 6 months after MI.

Conclusion

MMP1 and MMP3 haplotypes are strongly associated with MI. Further studies are needed to validate this result and to examine their association with echocardiographic parameters of LV structure and function after MI.
Time–restricted eating alters the 24‐hour profile of adipose tissue transcriptome in men with obesity
Authors: Zhao Lijun , Hutchison Amy T. , Liu Bo , Wittert Gary A. , Thompson Campbell H. , Nguyen Leanne , Au John , Vincent Andrew , Manoogian Emily N. C. , Le Hiep D. , Williams April E. , Banks Siobhan , Panda Satchidananda , Heilbronn Leonie K.
Published: August 2022

Objective

Time‐restricted eating (TRE) restores circadian rhythms in mice, but the evidence to support this in humans is limited. The objective of this study was to investigate the effects of TRE on 24‐hour profiles of plasma metabolites, glucoregulatory hormones, and the subcutaneous adipose tissue (SAT) transcriptome in humans.

Methods

Men (n = 15, age = 63 [4] years, BMI 30.5 [2.4] kg/m2) were recruited. A 35‐hour metabolic ward stay was conducted at baseline and after 8 weeks of 10‐hour TRE. Assessment included 24‐hour profiles of plasma glucose, nonesterified fatty acid (NEFA), triglyceride, glucoregulatory hormones, and the SAT transcriptome. Dim light melatonin onset and cortisol area under the curve were calculated.

Results

TRE did not alter dim light melatonin onset but reduced morning cortisol area under the curve. TRE altered 24‐hour profiles of insulin, NEFA, triglyceride, and glucose‐dependent insulinotropic peptide and increased transcripts of circadian locomotor output cycles protein kaput (CLOCK) and nuclear receptor subfamily 1 group D member 2 (NR1D2) and decreased period circadian regulator 1 (PER1) and nuclear receptor subfamily 1 group D member 1 (NR1D1) at 12:00 am. The rhythmicity of 450 genes was altered by TRE, which enriched in transcripts for transcription corepressor activity, DNA‐binding transcription factor binding, regulation of chromatin organization, and small GTPase binding pathways. Weighted gene coexpression network analysis revealed eigengenes that were correlated with BMI, insulin, and NEFA.

Conclusions

TRE restored 24‐hour profiles in hormones, metabolites, and genes controlling transcriptional regulation in SAT, which could underpin its metabolic health benefit.
Xenon‐enhanced computed tomography assessment of brown adipose tissue distribution and perfusion in lean, obese, and diabetic primates
Authors: Garside John C. , Kavanagh Kylie , Block Masha R. , Williams Abigail G. , Branca Rosa T.
Published: August 2022

Objective

This study aimed to validate xenon‐enhanced computed tomography (XECT) for the detection of brown adipose tissue (BAT) and to use XECT to assess differences in BAT distribution and perfusion between lean, obese, and diabetic nonhuman primates (NHPs).

Methods

Whole‐body XECT imaging was performed in anesthetized rhesus and vervet monkeys during adrenergic stimulation of BAT thermogenesis. In XECT images, BAT was identified as fat tissue that, during xenon inhalation, underwent significant radiodensity enhancement compared with subcutaneous fat. To measure BAT blood flow, BAT radiodensity enhancement was measured over time on the six computed tomography scans acquired during xenon inhalation. Postmortem immunohistochemical staining was used to confirm imaging findings.

Results

XECT was able to correctly identify all BAT depots that were confirmed at necropsy, enabling construction of the first comprehensive anatomical map of BAT in NHPs. A significant decrease in BAT perfusion was found in diabetic animals compared with obese animals and healthy animals, as well as absence of axillary BAT and significant reduction of supraclavicular BAT in diabetic animals compared with obese and lean animals.

Conclusions

The use of XECT in NHP models of obesity and diabetes allows the analysis of the impact of metabolic status on BAT mass and perfusion.
Impacts of aphid herbivory on mycorrhizal growth responses across three cultivars of wheat
Authors: Charters Michael D. , Durant Emily K. , Sait Steven M. , Field Katie J.
Published: August 2022

Societal Impact Statement

The Earth's population is projected to rise to 9.7 billion by 2050 resulting in mounting pressure to increase agricultural yields in a sustainable manner. Arbuscular mycorrhizal (AM) fungi may be important players in this agricultural transition given their capacity to improve soil and plant health. Benefits gained by crops hosting AM fungi can be cultivar‐specific and also affected by insect herbivory, although the combined effect of these factors remains unclear. Here, we show that, in an economically and socially significant tri‐partite system, there is interplay between crop cultivar, AM colonisation and aphid herbivory on plant growth and nutritional status.

Arbuscular mycorrhizal (AM) fungi are critical components of the rhizosphere across nearly all terrestrial biomes. AM fungi associate with most plants, including major crops, usually increasing plant access to soil nutrients and enhancing defence against pests and pathogens in return for photosynthetic carbon (C). However, plant growth responses to AM fungi vary according to species and genotype, an issue pertinent in agro‐ecosystems where crop cultivar can play an important role in AM function. Evidence suggests other biotic interactions, including with sap‐feeding aphids, impact the function of AM symbioses in plants. Nonetheless, whether these biotic factors alter genotype (or cultivar)‐specific plant growth and nutritional responses to colonisation by AM fungi remains unclear.

Here, we investigated whether mycorrhizal responsiveness of three cultivars of wheat (Triticum eastivum L.) to colonisation by a ubiquitously occurring AM fungus (Rhizophagus irregularis) differ in the presence or absence of bird cherry‐oat aphids (Rhopalosiphum padi), a major pest of cereals.

Our findings show that although AM fungal colonisation and AM‐mediated plant growth responses were not affected by aphid feeding, there was variation between cultivars in the benefits gained by host plants in terms of nutrient acquisition and root growth, while aphid abundances also differed between wheat varieties.

Understanding what causes cultivar‐specific outcomes and how they ultimately impact plant growth promotion, crop yields and food production represent key future research goals in agroecology.
Xanthotoxin (8‐methoxypsoralen): A review of its chemistry, pharmacology, pharmacokinetics, and toxicity
Authors: Wu Anxin , Lu Jing , Zhong Guofeng , Lu Ling , Qu Yan , Zhang Chen
Published: August 2022

Xanthotoxin (XAT) is a natural furanocoumarins, a bioactive psoralen isolated from the fruit of the Rutaceae plant Pepper, which has received increasing attention in recent years due to its wide source and low cost. By collecting and compiling literature on XAT, the results show that XAT exhibits significant activity in the treatment of various diseases, including neuroprotection, skin repair, osteoprotection, organ protection, anticancer, antiinflammatory, antioxidative stress and antibacterial. In this paper, we review the pharmacological activity and potential molecular mechanisms of XAT for the treatment of related diseases. The data suggest that XAT can mechanistically induce ROS production and promote apoptosis through mitochondrial or endoplasmic reticulum pathways, regulate NF‐κB, MAPK, JAK/STAT, Nrf2/HO‐1, MAPK, AKT/mTOR, and ERK1/2 signaling pathways to exert pharmacological effects. In addition, the pharmacokinetics properties and toxicity of XAT are discussed in this paper, further elucidating the relationship between structure and efficacy. It is worth noting that data from clinical studies of XAT are still scarce, limiting the use of XAT in the clinic, and in the future, more in‐depth studies are needed to determine the clinical efficacy of XAT.
Online monitoring of profiles via function‐on‐scalar model with an application to industrial busbar
Authors: Zhang Wei , Niu Zhanwen , He Zhen , He Shuguang
Published: August 2022

In Statistical Process Control, profile monitoring is used for monitoring whether the process is in‐control or not by checking the relationship stability between the process response and covariates. In the industrial process recently, the functional relationship between the process variables is more and more complex, and the profile data are often time‐dependent and subject to within‐profile autocorrelation. We need to use appropriate models to characterize these complex relationships, and design new profile monitoring schemes to ensure satisfactory process monitoring performance. This paper studies a practical nonparametric profile monitoring problem, in which the functional relationship is in the form of function‐on‐scalar and within‐profile data are autocorrelated. A new online profile monitoring scheme is proposed to monitor process anomalies in real time. In Phase Ⅰ, based on the in‐control historical data, the model for the process is established estimated. Then, using the monitoring statistics based on penalty spline smoothing, the function‐on‐scalar monitoring parameters control scheme with a moving window is presented, and is applied to the anomaly monitoring of online sequential profile data. A large number of numerical simulation results show that in the presence of the function‐on‐scalar relationship, the proposed scheme has a superior performance in various cases. Finally, an application example of industrial busbar running process monitoring is given to illustrate the effectiveness of the scheme.
Experimental evaluation of louver guidance efficiency for green sturgeon (Acipenser medirostris)
Authors: Steel Anna E. , Nguyen Trinh , Cocherell Dennis E. , Carr Kara J. , Bell Heather , Peterson Amanda , Kavvas M. Levent , Fangue Nann A.
Published: August 2022

Throughout the world, louver‐bypass systems are a common method for fish protection at water diversion sites. Their performance has been evaluated for pelagic, strong‐swimming teleost fishes, but limited information exists regarding the effectiveness of louvers for guiding sturgeon, despite being a globally threatened taxon. This study used controlled laboratory experiments to quantify louver efficiency for juvenile green sturgeon under a range of conditions. Fish guidance efficiency was influenced most strongly by fish size and approach velocity, with poor efficiency for small fish at high velocities. Low velocities and, to a lesser extent, daylight conditions allowed a greater proportion of fish to remain upstream of the louver at all sizes. High velocities resulted in the greatest contact rate between the sturgeon and louver face. Louvers can be effective for benthic, weak‐swimming fish, but site‐ and species‐specific needs should always be considered in the development or operation of a louver guidance system.
Visible Light Mediated Heck Coupling of Inactivated Aryl Fluoride/Chloride Over a Sulfonic Acid Functionalized, Melamine‐based Metal‐free Porphyrin Photocatalyst
Authors: Bhuse Darpan Vijaykumar , Bhagat Pundlik Rambhau
Published: August 2022

We report the synthesis of a new, sulfonic acid functionalized, melamine‐based metal‐free porphyrin photocatalyst (MBMFPc) for the C−C coupling of the most unreactive aryl halides with alkenes under visible light irradiation. The ionic liquid‐based photocatalyst was characterized using various analytical techniques Proton Nuclear Magnetic Resonance (1HNMR) Spectroscopy, Carbon Nuclear Magnetic Resonance (13CNMR) Spectroscopy, Fourier Transformed Infrared Spectroscopy (FT‐IR), Energy‐dispersive X‐ray Spectroscopy (EDAX), Scanning Electron Microscope (SEM), Brunauer‐Emmett‐Teller (B.E.T) and Ultraviolet‐Visible Spectroscopy (UV‐Vis). The MBMFPc photocatalyst with noticeable Hammett acidity (0.56) and optimal bandgap of 1.44 eV was found to as an effective catalyst in the Mizoroki‐Heck coupling of inactivated aryl fluoride/chloride using 5 W LED in a homemade photoreactor under ambient conditions. The protocol comprising metal‐free green photocatalyst tolerated a variety of aliphatic/aromatic alkenes bearing different substituents afforded good to excellent yields. The role of photogenerated excitons was confirmed by scavenger studies with K2S2O8 and EDTA. The leaching test, stability, and reusability of MBMFPc photocatalyst evidenced as a perfect heterogeneous photocatalyst and afford appreciable yield (80 %) after 5 cycles. A plausible mechanism for photocatalytic C−C coupling has been proposed and described. A metal‐free acid‐functionalized ionic liquid‐based MBMFPc photocatalyst with appreciable TON (4,51,948) and TOF (22,597 h−1) could gain significant attraction as a green catalyst in the pharmaceutical industries for the synthesis of intermediates by C−C coupling using commercial aryl chlorides.
Heteroatom‐Modified Zeolite Y and Catalytic Performance of Their NiWS Supported Catalysts for Hydrocracking of Naphthalene
Authors: Cheng Yan , Dai Xiaojun , Wei Qiang , Wang Xiaohan , Zhou Yasong
Published: August 2022

In order to prepare hydrocracking catalyst with high catalytic performance for producing chemical raw materials, NiW supported catalysts was prepared with Ni−P co‐modified Y zeolites as the supports for the hydrocracking of naphthalene. Y zeolites were impregnated with different Ni−P contents, and the effects of Ni−P co‐modification on the physicochemical properties of Y zeolites, the properties of the active phases of the catalysts and the catalytic performance of catalysts were analyzed via a series of characterization methods. Ni−P co‐modification could effectively improve the pore properties and acid properties of Y zeolites, and made the acid density and acid strength of Y zeolites meet the requirements of selective cracking of naphthalene. Ni−P co‐modification could also effectively improve the reducibility of active metals,dispersion and stacking number of active phases of the catalysts, which greatly improved the selectivity of the target product (C6−C8) of the catalysts. Compared with NiW/HY, the yield of C6‐C8 products of NiW/2‐Ni/P−Y increased by 30.8 %. It is expected to provide a feasible strategy for the design and preparation of hydrocracking catalysts for the production of chemical raw materials in the integration of refining and chemical industry.
MOFs‐Derived Flower‐Like Hierarchically Porous Zn‐Mn‐Se/C Composite for Extraordinary Rate Performance and Durable Anode of Sodium‐Ion and Potassium‐Ion Batteries
Authors: Zhou Peng , Zhang Mingyu , Wang Liping , Huang Qizhong , Su Zhean , Xu Ping , Zou Renhao , Wang Xiaodong , Zeng Cen , Ba Kaixun
Published: August 2022

The slow kinetics and poor structural stability prevent transition metal selenides from being widely used in sodium‐ion batteries (SIBs) and potassium‐ion batteries (PIBs). Herein, the “flower‐like” porous carbon anchored by Zn‐Mn binary selenides (ZMS@FC) composites are fabricated by selenizing the modified hierarchically metal‐organic frameworks. The 2D conductive hierarchically flakes’ abundant pore structure and multiple active sites shorten the ion diffusion length and promote conductivity, while the synergistic effect of the binary metals and intrinsic large pseudocapacitive contribution effectively improve capacity and rate performance. ZMS@FC composites exhibit impressive rate capability of 294.4 mA h g–1 at 10 A g–1 and excellent cyclic stability with 369.6 mA h g–1 specific capacity retention at 2 A g–1 after 1000 cycling in SIBs. It is noted that 156.9 mA h g–1 can be retained at 5 A g–1 and 227.0 mA h g–1 is remained after 500 cycles at 2 A g–1 in PIBs. The ex situ X‐ray diffraction patterns and transmission electron microscopy pictures are used to confirm the conversion reaction processes of the Zn‐Mn‐Se. Designing high‐performance energy storage materials may benefit greatly from the universal synthesis technology of bimetallic sulfide anodes for enhanced SIBs and PIBs.
Re: Peripartum echocardiographic changes in women with hypertensive disorders of pregnancy
Authors: Florez D. , Barrios M. , de la Hoz‐Valle J.
Published: August 2022

Linked article: This Correspondence comments on Giorgione et al. Click here to view the article.
A generic approach to wind farm control and the power adjusting controller
Authors: Stock Adam , Leithead William
Published: August 2022

As wind farms become larger, there is scope for improved operation via wind farm control. Further development of wind farm control would be facilitated by more flexible operation of wind farms and so by more flexible operation of wind turbines. A novel approach to wind farm control is proposed that provides full flexibility of both. It consists of a wind farm controller architecture and an interface to individual turbines. The design of a specific realisation of the interface, the Power Adjusting Controller, is presented that requires little information on the turbine dynamics or controller and does not compromise the operation of the wind turbine controller or the turbine's safety. Results from a DNV Bladed simulation of a 5MW wind turbine are presented to illustrate the behaviour of the Power Adjusting Controller and to confirm that it meets the requirements to enable fully flexible operation of wind turbines and, so of wind farms.
Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts
Authors: Albert Elvira , Gordillo Pablo , Hernández-Cerezo Alejandro , Rodríguez-Núñez Clara , Rubio Albert
Published: August 2022

The use of the Ethereum blockchain platform [17] has experienced an enormous growth since its very first transaction back in 2015 and, along with it, the verification and optimization of the programs executed in the blockchain (known as Ethereum smart contracts) have raised considerable interest within the research community.
An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Authors: Bromberger Martin , Leutgeb Lorenz , Weidenbach Christoph
Published: August 2022

The importance of subsumption testing for redundancy elimination in first-order logic automatic reasoning is well-known. Although the problem is already NP-complete for first-order clauses, the meanwhile developed test pipelines efficiently decide subsumption in almost all practical cases. We consider subsumption between first-oder clauses of the Bernays-Schönfinkel fragment over linear real arithmetic constraints: BS(LRA). The bottleneck in this setup is deciding implication between the LRA constraints of two clauses. Our new sample point heuristic preempts expensive implication decisions in about 94% of all cases in benchmarks. Combined with filtering techniques for the first-order BS part of clauses, it results again in an efficient subsumption test pipeline for BS(LRA) clauses.
Evonne: Interactive Proof Visualization for Description Logics (System Description)
Authors: Alrabbaa Christian , Baader Franz , Borgwardt Stefan , Dachselt Raimund , Koopmann Patrick , Méndez Julián
Published: August 2022

Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The “justifications” usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.
GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Authors: Tammet Tanel , Draheim Dirk , Järv Priit
Published: August 2022

Our goal is to develop a logic-based component for hybrid – machine learning plus logic – commonsense question answering systems. The paper presents an implementation GK of default logic for handling rules with exceptions in unrestricted first order knowledge bases. GK is built on top of our existing automated reasoning system with confidence calculation capabilities. To overcome the problem of undecidability of checking potential exceptions, GK performs delayed recursive checks with diminishing time limits. These are combined with the taxonomy-based priorities for defaults and numerical confidences.
From the Universality of Mathematical Truth to the Interoperability of Proof Systems
Authors: Dowek Gilles
Published: August 2022

The development of computerized proof systems, such as Coq, Matita, Agda, Lean, HOL 4, HOL Light, Isabelle/HOL, Mizar, etc. is a major step forward in the never ending quest of mathematical rigor.
Lash 1.0 (System Description)
Authors: Brown Chad E. , Kaliszyk Cezary
Published: August 2022

Lash is a higher-order automated theorem prover created as a fork of the theorem prover Satallax. The basic underlying calculus of Satallax is a ground tableau calculus whose rules only use shallow information about the terms and formulas taking part in the rule. Lash uses new, efficient C representations of vital structures and operations. Most importantly, Lash uses a C representation of (normal) terms with perfect sharing along with a C implementation of normalizing substitutions. We describe the ways in which Lash differs from Satallax and the performance improvement of Lash over Satallax when used with analogous flag settings. With a 10 s timeout Lash outperforms Satallax on a collection TH0 problems from the TPTP. We conclude with ideas for continuing the development of Lash.
Binary Codes that Do Not Preserve Primitivity
Authors: Holub Štěpán , Raška Martin , Starosta Štěpán
Published: August 2022

A code X is not primitivity preserving if there is a primitive list $$\mathbf {w}\in \texttt {lists}\, X$$

w
∈
lists

X

whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a description of $$\{x,y\}$$

{
x
,
y
}

-interpretations of the square xx if $$\left| y \right| \le \left| x \right| $$

y

≤

x

. We also provide a formalized parametric solution of the related equation $$x^jy^k = z^\ell $$

x
j

y
k

=

z
ℓ

.
Formula Simplification via Invariance Detection by Algebraically Indexed Types
Authors: Matsuzaki Takuya , Fujita Tomohiro
Published: August 2022

We describe a system that detects an invariance in a logical formula expressing a math problem and simplifies it by eliminating variables utilizing the invariance. Pre-defined function and predicate symbols in the problem representation language are associated with algebraically indexed types, which signify their invariance property. A Hindley-Milner style type reconstruction algorithm is derived for detecting the invariance of a problem. In the experiment, the invariance-based formula simplification significantly enhanced the performance of a problem solver based on quantifier-elimination for real-closed fields, especially on the problems taken from the International Mathematical Olympiads.
Paraconsistent Gödel Modal Logic
Authors: Bílková Marta , Frittella Sabine , Kozhemiachenko Daniil
Published: August 2022

We introduce a paraconsistent modal logic$$\mathbf {K}\mathsf {G}^2$$KG2, based on Gödel logic with coimplication (bi-Gödel logic) expanded with a De Morgan negation$$\lnot $$¬. We use the logic to formalise reasoning with graded, incomplete and inconsistent information. Semantics of$$\mathbf {K}\mathsf {G}^2$$KG2is two-dimensional: we interpret$$\mathbf {K}\mathsf {G}^2$$KG2on crisp frames with two valuations$$v_1$$v1and$$v_2$$v2, connected via$$\lnot $$¬, that assign to each formula two values from the real-valued interval [0, 1]. The first (resp., second) valuation encodes the positive (resp., negative) information the state gives to a statement. We obtain that$$\mathbf {K}\mathsf {G}^2$$KG2is strictly more expressive than the classical modal logic$$\mathbf {K}$$Kby proving that finitely branching frames are definable and by establishing a faithful embedding of$$\mathbf {K}$$Kinto$$\mathbf {K}\mathsf {G}^2$$KG2. We also construct a constraint tableau calculus for$$\mathbf {K}\mathsf {G}^2$$KG2over finitely branching frames, establish its decidability and provide a complexity evaluation.
Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
Authors: Lahav Ori , Zohar Yoni
Published: August 2022

A four-valued semantics for the modal logic K is introduced. Possible worlds are replaced by a hierarchy of four-valued valuations, where the valuations of the first level correspond to valuations that are legal w.r.t. a basic non-deterministic matrix, and each level further restricts its set of valuations. The semantics is proven to be effective, and to precisely capture derivations in a sequent calculus for K of a certain form. Similar results are then obtained for the modal logic KT, by simply deleting one of the truth values.
Local Reductions for the Modal Cube
Authors: Nalon Cláudia , Hustadt Ullrich , Papacchini Fabio , Dixon Clare
Published: August 2022

The modal logic$${\mathsf {K}}$$Kis commonly used to represent and reason about necessity and possibility and its extensions with combinations of additional axioms are used to represent knowledge, belief, desires and intentions. Here we present local reductions of all propositional modal logics in the so-called modal cube, that is, extensions of$${\mathsf {K}}$$Kwith arbitrary combinations of the axioms$${\mathsf {B}}$$B,$${\mathsf {D}}$$D,$${\mathsf {T}}$$T,$${\mathsf {4}}$$4and$${\mathsf {5}}$$5to a normal form comprising a formula and the set of modal levels it occurs at. Using these reductions we can carry out reasoning for all these logics with the theorem prover "Image missing". We define benchmarks for these logics and experiment with the reduction approach as compared to an existing resolution calculus with specialised inference rules for the various logics.
Flexible Proof Production in an Industrial-Strength SMT Solver
Authors: Barbosa Haniel , Reynolds Andrew , Kremer Gereon , Lachnitt Hanna , Niemetz Aina , Nötzli Andres , Ozdemir Alex , Preiner Mathias , Viswanathan Arjun , Viteri Scott , Zohar Yoni , Tinelli Cesare , Barrett Clark
Published: August 2022

Proof production for SMT solvers is paramount to ensure their correctness independently from implementations, which are often prohibitively difficult to verify. Historically, however, SMT proof production has struggled with performance and coverage issues, resulting in the disabling of many crucial solving techniques and in coarse-grained (and thus hard to check) proofs. We present a flexible proof-production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers and show how we leverage it to produce detailed proofs, including for components previously unsupported by any solver. The architecture allows proofs to be produced modularly, lazily, and with numerous safeguards for correctness. This architecture has been implemented in the state-of-the-art SMT solver cvc5. We evaluate its proofs for SMT-LIB benchmarks and show that the new architecture produces better coverage than previous approaches, has acceptable performance overhead, and supports detailed proofs for most solving components.
Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Authors: Das Anupam , Girlando Marianna
Published: August 2022

We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic ($$\mathrm {PDL}$$
PDL
), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and $$\mathrm {PDL}$$
PDL
, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting ‘alternating traces’ and necessitating a more intricate soundness argument than for traditional cyclic proofs.
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
Authors: Durán Francisco , Eker Steven , Escobar Santiago , Martí-Oliet Narciso , Meseguer José , Rubio Rubén , Talcott Carolyn
Published: August 2022

Equational unification and matching are fundamental mechanisms in many automated deduction applications. Supporting them efficiently for as wide as possible a class of equational theories, and in a typed manner supporting type hierarchies, benefits many applications; but this is both challenging and nontrivial. We present Maude 3.2’s efficient support of these features as well as of symbolic reachability analysis of infinite-state concurrent systems based on them.
A Framework for Approximate Generalization in Quantitative Theories
Authors: Kutsia Temur , Pau Cleo
Published: August 2022

Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into “proximal” up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.
On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices
Authors: Akshay S. , Chakraborty Supratik , Pal Debtanu
Published: August 2022

The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem in this setting is as follows: given a set of pairs of rational weights and matrices$$\{(w_1, A_1), \ldots , (w_m, A_m)\}$${(w1,A1),…,(wm,Am)}, does there exist an integerNs.t for all$$n \ge N$$n≥N,$$\sum _{i=1}^m w_i\cdot A_i^n \ge 0$$∑i=1mwi·Ain≥0(resp.$$> 0$$>0). We study this problem, its applications and its connections to linear recurrence sequences. Our first result is that for$$m\ge 2$$m≥2, the problem is as hard as the ultimate positivity of linear recurrences, a long standing open question (known to be$$\mathsf {coNP}$$coNP-hard). Our second result is that for any$$m\ge 1$$m≥1, the problem reduces to ultimate positivity of linear recurrences. This yields upper bounds for several subclasses of matrices by exploiting known results on linear recurrence sequences. Our third result is a general reduction technique for a large class of problems (including the above) from diagonalizable case to the case where the matrices are simple (have non-repeated eigenvalues). This immediately gives a decision procedure for our problem for diagonalizable matrices.
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Authors: Frohn Florian , Giesl Jürgen
Published: August 2022

We present the Loop Acceleration Tool (), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on the novel calculus from [10, 11] for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, uses a new approach based on unsat cores. We evaluate ’s power and performance by extensive experiments.
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Authors: Lommen Nils , Meyer Fabian , Giesl Jürgen
Published: August 2022

There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use results on such subclasses of programs where complexity bounds are computable within incomplete approaches for complexity analysis of full integer programs. To this end, we present a novel modular approach which computes local runtime bounds for subprograms which can be transformed into twn-loops. These local runtime bounds are then lifted to global runtime bounds for the whole program. The power of our approach is shown by our implementation in the tool $$\textsf {KoAT}$$
KoAT
which analyzes complexity of programs where all other state-of-the-art tools fail.
SAT-Based Proof Search in Intermediate Propositional Logics
Authors: Fiorentini Camillo , Ferrari Mauro
Published: August 2022

We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based prover$$\texttt {intuitR} $$intuitRfor$$\mathrm {IPL} $$IPL(Intuitionistic Propositional Logic). Given an intermediate logicLand a formula$$\alpha $$α, the procedure outputs either a Kripke countermodel for$$\alpha $$αor the instances of the characteristic axioms ofLthat must be added to$$\mathrm {IPL} $$IPLin order to prove$$\alpha $$α. The procedure exploits an incremental SAT-solver; during the computation, new clauses are learned and added to the solver.
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)
Authors: Kremer Gereon , Reynolds Andrew , Barrett Clark , Tinelli Cesare
Published: August 2022

The SMT solver solves quantifier-free nonlinear real arithmetic problems by combining the cylindrical algebraic coverings method with incremental linearization in an abstraction-refinement loop. The result is a complete algebraic decision procedure that leverages efficient heuristics for refining candidate models. Furthermore, it can be used with quantifiers, integer variables, and in combination with other theories. We describe the overall framework, individual solving techniques, and a number of implementation details. We demonstrate its effectiveness with an evaluation on the SMT-LIB benchmarks.
Preprocessing of Propagation Redundant Clauses
Authors: Reeves Joseph E. , Heule Marijn J. H. , Bryant Randal E.
Published: August 2022

Thepropagation redundant(PR) proof system generalizes theresolutionandresolution asymmetric tautologyproof systems used byconflict-driven clause learning(CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solverSaDiCaLincorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We presentPReLearn, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large portion of SAT competition benchmarks we found that preprocessing withPReLearnimproves solver performance. In addition, there were several satisfiable and unsatisfiable formulas that could only be solved after preprocessing withPReLearn.PReLearnsupports proof logging, giving a high level of confidence in the results.
IKT-Nutzung im Kontext von Gesundheit und Fitness im Alter
Authors: Seifert Alexander , Schelling Hans Rudolf
Published: August 2022

Fitness- und Gesundheitswerte werden heute meist digital mit Wearables und Apps gemessen. Es gibt jedoch kaum Studien, welche die alltägliche Nutzung dieser Selbstvermessungstechnologien bei älteren Personen empirisch erforschen. Der vorliegende Bericht untersucht diese Nutzung anhand von Ergebnissen aus einer repräsentativen Schweizer Bevölkerungsbefragung, bei der 1149 Personen ab 65 Jahren befragt wurden. Die Ergebnisse zeigen, dass Wearables und Gesundheits-Apps noch eher selten von älteren Personen genutzt werden; dennoch sind hier Nutzungspotenziale erkennbar.
Digitale Unterstützung für junge Senior*innen: Auswahlkriterien für einen sozialen Roboter
Authors: Abseher Christoph , Igerc Irina Elisabeth , Schneider Cornelia
Published: August 2022

In den nächsten Jahren gehen geburtenstarke Jahrgänge in Pension. Dadurch steigt der Bedarf an alters- und bedarfsgerechten digitalen Lösungen für diese mittlerweile technikvertrautere Zielgruppe. Soziale Roboter bieten hier eine Möglichkeit der digitalen Unterstützung. Dieser Beitrag beschäftigt sich mit einem Kriterienkatalog, der eine systematische Auswahl von sozialen Robotern ermöglicht.
Wider die schlechte Gewohnheit: Selbstregulation erhöhen durch Fit-mit-ILSE
Authors: Würth Sabine , Hupfeld Hannah
Published: August 2022

Viele Menschen haben die Intention, sich mehr zu bewegen, scheitern aber an der Umsetzung in konkretes Verhalten. Fit-mit-ILSE, ein IKT-basiertes Bewegungsprogramm, unterstützt Personen bei ihrer Selbstregulation, um diese Intentions-Verhaltens-Lücke zu schließen. Basierend auf dem MoVo-Konzept von Fuchs (2007) wird im Rahmen eines Lernmoduls insbesondere der konstruktive Umgang mit Barrieren und Hindernissen vermittelt. Die Evaluierung von Fit-mit-ILSE legt nahe, dass ausgewählte Selbstregulationstechniken zielführend geschult werden können. Die Analysen zeigen, dass Fit-mit-ILSE insbesondere die subjektiv wahrgenommene Wirksamkeit des Barrieremanagement erhöht.
Level-Up? Zur Gamifizierung von Fitness- und Gesundheits-Apps
Authors: Loh Wulf
Published: August 2022

Gamifizierungsstrategien werden in Fitness-, Gesundheits- und Wohlbefindens-Apps weitläufig eingesetzt. In diesem Text wird untersucht, ob und inwieweit Gamifizierungen ethisch problematische Formen von Einflussnahme darstellen können. Dabei besteht zum einen die Gefahr, dass sie in der Motivation der Nutzer:innen auf unzulässige Formen von Paternalismus zurückgreifen. Zum anderen könnten hier ethisch bedenkliche Manipulationsstrategien im Spiel sein, wenn Apps versuchen, Nutzer:innen möglichst lange in der App zu halten und zur vermehrten Datenpreisgabe zu bewegen. Im Text wird dafür argumentiert, dass dies vor allem a) von der Schwere der motivationalen Effekte, b) dem Grad ihrer Erkennbarkeit, c) der Übereinstimmung der Ziele von Nutzer:in und App-Betreiber:innen, sowie d) der Wahrscheinlichkeit und Schwere unintendierter Nebenfolgen abhängt.
„Best Agers“ im digitalen Fitness-Trackingmodus. Zwischen Gesundheitsdispositiv und Selbstoptimierung
Authors: Dimitriou Minas
Published: August 2022

Ziel des Beitrages ist es, den semantischen Wandel des Fitnessbegriffes im Verhältnis zur präventivmedizinischen Bewegung am Beispiel des Konzepts des aktiven Alterns zu untersuchen. Parallel dazu soll der Einfluss von Tracking-Technologien und Anwendungen auf einen möglichen Bedeutungswandel in der Wechselbeziehung zwischen Gesundheit und Fitness bzw. Wellness analysiert werden.

Im Rahmen der Etablierung eines dominanten Gesundheitsdispositivs leisten Fitness und Wellness einen erheblichen Beitrag zur Klassifizierung, Konkretisierung und Aktualisierung von gesundheitsnormativen Idealen, was in den verschiedenen Bedeutungsverschiebungen und Interpretationsstrukturen deutlich wird. Durch die Tracking-Technologien im Prozess des aktiven Alterns und durch die Formierung neuer Subjektordnungen wird der Bedeutungswandel in der Wechselbeziehung zwischen Gesundheit und Fitness bzw. Wellness beschleunigt.
Fit mit Assistenzsystemen: Geht das denn?
Authors: Jungreitmayr Sonja
Published: August 2022

Es scheint viel Potenzial in Tablet und Co zu schlummern. Kann man der älteren Generation Programme zur Gesundheitsförderung via Smartphone und Applikationen näherbringen, sodass es ihr möglich ist mit diesen neuen Technologien länger fit und autonom in den eigenen vier Wänden zu leben? Ob diese Frage aufgrund vorliegender Erkenntnisse bestätigt werden kann oder doch wieder verworfen werden muss, versucht dieser Artikel zu ergründen.
USP48 and A20 synergistically promote cell survival in Helicobacter pylori infection
Authors: Jantaree Phatcharida , Chaithongyot Supattra , Sokolova Olga , Naumann Michael
Published: August 2022

The human pathogen Helicobacter pylori represents a risk factor for the development of gastric diseases including cancer. The H. pylori-induced transcription factor nuclear factor kappa-light-chain-enhancer of activated B cells (NF-κB) is involved in the pro-inflammatory response and cell survival in the gastric mucosa, and represents a trailblazer of gastric pathophysiology. Termination of nuclear NF-κB heterodimer RelA/p50 activity is regulated by the ubiquitin-RING-ligase complex elongin-cullin-suppressor of cytokine signalling 1 (ECSSOCS1), which leads to K48-ubiquitinylation and degradation of RelA. We found that deubiquitinylase (DUB) ubiquitin specific protease 48 (USP48), which interacts with the COP9 signalosome (CSN) subunit CSN1, stabilises RelA by deubiquitinylation and thereby promotes the transcriptional activity of RelA to prolong de novo synthesis of DUB A20 in H. pylori infection. An important role of A20 is the suppression of caspase-8 activity and apoptotic cell death. USP48 thus enhances the activity of A20 to reduce apoptotic cell death in cells infected with H. pylori. Our results, therefore, define a synergistic mechanism by which USP48 and A20 regulate RelA and apoptotic cell death in H. pylori infection.