dataesr/scientific-paragraphs-categorization huggingface dataset:
). An example of an agent is a user, although one individual user can have many agent profiles (see sec. 3. 2). Entities such as a trustworthy central database can also correspond to an agent. Trusted agents have been largely neglected in the formal reasoning world, but they are common in other high reliability settings, such as security. Nevertheless, agents are at least implicitly present in any formal development: to claim that a result has been formally achieved is tantamount to saying that some trustworthy agent (e. g. , peer reviewers) has correctly and successfully executed a specific collection of formal tools to convince themselves of that formal result. Furthermore, if one agent A trusts another B, there is no need for A to re-check B's proof scripts and re-execute any tools that B used to construct the result.
Dispatch also helps to analyze and modify the trust parameters for (compositions of) assertions. Second, we implement a version of the Abella interactive theorem prover  [9]  that can produce and consume assertions in DAMF, mediated by Dispatch. As an example of its use, we show how Abella can use a lemma that was stated and proved using the automated linear arithmetic reasoning tactics of Coq (v. 8. 16. 1); this lemma is manually translated from the Coq to the Abella language, with an explicit dependency on its Coq development, and added to the global store by the present authors. A user can accept this heterogeneous development as long as they trust Coq, Abella, and our translation of the Coq lemma to Abella. Moreover, this assertion, which contains explicit links to the externally sourced DAMF imports, can be published back to DAMF for use by others.
Languages, contexts, and formulas To transfer a theorem from a source proof system to a target proof system, we must be able to transfer the statement of the theorem, which we represent as a formula object in DAMF. To be as general as possible, we represent the content of such a formula as a string, i. e. , in a format suitable as an input to a parser of the source proof system. In order to determine that the input is well-formed, the source proof system may need further information about the features-symbols, predicates, functions, types, notations, hints, etc. -used in the formula. Such additional information is the context of the formula, which we represent as a document fragment in the language of the source proof system. For example, take the following theorem written in Coq 8. 16. 1: 1 Definition lincomb (n j k : nat) := exists x y, n = x * j + y * k.
2 Theorem ex_coq : forall n:nat, 8 <= n -> lincomb n 3 5. The formula corresponding to the theorem ex_coq is the literal string "forall n:nat, • • • lincomb n 3 5". The symbols 8, <=, etc. are part of the standard prelude of this language, and the symbol lincomb is defined in line 1, so a sufficient context necessary for Coq 8. 16. 1 to parse and type-check the theorem statement is the text of line 1, which is also written in the Coq 8. 16. 1 language. Abstractly, a formula object in DAMF is a triple (L, Σ, F ) where L denotes a language, Σ denotes a context, and F denotes a formula, all of which may conceptually be thought of as strings. We will use the schematic variable N to range over such formula objects. The language L is a canonical identifier (specifically, the cid of a DAMF language object) which may optionally represent information about a suitable loader for the language that will make sense of the strings Σ and F ; DAMF compares languages just by their identifiers.
Moreover, L is interpreted as defining all the globally available features; for instance, the symbol nat is part of the standard prelude of this version of Coq and should therefore be understood as being defined in the language Coq 8. 16. 1. The context Σ introduces any user-defined features such as the definition lincomb above that is not part of Coq's standard prelude. Note that DAMF formula objects are considered to be closed, i. e. , every symbol used in the formula is defined in the language or the context. From the perspective of DAMF, a formula object is an atomic entity. Additionally, DAMF does not need to be aware of any reasoning principles of the language or context components. For instance, no mechanism in DAMF would allow the substitution of a declared symbol in the context with a concrete definition.
16. 1 language to be used by a different system with a different language, say Abella 2. 0. 9, we will need to transform the formula objects in the former language to those in the latter language. This kind of translation is an example of a language adapter, which falls into the general class of adapters, and which creates a sequent by translating between languages or modifying the logical context by standard logical operations such as weakening (adding extra symbols), instantiation (replacing a symbol by a term), or unfolding (replacing a defined symbol by its definition). As an example, the Coq 8. 16. 1 example above can be translated to the Abella 2. 0. 9 language as follows, where the function symbols + and * are replaced by relations in Abella. 2 Import "nats". % some natural numbers library Define lincomb : nat -> nat -> nat -> prop by lincomb N J K := exists X Y U V, times X J U /\ times Y K V /\ plus U V N.
Such rules are neither syntactically well-formed nor desirable for our purposes. We use here a very weak access control logic (see  [1]  for a survey of such logics). Instead, checking the validity of a given derivation using Compose is computationally trivial: each instance of it must eliminate exactly the leftmost dependency in the second premise, which is a DAMF formula object that is compared by cid. Observe that the agent K does not participate in a meaningful way in a derivation that is built with the Compose rule. Thus, for a given end sequent of the form K says (⊢ N ), a Compose derivation can be seen as a proof outline for the desired theorem N , with the leaves of the derivation being the assertions that need to be sourced from an assertion database (such as the DAMF global store).
We say that an assertion (K says S) is published if it can be retrieved from such a database. The inference system is then enlarged with the following rule that can be used to complete the open leaves of the Compose derivation using assertions made by different agents. (K 1 says S) is published K 2 says S Trust [K 1 → K 2 ] This rule is parameterized by a pair of agents, K 1 and K 2 , and is understood to be applicable only when K 1 is in the user-specified allow list of K 2 (i. e. , K 1 speaks for K 2 , which we write as [K 1 → K 2 ]). We do not assume that agents have any additional closure properties beyond Compose and Trust. For example, suppose N A , N A→B , and N B are the formula objects that correspond to the formulas A, A → B, and B respectively in some language. We do not assume that the following rule is admissible: K says (Γ ⊢ N A→B ) K says (Γ ⊢ N A ) K says (Γ ⊢ N B ) mp.
Given these schemata, the aspects of tracking and trusting become natural: a formula present as a dependency in some assertion could be matched with the same formula present as the conclusion of a different assertion. It is also useful to annotate these core DAMF objects with additional metadata such as external names, proof objects, timestamps, etc. In DAMF, we have chosen to give the core objects a cid independent of the metadata; instead, for every core object, we define an annotated object that is composed of a link to the core object and a link to any additional metadata. DAMF follows the design principle that objects are to be considered equal at the DAMF level if they have the same cid: the content of the objects is not examined, and no IPLD-links are followed for such comparisons. Generally speaking, therefore, DAMF core objects will not link to annotated objects, since the annotations will factor into the cids and force disequality when undesired, such as when building compositions (sec.
The process we consider first in our implementation is lookup which will be discussed further below. Individual producers and consumers, such as theorem provers, can choose to implement some or several of these DAMF processes. However, many aspects of dealing with linked data and IPFS will be common to such tools, so we describe an intermediary tool called Dispatch that simplifies the interactions between these producers and consumers and the DAMF global store. Of course, Dispatch would be considered part of the trusted code base, along with IPFS and any utilities used to manipulate JSON data and cryptographic signatures. If this is problematic, Dispatch can be completely foregone in preference to native implementations. The Dispatch tool is distributed as an executable dispatch with three subcommands: publish, get, and lookup.
The dispatch publish command operates on one of a collection of standard input formats that contains local information corresponding to DAMF types. After syntactically validating this input, the publish command will construct and publish the global objects. Dispatch can also optionally interact with a specific storage service in order to make that object widely discoverable in the IPFS network. As an example, consider the following input for an assertion object, where newly created formulas and contexts are placed in the same file and are referred by local names such as plus_comm, and previously existing objects are referred by their cids using the damf: flag, such as the first value of "dependencies" (line 10) which refers to a formula object cid, as well as "language" and "mode" values which refer to existing language and tool objects respectively.
Edge systems example: Abella We have implemented a DAMF-aware branch of Abella  [9]  as an example of a system that interacts with assertions in DAMF with the help of Dispatch as a mediator. Abella was originally designed to test a particular approach to meta-theoretic reasoning using a new, proof-theoretically motivated mechanism for reasoning directly with bound variables (in particular, the ∇-quantifier  [31]  and a treatment of equality based on equivariant higher-order unification  [27] ). While the current implementation of Abella has succeeded with those meta-theoretic tasks  [23, 42] , the prover has not grown much beyond that domain. Indeed, Abella has some (mis)features that make it a good test case for DAMF: (1) it has no awareness of the file system and it is easy to replace the backing store from local files to objects stored in IPFS; (  2 ) it has a feature-poor proof language with nearly no support for proof automation and hence an underdeveloped formal mathematical libraries; and (3) it uses relational specifications as opposed to the more common functional programming specifications.
Furthermore, the area of meta-theory that Abella treats declaratively is also an area many conventional proof systems do not deal well, in part, because of the need to encode and manipulate bindings  [8, 24]. Such conventional systems might be willing to delegate such meta-theoretic reasoning to Abella. Ordinary Abella developments (in. thm files) support a kind of import mechanism which loads in marshaled results from a different run of Abella. We extend import with a new kind of statement: Import "damf:bafyr. " that refers to a collection of DAMF assertions (i. e. , a DAMF collection object whose elements are assertions). Dispatch is used to fetch all the referenced objects from IPFS as explained in the previous subsection. To appeal to an assertion, the elements of the context of the conclusion of the assertion are merged using their internal names with the ambient context of Abella where the assertion is appealed to.
Other use cases While it is common to view tools that perform pure computations (such as functional program execution or proof search a la λProlog) as producing assertions without proofs, there are various well-known reasoning systems that have been used a lot without being either certified or certifying: for example, Twelf  [33]. DAMF would enable Twelf-based assertions to be exported to agents willing to trust its type and totality checkers. The relationship of DAMF to the following topics is discussed in greater detail in the technical report  [3] : libraries as curation on top of the DAMF model of global objects; attacks in the adversarial environment of the web; and possible uses of this framework in settings (such as journalism) where the lack of formal proof means increasing the need to explicitly track trust.
, 12}. We could of course have used Coq to perform these computations as well, but it is pedagogically useful to see an example that combines both functional and relational programming. Further details on this example, including the various input files and the precise tools and commands to run to verify the development, can be found in the following location: https://distributed-assertions. github. io/example-walkthrough/. Require Import Arith Lia. Note the various appeals to the linear integer arithmetic solver lia in the proofs, either used directly or via a defined Ltac liarw defined in lines  13-15. If Coq were to add publishing support for DAMF, the sequent generated for the fib_square_lemma theorem above may look something like this: 1 { "format": "assertion", 2 "agent": "exampleAgent", 3 "claim": { 4 "format": "annotated-production", 5 "annotation": {"name": "fib_square_above"}, Here, the "mode" on line 7 represents a DAMF object that describes the Coq (v.
B. 4 Adapting λProlog and Coq sequents for Abella Taking stock, we have ground facts built in the higher-order logic programming language λProlog using the tool Teyjus, and a lemma about the rate of growth of the Fibonacci function written in the calculus of inductive constructions using the tool Coq. Obviously, neither of these languages correspond to the language G that forms the basis of the Abella theorem prover. Thus, we need adapters for translating these external dependencies to Abella's language. These adapters can, in principle, be quite sophisticated; for instance, they can be written using Dedukti. For illustration purposes in the present paper, we adapt the sequents by hand by asserting in Abella the intended translation at the point of importing the assertion. Imagine, for instance, that the fib5 assertion shown in Section B.
2 is given the cid bafyrei4j. Here is how we would import it in Abella: 37 %% FibExample. thm continuing. 38 Import "damf:bafyrei4j. " as 39 Theorem fib5: fib (s (s (s (s (s z))))) (s (s (s (s (s z))))). From the perspective of Abella, this looks just like an ordinary Theorem statement, except there is no proof that follows. Instead, Abella would generate the following adapter sequent (which it could then publish using Dispatch): 1 { "format": "assertion", 2 "agent": "exampleAgent", 3 "claim": { 4 "format": "annotated-production", 5 "annotation": {"name": "fib5"}, 6 "production": { 7 "mode": null, 8 "sequent": { 9 "conclusion": "fib5", "dependencies": [ "damf:bafyrei4j. /claim/sequent/conclusion" ] } } }, "formulas": { "fib5": { "language": "damf:bafyreig8. ", "content": "fib (s (s (s (s (s z))))).
", "context": ["fib5!context"] } }, "contexts": { "fib5!context": { "language": "damf:bafyreig8. ", "content": [ "Kind nat type. ", "Type z nat. ", "Type s nat -> nat. ", "Define fib : nat -> nat -> prop by. " ] } } } Lines 14 and 19 above are references to a DAMF object describing the Abella language. In line 7, the "mode" field is left as null to indicate that this assertion was not created by any tool; in other words, the agent "exampleAgent" is solely responsible for the assertion. If a tool had been used instead, this field would refer to the DAMF description of that tool. Finally, in line 11, the dependency that is included is the cid of the conclusion of the assertion object that was produced by λProlog, and in turn imported by Abella in line 38 of FibExample. thm. As explained in Section 3.
During each cell division, tens of thousands of DNA replication origins are co-ordinately activated to ensure the complete duplication of the human genome. However, replication fork progression can be challenged by many factors, including co-directional and head-on transcription-replication conflicts (TRC). Head-on TRCs are more dangerous for genome integrity. To study the direction of replication fork movement and TRCs, we developed a bioinformatics toolkit called OKseqHMM (https://github. com/CL-CHEN-Lab/OK-Seq, https://doi. org/10. 5281/zenodo. 7428883). Then, we used OKseqHMM to analyse a large number of datasets obtained by Okazaki fragment sequencing to directly measure the genomewide replication fork directionality (RFD) and to accurately predict replication initiation and termination at a fine resolution in organisms including yeast, mouse and human.
Importantly, we and others have recently demonstrated that R-loops frequently accumulate at transcription termination sites of actively transcribed genes with a high frequency of head-on TRCs  (22, 23). Therefore, systematically unveiling DNA replication features genome-wide is essential for human health. However, to date, no bioinformatic tool has been developed to analyse RFD data and to determine the replication initiation and termination positions genome-wide, although several methods have been previously described for OK-seq data analysis, for instance, the Hidden Markov Model (HMM) to analyse human OK-seq data  (6)  and origin efficiency metric (OEM) for yeast OK-seq data  (24, 25). Therefore, to set up a uniform framework for OK-seq data (and related data) analysis, we developed an integrative bioinformatics toolkit, called OKseqHMM, to directly obtain RFD profiles genome-wide and at high resolution.
In addition to the fork progression direction, this toolkit also gives information on replication initiation/termination zones and on long-travelling unidirectional forks using an algorithm based on HMM, and calculates the OEM to visualize the transition of RFD profile at multiple scales. It then generates the average metagene profiles and heatmaps to visualize the RFD/OEM distribution along the regions of interest (Figure  1 ). Using OKseqHMM and a large number of publicly available OK-seq datasets (13 in total) from S. cerevisiae, mouse and human cells, we successfully obtained high-resolution (∼1 kb for mouse and human cells and ∼50 bp for yeast) RFD profiles and accurate calling of the corresponding replication initiation and termination zones genome-wide.
By default, windows with < 30 reads on both strands were masked. The RF D values (between -1 and 1) were divided into five quantiles. Then, the HMM package of R (http://www. r-project. org/) was used to perform the HMM prediction with probabilities of transition and emission that are manually defined using the training dataset (Figure  2B ). The same transition and emission probabilities used in our previous study  (6)  were set as default values and used in all OK-seq data analyses in the current study. Two representative examples of human RFD profiles with the segments of IZs, TZs and two Flat states obtained by OKseqHMM are shown in Figure  2C, D. The choice of a 15 kb sliding window was based on a compromise between spatial resolution and reproducibility of ascending segment detection among biological replicates.
The average metagene profile/heatmap visualizes the RFD distribution in specific genomic regions To analyse RFD distributions around and/or among genomic regions of interest (e. g. the identified IZs or annotated genes), an additional module was developed for metadata analysis. Using the gene coordinates (or IZs) and the RFD and/or OEM big wiggle files generated with the OKseqHMM and/or OKseqOEM functions, the corresponding profiles/heatmaps can be easily generated with the computeMatrix and plotProfile/plotHeatmap functions of deepTools (https://deeptools. readthedocs. io/ en/develop/index. html)  (26)  by defining the genomic dis-tances of interest for the upstream and downstream borders (Figure  1 ).
Genome-wide detection of replication fork directionality and initiation zones using OK-seq data from different human cell lines Then, the OKseqHMM function was used to analyse previously published OK-seq data from HeLa MRL2 cells (  6 ) and new OK-seq data from HeLa S3 cells, a widely used Encode Tier 2 cell line. The RFD profiles of the two HeLa cell lines were very similar (R = 0. 86, P < 10 -15 ), suggesting similar replication programs and IZ positions (Figure  4A ). The correlation between HeLa cell lines was slightly lower than the correlation between the HeLa MRL2 cell biological replicates (R = 0. 92, P < 10 -15 ) (6), suggesting that the differences between HeLa cell lines were true biological differences and not only technical variations. In each HeLa cell line, ∼10 000 IZs were identified (Table  1 ), 67% of which were common between cell lines (Figure  4B ).
IZ conservation was even higher in early-replicating regions: 80% of early IZs were shared between HeLa cell lines (Figure  4B ). As expected, these shared IZs showed higher firing efficiency and larger size than IZs specific for each dataset (Supplementary Figure  S3A-D ). It should be noted that for cell-line specific IZs, the RFD transitions were much stronger in the mean RFD profile of the cell line in which such IZs were detected than in the other cell line. However, the RFD profiles in the other cell line were not completely flat, suggesting that some IZs with low firing efficiency were not detected with our current parameter setting. Interestingly, both shared and cell-specific IZs displayed a high probability of confidence, suggesting a low false positive detection rate (Supplementary Figure  S3E ).
A very striking difference between human and yeast RFD data was that the size of upward transitions of RFD, therefore the IZ length, ranged between 10 and 50 kb in human cells (∼30 kb on average, which is ∼20-fold larger than the IZ length in yeast), unlike the sharp 1 kb upward transition of RFD at fixed yeast origins (Figure  4A , Table  1 ). The OEM profile heatmaps, computed around IZs at different scales, showed the strongest positive signals at the corresponding scale: 10 kb scale for small IZs (<10 kb), 20 kb scale for medium IZs (20-50 kb) and 50 or 100 kb for large IZs (>50 kb) (Figure  4C ). This confirmed that RFD transitions are associated with the detected IZ length, and also supports the difference between yeast and human OK-seq patterns and the accuracy of IZ detection by OKseqHMM.
This clearly highlighted frequent replication initiation (upward transition of RFD) in the regions upstream of TSS and downstream of TTS. This leads to a codirectionality between replication and transcription at TSS and a higher risk of head-on TRC at TTS, in agreement with previous publications  (6, 22). As illustrated also in the study by Promonet et al, combining RFD profiles obtained from OK-seq data with other genomic data (e. g. gene transcription, R-loops, replication fork stalling and DNA damage) allowed us to show that fork pausing at TTS of highly expressed genes containing R-loops prevents head-on TRCs and maintains genome integrity  (22). In addition to the OK-seq data of HeLa cell lines, the OKseqHMM function was used to reanalyse publicly available OK-seq data from different human cell lines  (6, 27) , such as fibroblasts (IMR90), lymphoblastoid (GM06990) and lymphoma cells (Raji, BL79, IARC385), leiomyosarcoma cells (IB118, TLSE19), leukaemia cells (K562) and erythroblasts (TF1) (Table  1 , Figure  6 ).