bluuebunny/crossref_metadata_2025_split huggingface dataset:
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

AbstractThroughout 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

AbstractWe 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

AbstractIn 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

AbstractThe 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.
A generic approach to wind farm control and the power adjusting controller
Authors: Stock Adam , Leithead William 
Published: August 2022

AbstractAs 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

AbstractThe 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

AbstractThe 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

AbstractExplanations 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

AbstractOur 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.
Lash 1.0 (System Description)
Authors: Brown Chad E. , Kaliszyk Cezary 
Published: August 2022

AbstractLash 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

AbstractA 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

AbstractWe 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

AbstractWe 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

AbstractA 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

AbstractThe 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

AbstractProof 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

AbstractWe 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

AbstractEquational 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

AbstractAnti-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

AbstractThe 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

AbstractWe 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

AbstractThere 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

AbstractWe 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

AbstractThe 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.