Browse
Submit Data
Databases
API
Help

Dataset Information

0 Views

0 Connections

0 Citations

0 Reanalyses

0 Downloads

Omics score: 0

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

ABSTRACT: 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.

SUBMITTER: Joosten SJC

PROVIDER: S-EPMC7089722 | biostudies-literature | 2020

REPOSITORIES: biostudies-literature

ACCESS DATA

Json Xml

Similar Datasets

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

Project description: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.

| S-EPMC6995451 | 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

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.

Project description:We formally verify the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk , where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.

| S-EPMC7115093 | biostudies-literature

Identifiability and numerical algebraic geometry.

Project description:A common problem when analyzing models, such as mathematical modeling of a biological process, is to determine if the unknown parameters of the model can be determined from given input-output data. Identifiable models are models such that the unknown parameters can be determined to have a finite number of values given input-output data. The total number of such values over the complex numbers is called the identifiability degree of the model. Unidentifiable models are models such that the unknown parameters can have an infinite number of values given input-output data. For unidentifiable models, a set of identifiable functions of the parameters are sought so that the model can be reparametrized in terms of these functions yielding an identifiable model. In this work, we use numerical algebraic geometry to determine if a model given by polynomial or rational ordinary differential equations is identifiable or unidentifiable. For identifiable models, we present a novel approach to compute the identifiability degree. For unidentifiable models, we present a novel numerical differential algebra technique aimed at computing a set of algebraically independent identifiable functions. Several examples are used to demonstrate the new techniques.

| S-EPMC6910699 | biostudies-literature

Experimental Evidence for Algebraic Double-Layer Forces.

Project description:According to conventional wisdom, electric double-layer forces normally decay exponentially with separation distance. Here, we present experimental evidence of algebraically decaying double-layer interactions. We show that algebraic interactions arise in both strongly overlapping as well as counterion-only regimes, albeit the evidence is less clear for the former regime. In both of these cases, the disjoining pressure profile assumes an inverse square distance dependence. At small separation distances, another algebraic regime is recovered. In this regime, the pressure decays as the inverse of separation distance.

| S-EPMC6968886 | biostudies-literature

Detecting intermediate protein conformations using algebraic topology.

Project description:Understanding protein structure and dynamics is essential for understanding their function. This is a challenging task due to the high complexity of the conformational landscapes of proteins and their rugged energy levels. In particular, it is important to detect highly populated regions which could correspond to intermediate structures or local minima.We present a hierarchical clustering and algebraic topology based method that detects regions of interest in protein conformational space. The method is based on several techniques. We use coarse grained protein conformational search, efficient robust dimensionality reduction and topological analysis via persistent homology as the main tools. We use two dimensionality reduction methods as well, robust Principal Component Analysis (PCA) and Isomap, to generate a reduced representation of the data while preserving most of the variance in the data.Our hierarchical clustering method was able to produce compact, well separated clusters for all the tested examples.

| S-EPMC5731496 | biostudies-literature

Algebraic comparison of partial lists in bioinformatics.

Project description:The outcome of a functional genomics pipeline is usually a partial list of genomic features, ranked by their relevance in modelling biological phenotype in terms of a classification or regression model. Due to resampling protocols or to a meta-analysis comparison, it is often the case that sets of alternative feature lists (possibly of different lengths) are obtained, instead of just one list. Here we introduce a method, based on permutations, for studying the variability between lists ("list stability") in the case of lists of unequal length. We provide algorithms evaluating stability for lists embedded in the full feature set or just limited to the features occurring in the partial lists. The method is demonstrated by finding and comparing gene profiles on a large prostate cancer dataset, consisting of two cohorts of patients from different countries, for a total of 455 samples.

| S-EPMC3355159 | biostudies-literature

Algebraic signatures of convex and non-convex codes.

Project description:A convex code is a binary code generated by the pattern of intersections of a collection of open convex sets in some Euclidean space. Convex codes are relevant to neuroscience as they arise from the activity of neurons that have convex receptive fields. In this paper, we use algebraic methods to determine if a code is convex. Specifically, we use the neural ideal of a code, which is a generalization of the Stanley-Reisner ideal. Using the neural ideal together with its standard generating set, the canonical form, we provide algebraic signatures of certain families of codes that are non-convex. We connect these signatures to the precise conditions on the arrangement of sets that prevent the codes from being convex. Finally, we also provide algebraic signatures for some families of codes that are convex, including the class of intersection-complete codes. These results allow us to detect convexity and non-convexity in a variety of situations, and point to some interesting open questions.

| S-EPMC6750060 | biostudies-literature

OmicsDI is part of the ELIXIR infrastructure

OmicsDI is an Elixir interoperability service. Learn more ›

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