dataesr/scientific-paragraphs-categorization huggingface dataset:
The PSMSL has experience working with more than 200 data authorities and close co-operation with GLOSS/ Intergovernmental Oceanographic Commission/European Global Ocean Observing System, and therefore has the opportunity to take a world-leading role to develop and deliver a suite of SL services. For example, PSMSL already provides products 15  globally, regionally and nationally and will develop these further, particularly drawing on its expertise to support decision-makers. In addition to PSMSL, a variety of agencies and research groups have demonstrated leadership in this arena. In the United States, multiple frameworks have been developed to combine information about future SL rise with land-use, economic, and demographic data to inform decision makers and map regions of enhanced risk (e.
The Sea Level Futures Conference (Liverpool, United Kingdom,  July 2-4, 2018) , celebrating the 85th anniversary of PSMSL, reviewed the present status of SL science knowledge, covering key aspects of SL change. Special emphasis was given to existing SL observations, synthesis of available data and discussion of future novel observational techniques in coastal areas. The science provides clear evidence that SL is rising and this is already impacting vulnerable coastal areas, especially those with rapidly growing urban populations and associated infrastructure. Addressing these challenges in a warming climate requires integrated sustainable and continued observations, data products and advanced modeling capability. Thus, as recognized by conference participants, there is a requirement for close collaboration between scientists from different disciplines and the broad stakeholder community to develop plans for responding to SL change, storm surges and flood risk affecting the coastal zone.
Key actions necessary to enable the development of SL services that can effectively support adaptation and mitigation measures and empower decision-makers in coastal communities should include: • Commitment to sustained, systematic and complementary global and coastal measurements of SL and its components to understand observed variability and change, to constrain 18 https://uhslc. soest. hawaii. edu/sea-level-forecasts/ 19 https://coastal. er. usgs. gov/hurricanes/research/twlviewer/ longer term projections and to improve skill of forecasting and early warning systems. This commitment must be in line with efforts under the Global Ocean Observing System, Global Geodetic Observing System, GLOSS and other programs. • Commitment to extend the historical SL record through data rescue, digitization and the accurate detailed integration of historic tide gauge data into international repositories to reduce spatial and temporal gaps and to validate process-understanding as well as processbased climate models, and to detect and attribute the influence of natural (intrinsic and externally forced) and human-induced drivers.
ACKNOWLEDGMENTS The contents of this manuscript are partly based on the results from: the workshop on "Understanding the relationship between coastal sea level and large-scale ocean circulation, " held at and generously supported by the  International Space Science Institute, Bern, Switzerland ; the  Sea Level Futures Conference , hosted by the  National Oceanography Centre, Liverpool ,  United Kingdom ; the project " Advanced Earth System Modelling Capacity , " and the  Copernicus Marine Environmental Monitoring Service  through the  WaveFlow Service Evolution  project.
FUNDING RP was funded by  NASA  grant  NNH16CT00C. CD was supported by the  Australian Research Council  ( FT130101532  and  DP 160103130 ), the  Scientific Committee on Oceanic Research (SCOR) Working Group 148 , funded by national SCOR committees and a grant to SCOR from the  U. S. National Science Foundation  (Grant  OCE-1546580 ), and the  Intergovernmental Oceanographic Commission of UNESCO/International Oceanographic Data and Information Exchange (IOC/IODE) IQuOD Steering Group. SJ was supported by the  Natural Environmental Research Council  under Grant Agreement No. NE/P01517/1  and by the  EPSRC NEWTON Fund Sustainable Deltas Programme , Grant Number  EP/R024537/1. RvdW received funding from  NWO , Grant  866. 13. 001. WH was supported by  NASA  ( NNX17AI63G  and  NNX17AH25G ). CL was supported by  NASA  Grant  NNH16CT01C.
This work is a contribution to the  PIRATE  project funded by  CNES  (to TP). PT was supported by the  NOAA Research Global Ocean Monitoring and Observing Program  through its sponsorship of  UHSLC  ( NA16NMF4320058 ). JS was supported by  EU  contract  730030  (call  H2020-EO-2016 , "CEASELESS"). JW was supported by  EU Horizon 2020  Grant  633211 , Atlantos.
Ladder Logic is a programming language standardized in IEC 61131-3 and widely used for programming industrial Programmable Logic Controllers (PLC). A PLC program consists of inputs (whose values are given at runtime by factory sensors), outputs (whose values are given at runtime to factory actuators), and the logical expressions computing output values from input values. Due to the graphical form of Ladder programs, and the amount of inputs and outputs in typical industrial programs, debugging such programs is time-consuming and error-prone. We present, in this paper, a Why3based tool research prototype we have implemented for automating the use of deductive verification in order to provide an easy-to-use and robust debugging tool for Ladder programmers.
Introduction Programmable logic controllers (PLC) are industrial digital computers used as automation controllers of manufacturing processes, such as assembly lines or robotic devices. PLCs can simulate the hard-wired relays, timers and sequencers they have replaced, via software that expresses the computation of outputs from the values of inputs and internal memory. Ladder language, also known as Ladder Logic, is a programming language used to develop PLC software. This language uses circuits diagrams of relay logic hardware to represent a PLC program by a graphical diagram. This language was the first available to program PLCs. It is now standardized in IEC 61131-3  [1]  standard among other languages but is still widely used and very popular among technicians and electrical engineers. In conventional development of software, a great part of the development time is dedicated to debugging.
e. executing the program on a particular initial configuration and check its behavior). In industry, tests used to be run directly in the factory, which is very costly and risky. Nowadays, most of the tests are run on a software simulation, but some are often still run in the factory for a last check of the program behavior in real conditions of use, or for bypassing the difficulty to simulate particular sequences of inputs. Even when run on a software simulation, tests-based processes are still time-consuming and cannot be exhaustive. On the other hand, some research work has been done concerning formal analysis of Ladder programs. Most of this work  [7]  [6]  [9]  [10] concerns the verification of temporal properties of Ladder programs (a Ladder program being continuously executed in the PLC), and uses different model checking techniques.
Some other work used deductive verification to detect data races  [13]  and prove safety properties  [12]  (with some temporal aspects) of Ladder programs. Model-checking techniques are limited by the state explosion problem they face when addressing real-world problems. On the contrary, deductive verification may give full confidence in the obtained results but may also prevent from a full automatization of the process (in terms of proof automation and specification formalization). Our objective in this work was to make a proof of concept of an easy-to-use and robust tool for debugging Ladder programs, both increasing the quality of the code and decreasing the time to deploy, a crucial point in the context of Industry 4. 0, in which assembly lines are more often reconfigured, hence code evolves frequently.
Ladder Logic Ladder Logic is a graphical programming language using relay logics diagrams to represent a PLC program. A Ladder program takes inputs values (contacts) that correspond to the fact that physical relays are wired, not wired, pulsing (rising edge) or downing (falling edge) and other values stored in the internal memory of the PLC (booleans, integers, floating point, strings, etc. ). A Ladder program can output boolean values to the physical relays of the factory (coils) or it can call instructions, that may modify the values of the internal memory of the PLC (devices). Graphically, contacts are located at the left of the diagram. They can be combined in a serial way or in a parallel way (the obtained value is then the conjunction, resp. the disjunction of the two contacts values).
Since this format can only represent 4 digits decimal numbers, the BCD instruction raises an error when it is called on a device value that does not belong to interval [0; 9999]. This is typically the kind of runtime errors we want to detect with the tool we developed. Regarding this example, we were also interested in overflows that could occur when calling instruction INC. The example we present is very simple but typical industrial programs we had access to have hundreds of lines, hundreds of inputs, devices and outputs, and dozens of instructions calls. As a last point, such a Ladder program is executed cyclically in a synchronous way: first inputs are read, then the program is executed and eventually outputs are written. One single execution of the program is called a scan. We developed around fifty such formalizations of Ladder instructions in order to run our tool prototype on the industrial program samples we had access to.
Then our translation of Ladder programs to Why3 models consists in translating on-the-fly the logical expressions that correspond to coils and their combinations, and combine them with calls to the instructions formalizations of our library, using a single-state-assignment  [11]  transformation to handle the iterative aspect of Ladder programs. Our tool automatically 1 translates Ladder programs into Why3 modules that refer to the instructions formalizations described in the previous section. We implemented our own library to produce Why3 text files, to help the reuse of generated modules. During the translation, we use labels to keep information on code location of instruction calls to give improved feedback to the programmer when an error is found. Then we use Why3's WP calculus to 2 compute verification conditions that correspond to preconditions of instructions, and use Why3 API to 3 send those verification conditions to SMTsolver CVC4  [3]  (we chose CVC4 for its overall good performances and its ability to generate counter-examples when a verification condition cannot be proved).
Graphical user feedback We implemented a proof of concept of a graphical interface which gives back to the programmer information about found bugs, in an easy-to-understand manner. The aim of such an interface is to be directly integrated in Ladder IDEs. We based our prototype implementation on the Ocsigen web framework  [2]  which allowed us to quickly prototype a web-based graphical interface displaying information coming from our tool prototype implemented in OCaml. We identified three pieces of information that should be displayed to the programmer when a bug is found: the error location (where the error occurs), the error reason (why the error occurs) and the error scenario (when the error occurs). The error location is encoded during the on-the-fly translation from the Ladder program to the Why3 model: to each instruction call is attached a label which contains its location in the original source code.
This label is propagated during the WP calculus, appears in the verification condition sent to the automated solver and comes back in the counter-example the solver gives when it finds one. The error reason is encoded in the Why3 instructions library as shown in figure  2. It is attached, with a "expl:" label, to pre-conditions of Ladder instructions, and is propagated during the whole process, like code locations labels. As explained in the previous section, the error scenario consists in the initial and intermediate values that lead to the error. It is re-computed from solvers' counter-examples, and is expressed with colors for wiring values (blue when a wire is active, grey otherwise) and figures for other values above the corresponding devices. Figure  4  shows a screenshot of this graphical interface.
Performances Our proprietary prototype is implemented in OCaml, in about 13, 000 lines of code, including 3, 000 lines for our library to produce Why3 textual files and 4, 000 lines for the graphical user interface. We made some optimization effort concerning the modelization of Ladder language in Why3, in order to obtain a fully automated and fast process. But we made no optimization in our OCaml code, and even did not parallelize the calls to SMT-solvers. Nonetheless our protype has already pretty good performances. We ran our prototype tool on an industrial code sample with 1, 657 steps (i. e. contacts, coils and instruction calls), among which three instructions calls could lead to an error. On a virtualized Ubuntu 18. 04, running in VirtualBox 5. 2, under Windows 10 on a Intel Core i7-7500U 2.
Objective -NosoBase® is a collection of documentation centres with a national bibliographic database dedicated to infection prevention and control (IPC), with over 20 years of experience in France. As a quality assurance activity, this study was conducted in 2017 with a three-step approach to evaluate the bibliographic database regarding (1) the availability and coverage of citations; (2) the scope and relevance of content; and (3) the quality of the documentation centre services. Methods -The three-step quality approach involved (1) evaluating the availability and coverage of citations in NosoBase® by searching for the bibliographic citations of three systematic reviews on hand hygiene practices, published recently in three different peer-reviewed international journals; (2) evaluating the scope and relevance of content in NosoBase® by searching for all documents from 2015 indexed in NosoBase® under hand hygiene related keywords, and analyzing according to publication language, document type (e.
g. , legislation, research, or guidelines), and target audience; and 3) evaluating the strengths, weaknesses, and opportunities of the documentation centre services, with interviews involving the librarians. Results -NosoBase® contained 70. 8%-80. 9% of references directly concerning hand hygiene cited by the three systematic reviews. Of the 200 articles indexed in NosoBase® under hand hygiene related keywords in 2015, 22. 5% were French language based, with a significant representation of French non-indexed literature. The analysis of the documentation centre services highlighted future opportunities for growth, building on the strengths of experience and collaborations, to improve marketing and usability, targeting francophone IPC professionals. Conclusion -Specialized bibliographic databases may be useful and time efficient for the retrieval of relevant specialized content.
Introduction With the growing emphasis on evidence based practice, more databases and research content are now being made available. Yet it is often difficult and time-consuming for clinicians and researchers to locate relevant literature even if it is more accessible. Studies indicate that searches only on Google Scholar may not be enough  (Boeker, Vach, & Motschall, 2013) , and that searches on multiple databases are often necessary for finding relevant bibliographic content  (Rathbone, Carter, Hoffmann, & Glasziou, 2016). One earlier study compared several health-related databases (CINAHL, Cochrane Library, MEDLINE, PsycLIT, Sociofile, and Social Science Citation Index), and found that PsycLIT was the most useful database for information on the rehabilitation of people with severe mental illness in terms of search efficiency and relevance in this topic area, highlighting the importance of a specialized bibliographic database  (Brettle & Long, 2001).
More recently,  Rethlefsen, Murad, and Livingston (2014)  proposed that human-indexed databases allow faster, more comprehensive searching in terms of terminology and controlled vocabulary structure than solely computer algorithm-indexed databases such as Scopus and Google Scholar, despite search engines that search full-text articles in the latter. The impact of trained searching and assistance from trained information professionals and librarians has also been underlined (Centre for  Reviews and Dissemination, 2009). Librarian coauthors correlated with higher quality reported search strategies in general internal medicine systematic reviews, leading to a more comprehensive, true systematic review  (Rethlefsen, Farrell, Osterhaus Trzasko, & Brigham, 2015). As a quality assurance activity, this study evaluated NosoBase®.
Created in 1996, NosoBase® is a national project focused on infection prevention and control (IPC) in healthcare settings  (Savey, Sanlaville, & Fabry, 2000). It consists of five documentation centres, with trained librarians located in different cities in France (Lyon, Paris, Rennes, Bordeaux, and Nancy). It hosts a forum for IPC professionals and a website with resources and tools. There are collaborations with national medical or professional IPC learned societies, cooperation with other libraries, and bibliographic support to the national public health agency. Based in the French language, it manages a bibliographic database also known as NosoBase®, indexing up to 180 journals in multiple languages. This study describes a three-step quality assessment conducted in 2017 to evaluate the content of the database (steps 1 and 2) and the documentation centre services (step 3).
Literature Review Bibliographic databases came into being in the 19th and 20th centuries in response to the proliferation of journals and other publications, then went online in the late 20 th century  (Glasziou & Aronson, 2017). Specialized (or subject-specific) bibliographic databases are now available in diverse fields, from chemistry (Chemical Abstract Service) to psychology, psychiatry, and neurology (PsycINFO); from nursing and caring sciences (CINAHL) to geology (GeoBase)  (Gasparyan et al. , 2016). Many offer access mainly through subscription or through membership in professional associations. In France, bibliographic databases such as Pascal & Francis and the public health database Banque de Données en Santé Publique (BDSP) were developed in the 1970s and 1990s, respectively. It was noted that in the Pascal database, around 12% of the journals indexed were French language based, and 55% of the journals indexed were not available in PubMed  (Dufour, Mancini, & Fieschi, 2009).
However, bibliographic databases and the documentation centres that maintain them currently face growing costs for maintenance and rising competition from multidisciplinary databases such as PubMed that provide free online access. Researchers began to compare recall efficacy between multidisciplinary databases and specialized databases. One case study used a systematic review to investigate the performance of bibliographic databases in identifying the included studies. Its results showed that the use of at least two databases and reference checking were required to retrieve all included studies  (Beyer & Wright, 2013). Another study examined the yield of MEDLINE, EMBASE, and CENTRAL to find randomized controlled trials within the area of musculoskeletal disorders. It found that searching all three databases was not sufficient for identifying all effect studies on musculoskeletal disorders, though an additional 10 databases did only increase the median recall by 2%  (Aagaard, Lund, & Juhl, 2016).
However, the findings of this study have been disputed. Guistini and Kamel Boulos (2013)  noted that Google Scholar was still unreliable for searching systematic reviews due to its constantly changing content, algorithms, and database structure. Other studies found that Google Scholar missed important literature in evidence reviews and grey literature searching  (Haddaway, Collins, Coughlin, & Kirk, 2015)  or that it presented incomplete recall  (Bramer, Giustini, Kramer, & Anderson, 2013). In France, websites and portals in the French language dedicated to health literature have been in place for some time, such as CISMeF, Recomedical, BIU Santé Paris, and BDSP, a database for public health hosted by the national public health higher learning institution Ecole des Hautes Etudes en Santé Publique (EHESP) in Rennes.
Aims After more than 20 years of experience, the librarians of the documentation centre NosoBase® wanted to assess the quality and the usefulness of the services and tools provided. This study was conducted in 2017 with a threestep process to evaluate the bibliographic database NosoBase® regarding (1) the availability and coverage of citations and (2) the scope and relevance of content, as well as (3) the quality of the NosoBase® documentation centre services.
Methods A three-step quality assessment was used in order to evaluate the content of the database and the documentation centre services. Step 1 evaluated the availability and coverage of citations in NosoBase® through searching for bibliographic citations of three systematic reviews on hand hygiene practices, which were published recently in three different peerreviewed international journals. Step 2 evaluated the scope and relevance of content in NosoBase® by searching for all documents from 2015 indexed in NosoBase® under hand hygiene related keywords, and analyzing them according to publication language, document type (e. g. , legislation, research, or guidelines), and target audience. Step 3 evaluated the strengths, weaknesses, and opportunities of the documentation centre services, with input from the librarians.
Review 1: Musuuza, J. S. ,  Barker, A. , Ngam, C. , Vellardita, L. , & Safdar, N. (2016)  For each systematic review, all bibliographic citations were listed on a spreadsheet indicating availability, whether directly related to hand hygiene practices, and whether indexed under hand hygiene keywords, with a note for comments. Their availability in the database of NosoBase® was verified during February 2017. Step.
2: Scope and Relevance of Content in NosoBase® A search was performed on February 9, 2017, for all indexed documents under hand hygiene related keywords from the database of NosoBase®. The year 2015 was chosen since publications from the end of 2016 were not yet completely indexed by February 2017. The documents were analyzed according to the publication language and document type (e. g. , legislation, research article, or guidelines), as well as target audience. Step 3: Quality Review of the Documentation Centre Services Using the National Conservatory of Arts and Crafts and National Institute for Documentation Techniques (CNAM INTD, http://intd. cnam. fr/) methodologies as models  (Toneatti, 2008; Palisse, 2011) , a qualitative descriptive approach was chosen for this study, examining six categories: communication, accessibility, production, management, marketing, and opportunities, through a modified SWOT analysis (strengths, weaknesses, and opportunities, with threats analyzed under weaknesses).