BACKGROUND: Allele Specific Expression analysis is an important tool for integrating genome and transcriptome data. It quantifies expression variation between the two haplotypes of a diploid individual distinguished by heterozygous sites, and is a powerful tool to estimate cis-regulatory diversity of alleles. Clustering algorithms can be used to identify patterns or groups of genes/samples based on their expression profiles. Depending on the structure of the data, different existing clustering algorithm can be adapted to allele specific expression data. However, no ad-hoc procedure has been developed. RESULTS: In this work, we begin defining an expression matrix capturing allele expressions from an RNA-sequencing experiment. On this matrix, we develop a novel two-phase unsupervised clustering procedure, built on top of a spectral clustering algorithm, whose aim is to partition the population into groups of similar individuals, according to their allelic expression. As case-studies, the approach is used to cluster 98 cultivars representative of the variability observed in Vitis vinifera, starting from read counts of genes of chromosome 1 of leaves, and to analyze allele-specific count data from a CASTxMRL F1 hybrid mice dataset. CONCLUSION: Using the above mentioned real case-studies as well as generated synthetic data, we see that our algorithm shows significant robustness and outperforms other standard clustering techniques.

Co-lex partial orders (Cotumaccio et al., SODA 2021 and Journal of the ACM 2023) are a powerful tool to index finite automata, with applications to regular expression matching, generalizing Wheeler orders (Gagie et al., Theoretical Computer Science 2017). The co-lex width p of an automaton naturally measures how sortable its states are w.r.t. the co-lexicographic order among its accepted strings. Automata of co-lex width p can be compressed to O ( log ⁡ p ) bits per edge and admit regular expression matching in time proportional to p 2 per matched character. The deterministic co-lex width of a regular language L is the smallest width of such a co-lex order, among all DFAs recognizing L . Since languages of small co-lex width admit efficient solutions to hard computational problems on the language, computing the co-lex width of a language is relevant in applications. Previous work shows that the deterministic co-lex width p of a language L can be computed in m O ( p ) , given as input any DFA A with m transitions accepting L . For constant p (in particular Wheeler languages, where p = 1 ), the constant in the exponent is large and the exact complexity remains unknown. In this work, using new techniques, we show that one can decide in O ( m p ) if the deterministic co-lex width of the language recognized by a given minimum DFA is strictly smaller than p ≥ 2 . We complement this with a matching conditional lower bound based on the Strong Exponential Time Hypothesis. Hence, our paper essentially settles the complexity of the problem.

Abstract The celebrated Ackermann encoding of hereditarily finite sets is generalized to a parametric formula designed to map not only these sets but also hereditarily finite multisets and hypersets into the non-negative real numbers. This extension suggests a novel approach to the graph canonization problem by reducing it to a simple comparison of real values. By suitably varying the sole parameter of this formula, both the original Ackermann encoding and another previously studied map emerge as special cases. When the parameter is chosen from the natural numbers, the function yields a bijective encoding of a subuniverse of hereditarily finite multisets into the natural numbers. If, instead, the parameter is chosen to be transcendental and lies within a specific interval on the positive real line, the function is conjectured to provide an injective encoding of both multisets and hypersets.

We tackle the (classic) problem of minimizing (non)deterministic finite automata. The algorithm we put forward has the peculiarity of being incremental, i.e., the minimization proceeds by successive iterations, each producing a partially minimized automaton language-equivalent to the input one. Our algorithm builds upon Almeida et al. from 2014, fixing a minor mistake and generalizing it to the nondeterministic case. It relies on a coloring procedure of a graph associated to the automaton, keeping track of partial information. After dealing with the deterministic case, we extend this idea to the bisimulation-minimization of nondeterministic automata. The algorithms for both the deterministic and the nondeterministic cases run in time O(nm) for an automaton with n states and m transitions. The complexity for the deterministic case matches the complexity claimed by Almeida et al.. The nondeterministic case improves the fastest known incremental algorithm for this problem. We conclude introducing and using a notion of signature of a state, whose aim is to exploit pre-computed information potentially available, to speed-up the process. A signature is used to produce an initial partition of the automaton's states and can be easily integrated in both the incremental and the non-incremental algorithm.

The states of a finite-state automaton 𝒩 can be identified with collections of words in the prefix closure of the regular language accepted by 𝒩. But words can be ordered, and among the many possible orders a very natural one is the co-lexicographic order. Such naturalness stems from the fact that it suggests a transfer of the order from words to the automaton’s states. This suggestion is, in fact, concrete and in a number of articles automata admitting a total co-lexicographic ( co-lex for brevity) ordering of states have been proposed and studied. Such class of ordered automata — Wheeler automata — turned out to require just a constant number of bits per transition to be represented and enable regular expression matching queries in constant time per matched character. Unfortunately, not all automata can be totally ordered as previously outlined. In the present work, we lay out a new theory showing that all automata can always be partially ordered, and an intrinsic measure of their complexity can be defined and effectively determined, namely, the minimum width p of one of their admissible co-lex partial orders –dubbed here the automaton’s co-lex width . We first show that this new measure captures at once the complexity of several seemingly-unrelated hard problems on automata. Any NFA of co-lex width p : (i) has an equivalent powerset DFA whose size is exponential in p rather than (as a classic analysis shows) in the NFA’s size; (ii) can be encoded using just Θ(log p ) bits per transition; (iii) admits a linear-space data structure solving regular expression matching queries in time proportional to p 2 per matched character. Some consequences of this new parameterization of automata are that PSPACE-hard problems such as NFA equivalence are FPT in p , and quadratic lower bounds for the regular expression matching problem do not hold for sufficiently small p . Having established that the co-lex width of an automaton is a fundamental complexity measure, we proceed by (i) determining its computational complexity and (ii) extending this notion from automata to regular languages by studying their smallest-width accepting NFAs and DFAs. In this work we focus on the deterministic case and prove that a canonical minimum-width DFA accepting a language ℒ–dubbed the Hasse automaton ℋ of ℒ–can be exhibited. ℋ provides, in a precise sense, the best possible way to (partially) order the states of any DFA accepting ℒ, as long as we want to maintain an operational link with the (co-lexicographic) order of ℒ’s prefixes. Finally, we explore the relationship between two conflicting objectives: minimizing the width and minimizing the number of states of a DFA. In this context, we provide an analogue of the Myhill-Nerode Theorem for co-lexicographically ordered regular languages.

Abstract Suffix trees are an important data structure at the core of optimal solutions to many fundamental string problems, such as exact pattern matching, longest common substring, matching statistics, and longest repeated substring. Recent lines of research focused on extending some of these problems to vertex-labeled graphs, either by using efficient ad-hoc approaches which do not generalize to all input graphs, or by indexing difficult graphs and having worst-case exponential complexities. In the absence of an ubiquitous and polynomial tool like the suffix tree for labeled graphs, we introduce the labeled direct product of two graphs as a general tool for obtaining optimal algorithms in the worst case: we obtain conceptually simpler algorithms for the quadratic problems of string matching () and longest common substring () in labeled graphs. Our algorithms run in time linear in the size of the labeled product graph, which may be smaller than quadratic for some inputs, and their run-time is predictable, because the size of the labeled direct product graph can be precomputed efficiently. We also solve on graphs containing cycles, which was left as an open problem by Shimohira et al. in 2011. To show the power of the labeled product graph, we also apply it to solve the matching statistics () and the longest repeated string () problems in labeled graphs. Moreover, we show that our (worst-case quadratic) algorithms are also optimal, conditioned on the Orthogonal Vectors Hypothesis. Finally, we complete the complexity picture around by studying it on undirected graphs.

Indexing strings via prefix (or suffix) sorting is, arguably, one of the most successful algorithmic techniques developed in the last decades. Can indexing be extended to languages? The main contribution of this paper is to initiate the study of the sub-class of regular languages accepted by an automaton whose states can be prefix-sorted. Starting from the recent notion of Wheeler graph [Gagie et al., TCS 2017]— which extends naturally the concept of prefix sorting to labeled graphs—we investigate the properties of Wheeler languages, that is, regular languages admitting an accepting Wheeler finite automaton. We first characterize this family as the natural extension of regular languages endowed with the co-lexicographic ordering: the sorted prefixes of strings belonging to a Wheeler language are partitioned into a finite number of co-lexicographic intervals, each formed by elements from a single Myhill-Nerode equivalence class. We proceed by proving several results related to Wheeler automata: (i) We show that every Wheeler NFA (WNFA) with n states admits an equivalent Wheeler DFA (WDFA) with at most 2n – 1 – |Σ| states (Σ being the alphabet) that can be computed in O(n3) time. (ii) We describe a quadratic algorithm to prefix-sort a proper superset of the WDFAs, a O(n log n)-time online algorithm to sort acyclic WDFAs, and an optimal linear-time offline algorithm to sort general WDFAs. (iii) We provide a minimization theorem that characterizes the smallest WDFA recognizing the same language of any input WDFA. The corresponding constructive algorithm runs in optimal linear time in the acyclic case, and in O(n log n) time in the general case. (iv) We show how to compute the smallest WDFA equivalent to any acyclic DFA in nearly-optimal time. Our contributions imply new results of independent interest. Contributions (i-iii) provide a new class of NFAs for which the minimization problem can be approximated within a constant factor in polynomial time. Contribution (iv) provides a provably minimum-size solution for the well-studied problem of indexing deterministicacyclic graphs for linear-time pattern matching queries.

The main goal of this work is to propose a tool-chain capable of analyzing a data collection of temporally qualified (genetic) mutation profiles, i.e., a collection of DNA-sequences (genes) that present variations with respect to their “healthy” versions. We implemented a system consisting of a front-end, a reasoning core, and a post-processor: the first transforms the input data retrieved from medical databases into a set of logical facts, while the last displays the computation results as graphs. Concerning the reasoning core, we employed the Answer Set Programming paradigm, which is capable of deducing complex information from data. However, since the system is modular, this component can be replaced by any logic programming tool for different kinds of data analysis. Indeed, we tested the use of a probabilistic inductive logic programming core.

String attractors [STOC 2018] are combinatorial objects recently introduced to unify all known dictionary compression techniques in a single theory. A set $Γ\subseteq [1..n]$ is a $k$-attractor for a string $S\in[1..σ]^n$ if and only if every distinct substring of $S$ of length at most $k$ has an occurrence straddling at least one of the positions in $Γ$. Finding the smallest $k$-attractor is NP-hard for $k\geq3$, but polylogarithmic approximations can be found using reductions from dictionary compressors. It is easy to reduce the $k$-attractor problem to a set-cover instance where string's positions are interpreted as sets of substrings. The main result of this paper is a much more powerful reduction based on the truncated suffix tree. Our new characterization of the problem leads to more efficient algorithms for string attractors: we show how to check the validity and minimality of a $k$-attractor in near-optimal time and how to quickly compute exact and approximate solutions. For example, we prove that a minimum $3$-attractor can be found in optimal $O(n)$ time when $σ\in O(\sqrt[3+ε]{\log n})$ for any constant $ε>0$, and $2.45$-approximation can be computed in $O(n)$ time on general alphabets. To conclude, we introduce and study the complexity of the closely-related sharp-$k$-attractor problem: to find the smallest set of positions capturing all distinct substrings of length exactly $k$. We show that the problem is in P for $k=1,2$ and is NP-complete for constant $k\geq 3$.

The Lempel-Ziv factorization (LZ77) and the Run-Length encoded Burrows-Wheeler Transform (RLBWT) are two important tools in text compression and indexing, being their sizes z and r closely related to the amount of text self-repetitiveness. In this paper we consider the problem of converting the two representations into each other within a working space proportional to the input and the output. Let n be the text length. We show that RLBWT can be converted to LZ77 in O(n log r) time and O(r) words of working space. Conversely, we provide an algorithm to convert LZ77 to RLBWT in O(n(log r + log z)) time and O(r+z) words of working space. Note that r and z can be constant if the text is highly repetitive, and our algorithms can operate with (up to) exponentially less space than naive solutions based on full decompression.

This paper considers ∃*∀* prenex sentences of pure first-order predicate calculus with equality. This is the set of formulas which Ramsey's treated in a famous article of 1930. We demonstrate that the satisfiability problem and the problem of existence of arbitrarily large models for these formulas can be reduced to the satisfiability problem for ∃*∀* prenex sentences of Set Theory (in the relators ∈, =). We present two satisfiability-preserving (in a broad sense) translations Φ ↦ $\dot{\Phi}$ and Φ ↦ Φσ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if $\dot{\Phi}$ is satisfiable (in the domain of Set Theory) then so is Φ, and if Φσ is satisfiable (again, in the domain of Set Theory) then Φ can be satisfied in arbitrarily large finite structures of pure logic. It turns out that | $\dot{\Phi}$ | = $\mathcal{O}$ (|Φ|) and |Φσ| = $\mathcal{O}$ (|Φ|2). Our main result makes use of the fact that ∃*∀* sentences, even though constituting a decidable fragment of Set Theory, offer ways to describe infinite sets. Such a possibility is exploited to glue together infinitely many models of increasing cardinalities of a given ∃*∀* logical formula, within a single pair of infinite sets.

In this paper, we show that the LZ77 factorization of a text T ε Σncan be computed in O(R log n) bits of working space and O(n log R) time, R being the number of runs in the Burrows-Wheeler transform of T (reversed). For (extremely) repetitive inputs, the working space can be as low as O(log n) bits: exponentially smaller than the text itself. Hence, our result finds important applications in the construction of repetition-aware self-indexes and in the compression of repetitive text collections within small working space.

BACKGROUND: Bisulfite treatment of DNA followed by sequencing (BS-seq) has become a standard technique in epigenetic studies, providing researchers with tools for generating single-base resolution maps of whole methylomes. Aligning bisulfite-treated reads, however, is a computationally difficult task: bisulfite treatment decreases the (lexical) complexity of low-methylated genomic regions, and C-to-T mismatches may reflect cytosine unmethylation rather than SNPs or sequencing errors. Further challenges arise both during and after the alignment phase: data structures used by the aligner should be fast and should fit into main memory, and the methylation-caller output should be somehow compressed, due to its significant size. METHODS: As far as data structures employed to align bisulfite-treated reads are concerned, solutions proposed in the literature can be roughly grouped into two main categories: those storing pointers at each text position (e.g. hash tables, suffix trees/arrays), and those using the information-theoretic minimum number of bits (e.g. FM indexes and compressed suffix arrays). The former are fast and memory consuming. The latter are much slower and light. In this paper, we try to close this gap proposing a data structure for aligning bisulfite-treated reads which is at the same time fast, light, and very accurate. We reach this objective by combining a recent theoretical result on succinct hashing with a bisulfite-aware hash function. Furthermore, the new versions of the tools implementing our ideas|the aligner ERNE-BS5 2 and the caller ERNE-METH 2|have been extended with increased downstream compatibility (EPP/Bismark cov output formats), output compression, and support for target enrichment protocols. RESULTS: Experimental results on public and simulated WGBS libraries show that our algorithmic solution is a competitive tradeoff between hash-based and BWT-based indexes, being as fast and accurate as the former, and as memory-efficient as the latter. CONCLUSIONS: The new functionalities of our bisulfite aligner and caller make it a fast and memory efficient tool, useful to analyze big datasets with little computational resources, to easily process target enrichment data, and produce statistics such as protocol efficiency and coverage as a function of the distance from target regions.

BACKGROUND: The high throughput of modern NGS sequencers coupled with the huge sizes of genomes currently analysed, poses always higher algorithmic challenges to align short reads quickly and accurately against a reference sequence. A crucial, additional, requirement is that the data structures used should be light. The available modern solutions usually are a compromise between the mentioned constraints: in particular, indexes based on the Burrows-Wheeler transform offer reduced memory requirements at the price of lower sensitivity, while hash-based text indexes guarantee high sensitivity at the price of significant memory consumption. METHODS: In this work we describe a technique that permits to attain the advantages granted by both classes of indexes. This is achieved using Hamming-aware hash functions--hash functions designed to search the entire Hamming sphere in reduced time--which are also homomorphisms on de Bruijn graphs. We show that, using this particular class of hash functions, the corresponding hash index can be represented in linear space introducing only a logarithmic slowdown (in the query length) for the lookup operation. We point out that our data structure reaches its goals without compressing its input: another positive feature, as in biological applications data is often very close to be un-compressible. RESULTS: The new data structure introduced in this work is called dB-hash and we show how its implementation--BW-ERNE--maintains the high sensitivity and speed of its (hash-based) predecessor ERNE, while drastically reducing space consumption. Extensive comparison experiments conducted with several popular alignment tools on both simulated and real NGS data, show, finally, that BW-ERNE is able to attain both the positive features of succinct data structures (that is, small space) and hash indexes (that is, sensitivity). CONCLUSIONS: In applications where space and speed are both a concern, standard methods often sacrifice accuracy to obtain competitive throughputs and memory footprints. In this work we show that, combining hashing and succinct indexing techniques, we can attain good performances and accuracy with a memory footprint comparable to that of the most popular compressed indexes.

We introduce and prove the basic properties of encodings that generalize to non-well-founded hereditarily finite sets the bijection defined by Ackermann in 1937 between hereditarily finite sets and natural numbers.

We consider the algorithmic problem of computing the maximal simulation preorder (and quotient) on acyclic labelled graphs. The acyclicity allows to exploit an inner structure on the set of nodes, that can be processed in stages according to a set-theoretic notion of rank. This idea, previously used for bisimulation computation, on the one hand improves on the performances of the ensuing procedure and, on the other hand, gives to the solution an orderly iterative flavour making the algorithmic idea more explicit. The computational complexity achieved is good as we obtain the best performing algorithm for simulation computation on acyclic graphs, in both time and space. © The Author, 2013. Published by Oxford University Press. All rights reserved.

We propose a parallel algorithm that solves the best k-mismatches alignment problem against a genomic reference using the "one sequence/multiple processes" paradigm and distributed memory. Our proposal is designed to take advantage of a computing cluster using MPI (Message Passing Interface) for communication. Our solution distributes the reference among different nodes and each sequence is processed concurrently by different nodes. When a (putative) best solution is found, the successful process propagates the information to other nodes, reducing search space and saving computation time. The distributed algorithm was developed in C++ and optimized for the PLX and FERMI supercomputers, but it is compatible with every OpenMPI-based cluster. It was included in the ERNE (Extended Randomized Numerical alignEr) package, whose aim is to provide an all-inclusive set of tools for short reads alignment and cleaning. ERNE is free software, distributed under the Open Source License (GPL V3) and can be downloaded at: http://erne.sourceforge.net. The algorithm described in this work is implemented in the ERNE-PMAP and ERNE-PBS5 programs, the former designed to align DNA and RNA sequences, while the latter is optimized for bisulphite-treated sequences.

Abstract Summary: Chimera is a Bioconductor package that organizes, annotates, analyses and validates fusions reported by different fusion detection tools; current implementation can deal with output from bellerophontes, chimeraScan, deFuse, fusionCatcher, FusionFinder, FusionHunter, FusionMap, mapSplice, Rsubread, tophat-fusion and STAR. The core of Chimera is a fusion data structure that can store fusion events detected with any of the aforementioned tools. Fusions are then easily manipulated with standard R functions or through the set of functionalities specifically developed in Chimera with the aim of supporting the user in managing fusions and discriminating false-positive results. Availability and implementation: Chimera is implemented as a Bioconductor package in R. The package and the vignette can be downloaded at bioconductor.org. Contact: [email protected] Supplementary information: Supplementary data are available at Bioinformatics online.

BACKGROUND: In recent years more than 20 assemblers have been proposed to tackle the hard task of assembling NGS data. A common heuristic when assembling a genome is to use several assemblers and then select the best assembly according to some criteria. However, recent results clearly show that some assemblers lead to better statistics than others on specific regions but are outperformed on other regions or on different evaluation measures. To limit these problems we developed GAM-NGS (Genomic Assemblies Merger for Next Generation Sequencing), whose primary goal is to merge two or more assemblies in order to enhance contiguity and correctness of both. GAM-NGS does not rely on global alignment: regions of the two assemblies representing the same genomic locus (called blocks) are identified through reads' alignments and stored in a weighted graph. The merging phase is carried out with the help of this weighted graph that allows an optimal resolution of local problematic regions. RESULTS: GAM-NGS has been tested on six different datasets and compared to other assembly reconciliation tools. The availability of a reference sequence for three of them allowed us to show how GAM-NGS is a tool able to output an improved reliable set of sequences. GAM-NGS is also a very efficient tool able to merge assemblies using substantially less computational resources than comparable tools. In order to achieve such goals, GAM-NGS avoids global alignment between contigs, making its strategy unique among other assembly reconciliation tools. CONCLUSIONS: The difficulty to obtain correct and reliable assemblies using a single assembler is forcing the introduction of new algorithms able to enhance de novo assemblies. GAM-NGS is a tool able to merge two or more assemblies in order to improve contiguity and correctness. It can be used on all NGS-based assembly projects and it shows its full potential with multi-library Illumina-based projects. With more than 20 available assemblers it is hard to select the best tool. In this context we propose a tool that improves assemblies (and, as a by-product, perhaps even assemblers) by merging them and selecting the generating that is most likely to be correct.

We define a semantics for stochastic Concurrent Constraint Programming (sCCP), a stochastic process algebra, in terms of stochastic hybrid automata with piecewise deterministic continuous dynamics. To each program we associate a lattice of hybrid models, parameterized with respect to the degree of discreteness left. We study some properties of this lattice, presenting also an alternative semantics in which the degree of discreteness can be dynamically changed.

SUMMARY: The advent of high-throughput sequencers (HTS) introduced the need of new tools in order to analyse the large amount of data that those machines are able to produce. The mandatory first step for a wide range of analyses is the alignment of the sequences against a reference genome. We present a major update to our rNA (randomized Numerical Aligner) tool. The main feature of rNA is the fact that it achieves an accuracy greater than the majority of other tools in a feasible amount of time. rNA executables and source codes are freely downloadable at http://iga-rna.sourceforge.net/. CONTACT: [email protected]; [email protected] SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

BACKGROUND: Next Generation Sequencing technologies are able to provide high genome coverages at a relatively low cost. However, due to limited reads' length (from 30 bp up to 200 bp), specific bioinformatics problems have become even more difficult to solve. De novo assembly with short reads, for example, is more complicated at least for two reasons: first, the overall amount of "noisy" data to cope with increased and, second, as the reads' length decreases the number of unsolvable repeats grows. Our work's aim is to go at the root of the problem by providing a pre-processing tool capable to produce (in-silico) longer and highly accurate sequences from a collection of Next Generation Sequencing reads. RESULTS: In this paper a seed-and-extend local assembler is presented. The kernel algorithm is a loop that, starting from a read used as seed, keeps extending it using heuristics whose main goal is to produce a collection of error-free and longer sequences. In particular, GapFiller carefully detects reliable overlaps and operates clustering similar reads in order to reconstruct the missing part between the two ends of the same insert. Our tool's output has been validated on 24 experiments using both simulated and real paired reads datasets. The output sequences are declared correct when the seed-mate is found. In the experiments performed, GapFiller was able to extend high percentages of the processed seeds and find their mates, with a false positives rate that turned out to be nearly negligible. CONCLUSIONS: GapFiller, starting from a sufficiently high short reads coverage, is able to produce high coverages of accurate longer sequences (from 300 bp up to 3500 bp). The procedure to perform safe extensions, together with the mate-found check, turned out to be a powerful criterion to guarantee contigs' correctness. GapFiller has further potential, as it could be applied in a number of different scenarios, including the post-processing validation of insertions/deletions detection pipelines, pre-processing routines on datasets for de novo assembly pipelines, or in any hierarchical approach designed to assemble, analyse or validate pools of sequences.

Abstract As proved recently, the satisfaction problem for all prenex formulae in the set-theoretic Bernays-Shönfinkel-Ramsey class is semi-decidable over von Neumann's cumulative hierarchy. Here that semi-decidability result is strengthened into a decidability result for the same collection of formulae.

It is shown that within the language of Set Theory, if membership is assumed to be non-well-founded à la Aczel, then one can state the existence of infinite sets by means of an ∃∃∀∀ prenex sentence. Somewhat surprisingly, this statement of infinity is essentially the one which was proposed in 1988 for well-founded sets, and it is satisfied exclusively by well-founded sets. Stating infinity inside the BSR (Bernays–Schönfinkel–Ramsey) class of the ∃*∀*-sentences becomes more challenging if no commitment is taken as whether membership is well-founded or not: for this case, we produce an ∃∃∀∀∀ -sentence, thus lowering the complexity of the quantificational prefix with respect to earlier prenex formulations of infinity. We also show that no prenex specification of infinity can have a prefix simpler than ∃∃∀∀. The problem of determining whether a BSR-sentence involving an uninterpreted predicate symbol and = can be satisfied over a large domain is then reduced to the satisfiability problem for the set theoretic class BSR subject to the ill-foundedness assumption. Envisaged enhancements of this reduction, cleverly exploiting the expressive power of the set theoretic BSR-class, add to the motivation for tackling the satisfaction problem for this class, which appears to be anything but unchallenging.

The advent of Next Generation Sequencers (NGS) has driven the necessity to design new and more sophisticated tools in order to cope with the huge amount of data produced by these novel technologies. String alignment against a genome reference is the first and most important phase in every (re)-sequencing project. Recently, distributed tools able to align large amounts of sequences using clusters or clouds of computers, have been put forward. The aim of this work is to propose a new tool named mrNA (the MPI version of the original rNA program) able to align NGS data using a cluster of computers. mrNA was designed to tackle the main computational bottleneck of all classical parallel implementation of aligners: references longer than 4 Gbp. mrNA, together with rNA, are open source programs downloadable at http://iga-rna.sourceforge.net/.

Next Generation Sequencing has totally changed genomics: we are able to produce huge amounts of data at an incredible low cost if compared to Sanger sequencing. Despite this some old problems have become even more difficult, de-novo assembly being on top of this list. In this paper we propose a novel method that aims at improving de-novo assembly in presence of a closely related reference. The idea is to combine de-novo assembly and reference guided assembly in order to obtain an enhanced assembly.

Abstract As is well-known, the Bernays-Schönfinkel-Ramsey class of all prenex ∃*∀*-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are ∈ and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper.

Many software tools are currently available to solve the hard goal of assembling millions of fragments produced in sequencing projects. Such a variety includes packages for long and short reads, generated by classical and next-generation sequencing technologies. Often the result produced by different tools can diverge-sometime significantly-for many reasons: the underlying algorithm, the data structures employed, the heuristics implemented, default parameters, etc. On the ground of the above considerations, we were motivated in developing a methodology which may both guide in a comparison of different assembler's output and improve the overall quality of the genome assembly sequences,by merging the sequences produced by different assembly programs.

BACKGROUND: The construction of a whole-genome physical map has been an essential component of numerous genome projects initiated since the inception of the Human Genome Project. Its usefulness has been proved for whole-genome shotgun projects as a post-assembly validation and recently it has also been used in the assembly step to constrain on BACs positions. Fingerprinting is usually the method of choice for construction of physical maps. A clone fingerprint is composed of true peaks representing real fragments and background peaks, mainly composed of E. coli genomic DNA, partial digestions, star activity by-products, and machine background. High-throughput fingerprinting leads to the production of thousands of BAC clone fingerprints per day. That is why background peaks removal has become an important issue and needs to be automatized, especially in capillary electrophoresis based fingerprints. RESULTS: At the moment, the only tools available for such a task are GenoProfiler and its descendant FPMiner. The large variation in the quality of fingerprints that is usually present in large fingerprinting projects represents a major difficulty in the correct removal of background peaks that has only been partially addressed by the methods so far adopted that all require a long manual optimization of parameters. Thus, we implemented a new data-independent tool, FPB (FingerPrint Background removal), suitable for large scale projects as well as mapping of few clones. CONCLUSION: FPB is freely available at http://www.appliedgenomics.org/tools.php. FPB was used to remove the background from all fingerprints of three grapevine physical map projects. The first project consists of about 50,000 fingerprints, the second one consists of about 70,000 fingerprints, and the third one consists of about 45,000 fingerprints. In all cases a successful assembly was built.

We present a method to simulate biochemical networks described by the graphical notation of Molecular Interaction Maps within stochastic Concurrent Constraint Programming. Such maps are compact, as they represent implicitly a wide set of reactions, and therefore not easy to simulate with standard tools. The encoding we propose is capable to stochastically simulate these maps implicitly, without generating the full list of reactions.

Abstract Being able to state the principles which lie deepest in the foundations of mathematics by sentences in three variables is crucially important for a satisfactory equational rendering of set theories along the lines proposed by Alfred Tarski and Steven Givant in their monograph of 1987. The main achievement of this paper is the proof that the ‘kernel’ set theory whose postulates are extensionality. (E), and single-element adjunction and removal. (W) and (L), cannot be axiomatized by means of three-variable sentences. This highlights a sharp edge to be crossed in order to attain an ‘algebraization’ of Set Theory. Indeed, one easily shows that the theory which results from the said kernel by addition of the null set axiom, (N), is in its entirety expressible in three variables.

In this paper we describe an algorithm for the localization of structured models, i.e. sequences of (simple) motifs and distance constraints. It basically combines standard pattern matching procedures with a constraint satisfaction solver, and it has the ability, not present in similar tools, to search for partial matches. A significant feature of our approach, especially in terms of efficiency for the application context, is that the (potentially) exponentially many solutions to the considered problem are represented in compact form as a graph. Moreover, the time and space necessary to build the graph are linear in the number of occurrences of the component patterns.

We propose an alternative way to represent graphs via OBDDs based on the observation that a partition of the graph nodes allows sharing among the employed OBDDs. In the second part of the paper we present a method to compute at the same time the quotient w.r.t. the maximum bisimulation and the OBDD representation of a given graph. The proposed computation is based on an OBDD-rewriting of the notion of Ackermann encoding of hereditarily finite sets into natural numbers.

In this paper, a generalization of Kamp's theorem relative to the functional completeness of the until operator is proved. Such a generalization consists in showing the functional completeness of more expressive temporal operators with respect to the extension of the first‐order theory of linear orders MFO[<] with an extra binary relational symbol. The result is motivated by the search of a modal language capable of expressing properties and operators suitable to model time granularity in ω‐layered temporal structures.

The first-order theories of lists, multisets, compact lists (i.e., lists where the number of contiguous occurrences of each element is immaterial), and sets are introduced via axioms. Such axiomatizations are shown to be very well-suited for the integration with free functor symbols governed by the classical Clark's axioms in the context of (Constraint) Logic Programming. Adaptations of the extensionality principle to the various theories taken into account is then exploited in the design of unification algorithms for the considered data structures. All the theories presented can be combined providing frameworks to deal with several of the proposed data structures simultaneously. The unification algorithms proposed can be combined (merged) as well, to produce engines for such combination theories.

We investigate modal deduction through translation into standard logic and set theory. In a previous paper, using a set-theoretic translation method, we proved that derivability in the minimal modal logic K, corresponds precisely to derivability in a weak, computationally attractive set theory ω In this paper, this approach is shown equivalent to working with standard first-order translations of modal formulae in a theory of general frames. The employed techniques are mainly model-theoretic and set-theoretic, and they admit extensions to richer languages and modal deductive systems than that of basic modal logic. Some of these extensions are discussed in the last part of the paper.

In this paper we present a theoretical basis justifying the incorporation of decidability results for a first-order theory T into an automated theorem prover for T. We state rules which extend resolution using decidability results relative to T in both the ground and the non-ground case, and prove the correctness and completeness of these rules. This is done by considering the ground case of such theories first, and then by applying a straightforward lifting argument. Examples are given illustrating the inference speed-ups which can be obtained by considering decision procedures with resolution-based inference.

Abstract The axiom of infinity can be expressed by stating the existence of sets satisfying a formula which involves restricted universal quantifiers only, even if the axiom of foundation is not assumed.