bluuebunny/crossref_metadata_2025_split huggingface dataset:
Simple Rules for Market Selection and Entry
Authors: Shepherd Dean A. , Patzelt Holger , Breugst Nicola 
Published: June 2024

AbstractThis chapter offers simple rules for market selection and entry. These simple rules are: identify a broad opportunity set from which to choose the “best” one; think like a scientist to generate novel business models or opportunities; with resource constraints, embrace the lean startup approach; create, use, and adapt a community of inquiry to evaluate and co-construct an opportunity; and if your opportunity does not work out, pivot.
Synthesis of Recursive Programs in Saturation
Authors: Hozzová Petra , Amrollahi Daneshvar , Hajdu Márton , Kovács Laura , Voronkov Andrei , Wagner Eva Maria 
Published: June 2024

AbstractWe turn saturation-based theorem proving into an automated framework for recursive program synthesis. We introduce magic axioms as valid induction axioms and use them together with answer literals in saturation. We introduce new inference rules for induction in saturation and use answer literals to synthesize recursive functions from these proof steps. Our proof-of-concept implementation in theVampiretheorem prover constructs recursive functions over algebraic data types, while proving inductive properties over these types.
Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Authors: Heuer Jan , Wernhard Christoph 
Published: June 2024

AbstractWe show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs P and Q and vocabulary V (set of predicates) the existence of a program R in V such that $$P \cup R$$

P
∪
R

and $$P \cup Q$$

P
∪
Q

are strongly equivalent can be expressed as a first-order entailment. Moreover, our result is effective: A program R can be constructed from a Craig interpolant for this entailment, using a known first-order encoding for testing strong equivalence, which we apply in reverse to extract programs from formulas. As a further perspective, this allows transforming logic programs via transforming their first-order encodings. In a prototypical implementation, the Craig interpolation is performed by first-order provers based on clausal tableaux or resolution calculi. Our work shows how definability and interpolation, which underlie modern logic-based approaches to advanced tasks in knowledge representation, transfer to answer set programming.
Regularization in Spider-Style Strategy Discovery and Schedule Construction
Authors: Bártek Filip , Chvalovský Karel , Suda Martin 
Published: June 2024

AbstractTo achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov’s system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.
Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
Authors: Lommen Nils , Meyer Éléanore , Giesl Jürgen 
Published: June 2024

AbstractRecently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabilistic programs and show its soundness for complexity analysis. To demonstrate its benefits, we implemented our new CFR technique in our complexity analysis tool .
Certifying Phase Abstraction
Authors: Froleyks Nils , Yu Emily , Biere Armin , Heljanko Keijo 
Published: June 2024

AbstractCertification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.
Quantifier Shifting for Quantified Boolean Formulas Revisited
Authors: Heisinger Simone , Heisinger Maximilian , Rebola-Pardo Adrian , Seidl Martina 
Published: June 2024

AbstractModern solvers for quantified Boolean formulas (QBFs) process formulas in prenex form, which divides each QBF into two parts: the quantifier prefix and the propositional matrix. While this representation does not cover the full language of QBF, every non-prenex formula can be transformed to an equivalent formula in prenex form. This transformation offers several degrees of freedom and blurs structural information that might be useful for the solvers. In a case study conducted 20 years back, it has been shown that the applied transformation strategy heavily impacts solving time. We revisit this work and investigate how sensitive recent QBF solvers perform w.r.t. various prenexing strategies.
MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper)
Authors: Hader Thomas , Kaufmann Daniela , Irfan Ahmed , Graham-Lengrand Stéphane , Kovács Laura 
Published: June 2024

AbstractThis system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2 ’s frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.
A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations
Authors: Ge Rui , Garcia Ronald , Summers Alexander J. 
Published: June 2024

AbstractSMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to be challenging. If quantifier instantiation is not carefully controlled, then runtime and outcomes can be brittle and hard to predict. In particular, uncontrolled quantifier instantiation can lead to unexpected incompleteness and even non-termination. E-matching is the most widely-used approach for controlling quantifier instantiation, but when axiomatisations are complex, even experts cannot tell whether or not their use of E-matching guarantees completeness or termination.This paper presents a new formal model that facilitates the proof, once and for all, that giving a complex E-matching-based axiomatisation to an SMT solver such as Z3 or cvc5, cannot cause non-termination. Key to our technique is an operational semantics for solver behaviour that models how the E-matching rules common to most solvers are used to determine when quantifier instantiations are enabled, but abstracts over irrelevant details of individual solvers. We demonstrate the effectiveness of our technique by presenting a termination proof for a set theory axiomatisation adapted from those used in the Dafny and Viper verifiers.
Fast and Verified UNSAT Certificate Checking
Authors: Lammich Peter 
Published: June 2024

AbstractWe describe a formally verified checker for unsatisfiability certificates in the LRAT format, which can be run in parallel with the SAT solver, processing the certificate while it is being produced. It is implemented time and memory efficiently, thus increasing the trust in the SAT solver at low additional cost.The verification is done w.r.t. a grammar of the DIMACS format and a semantics of CNF formulas, down to the LLVM code of the checker. In this paper, we report on the checker and its design process using the Isabelle-LLVM stepwise refinement approach.
Stepping Stones in the TPTP World
Authors: Sutcliffe Geoff 
Published: June 2024

AbstractThe TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. There are key components that help make the TPTP World a success: the TPTP problem library was first released in 1993, the CADE ATP System Competition (CASC) was conceived after CADE-12 in 1994, problem difficulty ratings were added in 1997, the current TPTP language was adopted in 2003, the SZS ontologies were specified in 2004, the TSTP solution library was built starting around 2005, the Specialist Problem Classes (SPCs) have been used to classify problems since 2010, the SystemOnTPTP service has been offered from 2011, the StarExec service was started in 2013, and a world of TPTP users have helped all along. This paper reviews these stepping stones in the development of the TPTP World.
A Higher-Order Vampire (Short Paper)
Authors: Bhayat Ahmed , Suda Martin 
Published: June 2024

AbstractThe support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and a dedicated strategy schedule. The theoretical ideas are still under development, so we discuss them at a high level in this paper. We also describe the implementation of the calculus in the Vampire theorem prover, the strategy schedule construction and several empirical performance statistics.
Nature of Science-Perspektiven aus der Didaktik der Biologie – Theorie und Praxis
Authors: Reinisch Bianca , Krüger Dirk , Mahler Daniela 
Published: June 2024

ZusammenfassungDie Komplexität und Dynamik der heutigen Welt, geprägt durch vielfältige technologische Fortschritte und globale Herausforderungen wie Klimawandel und Biodiversitätsverlust, rücken die Notwendigkeit einer fundierten naturwissenschaftlichen Bildung in den Vordergrund. Besonders die Biologie als Wissenschaft des Lebens spielt eine entscheidende Rolle für das Verständnis dieser komplexen Themen. Gleichzeitig rückt die naturwissenschaftliche Forschung als solche vermehrt – teils kritisch oder wenig reflektiert – in den Fokus der gesellschaftlichen Aufmerksamkeit. Die öffentliche Kommunikation von Forschungsergebnissen seitens Forschender spielt in diesem Kontext eine verstärkte Rolle. Die adäquate Einordnung und Bewertung solcher Ergebnisse verlangen dabei vielfältige Kompetenzen seitens der einzelnen Person. Ein Verständnis der Nature of Science, also der Natur der Naturwissenschaft selbst, kann dazu beitragen, Studien und ihre Ergebnisse in bestehende Erkenntnisse einzuordnen sowie etwaige Konsequenzen für sich und andere abzuleiten.
Die Natur der Naturwissenschaftsdidaktiken als Reflexionsmöglichkeit für die Lehrkräftebildung
Authors: Büssing Alexander Georg 
Published: June 2024

ZusammenfassungWährend die Förderung des professionellen Wissens grundsätzlich eine große Rolle innerhalb der Lehrkräftebildung spielt, wurden epistemische Aspekte dieses Wissens bisher nur unzureichend thematisiert. Gerade in Modellen wie dem Refined Consensus Model of Pedagogical Content Knowledge (RCM), welches eine Differenzierung unterschiedlicher Facetten des fachdidaktischen Wissens beschreibt, werden die entsprechenden epistemischen Voraussetzungen nicht beachtet. Dies betrifft insbesondere die fachdidaktischen Wissensformen, für die bisher keine Systematisierung epistemischer Aspekte besteht. Hierfür könnte die Nature of Science (NOS) eine wichtige Perspektive bilden. Ein sinnvoller Ansatz könnte der Family Resemblance Approach (FRA) nach Erduran et al. (2019) darstellen, laut dem insgesamt elf Kategorien zur Charakterisierung von kognitiv-epistemischen und sozial-institutionellen Dimensionen von Wissenschaften unterschieden werden können. Im Beitrag wird eine solche Systematisierung als Natur der Naturwissenschaftsdidaktiken vorgeschlagen und anhand von drei Thesen diskutiert. Dabei stellt Wissen über die Natur der Naturwissenschaften eine Voraussetzung für professionelles fachdidaktisches Wissen von Lehrkräften dar (These 1), da epistemische Aspekte des fachdidaktischen Wissens nur unzureichend durch NOS beschrieben werden. Dieses Wissen über die Natur der Naturwissenschaften wirkt sich in der Schulpraxis aus (These 2) und sollte daher expliziter in der Lehrkräftebildung thematisiert werden (These 3). Auch wenn die Natur der Naturwissenschaftsdidaktiken bisher nur theoretisch postuliert ist, kann eine solche Systematisierung der Komplexität naturwissenschaftsdidaktischen Handelns besser gerecht werden und sollte daher weiterverfolgt werden.
Umgang mit Ungewissheit als Charakteristikum von Nature of Science
Authors: Lübke Britta , Heuckmann Benedikt 
Published: June 2024

ZusammenfassungAus wissenschaftstheoretischer Perspektive lässt sich Ungewissheit als konstitutives und produktives Element der Naturwissenschaften beschreiben. In bisherigen Nature of Science (NOS)-Konzeptionen spielt Ungewissheit jedoch nur eine untergeordnete Rolle. Für den deutschsprachigen Diskurs kommt erschwerend hinzu, dass sich der englische Begriff uncertainty sowohl mit Ungewissheit als auch mit Unsicherheit übersetzen lässt. In diesem Artikel wird eine Unterscheidung der Begriffe vorgeschlagen. Der für den Kontext von NOS präferierte Begriff der Ungewissheit im Sinne eines Nicht-Genau-Wissens wird zudem ausdifferenziert, indem zwischen epistemischer und ontologischer Ungewissheit sowie zwischen technischer Ungewissheit und Konsensungewissheit unterschieden wird. Für die Frage nach der Integration in Lehr-Lern-Konzepte wird das Verhältnis von Ungewissheit und Vorläufigkeit vor dem Hintergrund der Unterscheidung Latours zwischen ready-made-science und science-in-the-making diskutiert. Zudem wird mit dem Family Resemblance Approach eine NOS-Konzeption auf mögliche Anknüpfungspunkte für die Thematisierung des Umgangs mit Ungewissheit in den Naturwissenschaften untersucht.
Erkenntnisgewinnung (v)erklärt
Authors: Großmann Leroy , Krüger Dirk 
Published: June 2024

ZusammenfassungDie Hypothese bildet einen zentralen Bestandteil im Rahmen naturwissenschaftlicher Erkenntnisprozesse. Ihr kommt als kognitiv-epistemischer Aspekt eines elaborierten Nature of Science-Verständnisses eine große Bedeutung zu. Der Begriff ist jedoch doppeldeutig: So wird der Begriff Hypothese einerseits sachangemessen für deduktiv aus einer soliden Wissensbasis abgeleitete, begründete und empirisch prüfbare Voraussagen eines Untersuchungsergebnisses genutzt. Wir schlagen vor, den andererseits in der Schule verwendeten Begriff Hypothese für vorläufige, häufig vage Ideen, mit denen man sich ein noch unbekanntes Phänomen zu erklären versucht, durch Erklärungsversuch zu ersetzen. Die Nutzung des Hypothesen-Begriffs, einerseits mit dem Schwerpunkt im Kompetenzbereich Erkenntnisgewinnung über Hypothesen zu reflektieren und andererseits mit Sachkompetenz eine fachangemessene Erklärung zu finden, wird in diesem Beitrag anhand einer exemplarischen Analyse zweier Staatsexamensentwürfe im Fach Biologie illustriert. Abschließend werden Perspektiven für die empirische fachdidaktische Forschung aufgezeigt.
Organic matter, carbon, and nitrogen relationships of regreened forest soils in an industrially impacted landscape
Authors: Levasseur Patrick A. , Aherne Julian , Basiliko Nathan , Watmough Shaun A. 
Published: June 2024

Context Soil organic matter (SOM) is largely composed of carbon (C) and nitrogen (N), the proportions of which often change with soil depth. The relationships between SOM, C, and N in forest soils can be greatly altered in degraded landscapes and understanding these relationships is integral for successful forest restoration planning. Aims The current study investigated SOM, C, and N relationships in highly degraded forest soils by depth following regreening (one-time application of soil amendments and afforestation). Additionally, the use of standard C:OM ratios (which are commonly used to estimate soil C) were assessed. Methods The SOM, C, and N were measured at five different depths, at nine sites, ranging in time since regreening treatment applications across one of the world’s largest regreening programmes in the City of Greater Sudbury, Canada. Key results The C:OM and C:N ratios decreased with soil depth while N:OM increased. The C and N were significantly correlated with SOM at all depths (excluding the L horizon). The C:OM ratio was lower than standard values and did not change between 16 and 41 years since the application of 10 Mg ha−1 of dolomitic limestone. Conclusions Despite massive soil degradation, SOM, C, and N relationships over soil depth at the regreening sites are consistent with unimpacted forest soils. Applying commonly used C:OM ratios drastically overestimated soil C pools, especially at lower depths. Implications Even in the most degraded landscapes, restoration can improve soil properties. Standard C:OM ratios should be used with caution.
Slavery, homeownership, and contemporary perinatal outcomes in the southeast: a test of mediation and moderation
Authors: Stanhope Kaitlyn K , Kramer Michael R , McKinnon Izraelle , Carter Sierra , Boulet Sheree L 
Published: June 2024

Abstract
The objective of this study was to estimate the effect of geographic variation in historic slavery on perinatal outcomes (chronic hypertension, hypertensive disorders of pregnancy [HDP], very preterm birth [VPTB], or very low birth weight birth [VLBW]) among Black people living in states where slavery was legal in 1860; and to test mediation by Black homeownership. We linked data on the proportion of enslaved residents from the 1860 Census to natality data on outcomes (2013-2021) using resident county. The percentage of Black residents in a county who owned their home was a potential mediator. We fit log binomial models to estimate risk ratios (RRs) representing total and controlled direct effects (accounting for Black homeownership) of the proportion enslaved on outcomes, accounting for potential confounding, using marginal structural models. Among 2 443 198 included births, 8.8% (213 829) experienced HDP, 4.1% (100 549) chronic hypertension, 3.3% (81 072) VPTB, and 2.6% (62 538) VLBW. There was an increase in chronic hypertension and VPTB risk, but not HDP or VLBW, in counties with a 10% greater proportion of enslaved residents in 1860 (adjusted RR [95% CI], chronic hypertension: 1.06 [1.02-1.1]; VPTB: 1.02 [1.00-1.05]; HDP: 1.00 [0.98-1.02]; and VLBW: 1.01 [1.00-1.03]). There was not evidence of mediation by Black homeownership. We conclude that historic slavery remains relevant for perinatal health.
Risk factors of peritoneal dialysis–related peritonitis in the Japan Peritoneal Dialysis Outcomes and Practice Patterns Study (PDOPPS)
Authors: Ito Yasuhiko , Tu Charlotte , Yamaguchi Makoto , Koide Shigehisa , Ryuzaki Munekazu , Bieber Brian , Pisoni Ronald L , Perl Jeffrey , Minakuchi Jun , Kawanishi Hideki ,   the Japan PDOPPS Study Committee, Kawanishi Hideki , Minakuchi Jun , Tomo Tadashi , Tsuchiya Ken , Nitta Kousaku , Ryuzaki Munekazu , Fukazawa Mizuya , Ito Yasuhiro , Nakamoto Hidetomo , Yamashita Akihiro 
Published: June 2024

ABSTRACT

Background
Peritoneal dialysis (PD)-related peritonitis is a major complication of PD. Wide variations in peritonitis prevention, treatment strategies and consequences are seen between countries. These between-country differences may result from modifiable risk factors and clinical practices.

Methods
A total of 1225 Japanese PD patients were included and prospectively followed in the Peritoneal Dialysis Outcomes and Practice Patterns Study phase 1 (2014–2018) and phase 2 (2018–2022). Associations between PD-related peritonitis and various risk factors were assessed by Cox proportional hazards survival models.

Results
During follow-up (median 1.52 years), 539 peritonitis episodes were experienced by 364 patients. The country crude peritonitis rate was 0.27 episodes/patient-year. In the fully adjusted model, noticeable patient-level factors associated with experiencing any peritonitis included age {hazard ratio [HR] 1.07 per 5-year increase [95% confidence interval (CI) 1.01–1.14]}, serum albumin level [HR 0.63 per 1 g/dl higher (95% CI 0.48–0.82)] and continuous ambulatory peritoneal dialysis (PD) [HR 1.31 versus automated PD (95% CI 1.05–1.63)]. The adoption of antibiotic prophylaxis practice at the time of PD catheter insertion [HR 0.63 (95% CI 0.51–0.78)] or when having complicated dental procedures [HR 0.74 (95% CI 0.57–0.95)] or lower endoscopy [HR 0.69 (95% CI 0.54–0.89)] were associated with lower hazards of any peritonitis, while a routine facility practice of having more frequent regular medical visits was associated with a higher hazard.

Conclusion
Identification of risk factors in Japan may be useful for developing future versions of guidelines and improving clinical practices in Japan. Investigation of country-level risk factors for PD-related peritonitis is useful for developing and implementing local peritonitis prevention and treatment strategies