Browse
Submit Data
Databases
API
Help

Dataset Information

0 Views

0 Connections

0 Citations

0 Reanalyses

0 Downloads

Omics score: 0

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.

ABSTRACT: In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial within some domains, such as a rectangular box and a half-plane.

SUBMITTER: Li W

PROVIDER: S-EPMC6995451 | biostudies-literature | 2020

REPOSITORIES: biostudies-literature

ACCESS DATA

Json Xml

Publications

Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL.

Li Wenda W Paulson Lawrence C LC

Journal of automated reasoning 20190403 2

In complex analysis, the winding number measures the number of times a path (counter-clockwise) winds around a point, while the Cauchy index can approximate how the path winds. We formalise this approximation in the Isabelle theorem prover, and provide a tactic to evaluate winding numbers through Cauchy indices. By further combining this approximation with the argument principle, we are able to make use of remainder sequences to effectively count the number of complex roots of a polynomial withi ...[more]

PMID: 32063661

Similar Datasets

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

Project description:We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle’s code generator. The development combines various existing formalizations such as matrices, Sturm’s theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.

| S-EPMC7089722 | biostudies-literature

Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset).

Project description:The authors universal (meta-)logical reasoning approach is demonstrated and assessed with a prominent riddle in epistemic reasoning: the Wise Men Puzzle. The presented solution puts a particular emphasis on the adequate modeling of common knowledge and it illustrates the elegance and the practical relevance of the shallow semantical embedding approach when utilized within modern proof assistant systems such as Isabelle/HOL. The contributed dataset provides supporting evidence for claims made in the article "Universal (meta-)logical reasoning: Recent successes" (Benzmüller, 2019).

| S-EPMC6468147 | biostudies-literature

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

Project description:The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

| S-EPMC7413592 | biostudies-literature

LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset).

Project description:The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical and legal theories at different conceptual layers. More concretely, it comprises, in form of a dataset (Isabelle/HOL theory files), formal encodings of multiple deontic logics, logic combinations, deontic paradoxes and normative theories in the higher-order proof assistant system Isabelle/HOL. The data were acquired through application of the LogiKEy methodology, which supports experimentation with different normative theories, in different application scenarios, and which is not tied to specific logics or logic combinations. Our workbench consolidates related research contributions of the authors and it may serve as a starting point for further studies and experiments in flexible and expressive ethical and legal reasoning. It may also support hands-on teaching of non-trivial logic formalisms in lecture courses and tutorials. The LogiKEy methodology and framework is discussed in more detail in the companion research article titled "Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support" [5].

| S-EPMC7586073 | biostudies-literature

Majorana charges, winding numbers and Chern numbers in quantum Ising models.

Project description:Mapping a many-body state on a loop in parameter space is a simple way to characterize a quantum state. The connections of such a geometrical representation to the concepts of Chern number and Majorana zero mode are investigated based on a generalized quantum spin system with short and long-range interactions. We show that the topological invariants, the Chern numbers of corresponding Bloch band, is equivalent to the winding number in the auxiliary plane, which can be utilized to characterize the phase diagram. We introduce the concept of Majorana charge, the magnitude of which is defined by the distribution of Majorana fermion probability in zero-mode states, and the sign is defined by the type of Majorana fermion. By direct calculations of the Majorana modes we analytically and numerically verify that the Majorana charge is equal to Chern numbers and winding numbers.

| S-EPMC5558019 | biostudies-other

TRUmiCount: correctly counting absolute numbers of molecules using unique molecular identifiers.

Project description:Motivation:Counting molecules using next-generation sequencing (NGS) suffers from PCR amplification bias, which reduces the accuracy of many quantitative NGS-based experimental methods such as RNA-Seq. This is true even if molecules are made distinguishable using unique molecular identifiers (UMIs) before PCR amplification, and distinct UMIs are counted instead of reads: Molecules that are lost entirely during the sequencing process will still cause underestimation of the molecule count, and amplification artifacts like PCR chimeras create phantom UMIs and thus cause over-estimation. Results:We introduce the TRUmiCount algorithm to correct for both types of errors. The TRUmiCount algorithm is based on a mechanistic model of PCR amplification and sequencing, whose two parameters have an immediate physical interpretation as PCR efficiency and sequencing depth and can be estimated from experimental data without requiring calibration experiments or spike-ins. We show that our model captures the main stochastic properties of amplification and sequencing, and that it allows us to filter out phantom UMIs and to estimate the number of molecules lost during the sequencing process. Finally, we demonstrate that the phantom-filtered and loss-corrected molecule counts computed by TRUmiCount measure the true number of molecules with considerably higher accuracy than the raw number of distinct UMIs, even if most UMIs are sequenced only once as is typical for single-cell RNA-Seq. Availability and implementation:TRUmiCount is available at http://www.cibiv.at/software/trumicount and through Bioconda (http://bioconda.github.io). Supplementary information:Supplementary information is available at Bioinformatics online.

| S-EPMC6157883 | biostudies-literature

Counting and correcting errors within unique molecular identifiers to generate absolute numbers of sequencing molecules

Project description:This SuperSeries is composed of the SubSeries listed below.

2023-06-01 | GSE218903 | GEO

Counting and correcting errors within unique molecular identifiers to generate absolute numbers of sequencing molecules [scRNA-Seq]

Project description:Unique Molecular Identifiers (UMIs) are random oligonucleotide barcodes sequences? that are critical for the removal of PCR amplification biases within both bulk and single-cell sequencing experiments. However, the impact that PCR and sequencing errors have on the accuracy of generating absolute counts of RNA molecules is underappreciated. We demonstrate that PCR errors and not sequencing errors are the main source of inaccuracy in sequencing data and that the use of UMIs synthesized with homotrimeric nucleoside building blocks provides a solution to pinpoint and remove errors, allowing absolute counting of sequenced molecules.

2023-06-01 | GSE218901 | GEO

Counting and correcting errors within unique molecular identifiers to generate absolute numbers of sequencing molecules [RNA-seq]

2023-06-01 | GSE218899 | GEO

p-adic numbers encode complex networks.

Project description:The Erdős-Rényi (ER) random graph G(n, p) analytically characterizes the behaviors in complex networks. However, attempts to fit real-world observations need more sophisticated structures (e.g., multilayer networks), rules (e.g., Achlioptas processes), and projections onto geometric, social, or geographic spaces. The p-adic number system offers a natural representation of hierarchical organization of complex networks. The p-adic random graph interprets n as the cardinality of a set of p-adic numbers. Constructing a vast space of hierarchical structures is equivalent for combining number sequences. Although the giant component is vital in dynamic evolution of networks, the structure of multiple big components is also essential. Fitting the sizes of the few largest components to empirical data was rarely demonstrated. The p-adic ultrametric enables the ER model to simulate multiple big components from the observations of genetic interaction networks, social networks, and epidemics. Community structures lead to multimodal distributions of the big component sizes in networks, which have important implications in intervention of spreading processes.

| S-EPMC7794417 | biostudies-literature

OmicsDI is part of the ELIXIR infrastructure

OmicsDI is an Elixir interoperability service. Learn more ›

Tweets

OmicsDI Databases

PRIDE
PeptideAtlas
MassIVE
JPOST Repository
Physiome Model Repository

EGA
EVA
ENA
LINCS
PAXDB
Cell Collective

MetaboLights
Metabolomics Workbench
MetabolomeExpress
GNPS
BioModels
FAIRDOMHub

ArrayExpress
dbGaP
ExpressionAtlas
GEO
NODE

Information

Databases
Help
API
Contact us
Code on GitHub
Terms of use
Submit Data