اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدJEFL: Joint Embedding of Formal Proof Libraries
161
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
The heterogeneous nature of the logical foundations used in different interactive proof assistant libraries has rendered discovery of similar mathematical concepts among them difficult. In this paper, we compare a previously proposed algorithm for matching concepts across libraries with our unsupervised embedding approach that can help us retrieve similar concepts. Our approach is based on the fasttext implementation of Word2Vec, on top of which a tree traversal module is added to adapt its algorithm to the representation format of our data export pipeline. We compare the explainability, customizability, and online-servability of the approaches and argue that the neural embedding approach has more potential to be integrated into an interactive proof assistant.
قيم البحث
اقرأ أيضاً
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, sp
ecifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented tremendous theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution and our experiences will prove valuable to others undertaking such efforts.
Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER and FaCT++,
have been implemented, but these provers themselves have not been yet certified. In order to ensure the soundness of derivations in these DLs, it is necessary to formally verify the deductions applied by these reasoners. Formal methods offer powerful tools for the specification and verification of proof procedures, among them there are methods for proving properties such as soundness, completeness and termination of a proof procedure. In this paper, we present the definition of a proof procedure for the Description Logic ALC, based on a semantic tableau method. We ensure validity of our prover by proving its soundness, completeness and termination properties using Isabelle proof assistant. The proof proceeds in two phases, first by establishing these properties on an abstract level, and then by instantiating them for an implementation based on lists.
The finite models of a universal sentence $Phi$ are the age of a structure if and only if $Phi$ has the joint embedding property. We prove that the computational problem whether a given universal sentence $Phi$ has the joint embedding property is und
ecidable, even if $Phi$ is additionally Horn and the signature is binary.
We present a collection of modular open source C++ libraries for the development of logic synthesis applications. These libraries can be used to develop applications for the design of classical and emerging technologies, as well as for the implementa
tion of quantum compilers. All libraries are well documented and well tested. Furthermore, being header-only, the libraries can be readily used as core components in complex logic synthesis systems.
In recent years, knowledge graph embedding becomes a pretty hot research topic of artificial intelligence and plays increasingly vital roles in various downstream applications, such as recommendation and question answering. However, existing methods
for knowledge graph embedding can not make a proper trade-off between the model complexity and the model expressiveness, which makes them still far from satisfactory. To mitigate this problem, we propose a lightweight modeling framework that can achieve highly competitive relational expressiveness without increasing the model complexity. Our framework focuses on the design of scoring functions and highlights two critical characteristics: 1) facilitating sufficient feature interactions; 2) preserving both symmetry and antisymmetry properties of relations. It is noteworthy that owing to the general and elegant design of scoring functions, our framework can incorporate many famous existing methods as special cases. Moreover, extensive experiments on public benchmarks demonstrate the efficiency and effectiveness of our framework. Source codes and data can be found at url{https://github.com/Wentao-Xu/SEEK}.
الأسئلة المقترحة
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
