اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدMaking Isabelle Content Accessible in Knowledge Representation Formats
72
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and MMT that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) -- more than 12 thousand theories and locales resulting in over 65GB of OMDoc/XML. Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.
قيم البحث
اقرأ أيضاً
Treatment recommendations within Clinical Practice Guidelines (CPGs) are largely based on findings from clinical trials and case studies, referred to here as research studies, that are often based on highly selective clinical populations, referred to
here as study cohorts. When medical practitioners apply CPG recommendations, they need to understand how well their patient population matches the characteristics of those in the study cohort, and thus are confronted with the challenges of locating the study cohort information and making an analytic comparison. To address these challenges, we develop an ontology-enabled prototype system, which exposes the population descriptions in research studies in a declarative manner, with the ultimate goal of allowing medical practitioners to better understand the applicability and generalizability of treatment recommendations. We build a Study Cohort Ontology (SCO) to encode the vocabulary of study population descriptions, that are often reported in the first table in the published work, thus they are often referred to as Table 1. We leverage the well-used Semanticscience Integrated Ontology (SIO) for defining property associations between classes. Further, we model the key components of Table 1s, i.e., collections of study subjects, subject characteristics, and statistical measures in RDF knowledge graphs. We design scenarios for medical practitioners to perform population analysis, and generate cohort similarity visualizations to determine the applicability of a study population to the clinical population of interest. Our semantic approach to make study populations visible, by standardized representations of Table 1s, allows users to quickly derive clinically relevant inferences about study populations.
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we f
oresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutschs algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoners Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.
We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in wei
ghted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one. This preprint has been accepted for publication at CICM 2020.
The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires t
o build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public repository of mechanically checked solutions of IMO Problems in the interactive theorem prover Isabelle/HOL. This repository is actively maintained by students of the Faculty of Mathematics, University of Belgrade, Serbia within the course Introduction to Interactive Theorem Proving.
Special Relativity is a cornerstone of modern physical theory. While a standard coordinate model is well-known and widely taught today, several alternative systems of axioms exist. This paper reports on the formalisation of one such system which is c
loser in spirit to Hilberts axiomatic approach to Euclidean geometry than to the vector space approach employed by Minkowski. We present a mechanisation in Isabelle/HOL of the system of axioms as well as theorems relating to temporal order. Proofs and excerpts of Isabelle/Isar scripts are discussed, particularly where the formal work required additional steps, alternative approaches, or corrections to Schutz prose.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
