اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدUniversal Horn Sentences and the Joint Embedding Property
224
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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 undecidable, even if $Phi$ is additionally Horn and the signature is binary.
قيم البحث
اقرأ أيضاً
We introduce the notion of a `pure` Abstract Elementary Class to block trivial counterexamples. We study classes of models of bipartite graphs and show: Main Theorem (cf. Theorem 3.5.2 and Corollary 3.5.6): If $(lambda_i : i le alpha<aleph_1)$ is a
strictly increasing sequence of characterizable cardinals (Definition 2.1) whose models satisfy JEP$(<lambda_0)$, there is an $L_{omega_1,omega}$ -sentence $psi$ whose models form a pure AEC and (1) The models of $psi$ satisfy JEP$(<lambda_0)$, while JEP fails for all larger cardinals and AP fails in all infinite cardinals. (2) There exist $2^{lambda_i^+}$ non-isomorphic maximal models of $psi$ in $lambda_i^+$, for all $i le alpha$, but no maximal models in any other cardinality; and (3) $psi$ has arbitrarily large models. In particular this shows the Hanf number for JEP and the Hanf number for maximality for pure AEC with Lowenheim number $aleph_0$ are at least $beth_{omega_1}$. We show that although AP$(kappa)$ for each $kappa$ implies the full amalgamation property, JEP$(kappa)$ for each kappa does not imply the full joint embedding property. We show the main combinatorial device of this paper cannot be used to extend the main theorem to a complete sentence.
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 ma
tching 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.
We show that the set of absolutely normal numbers is $mathbf Pi^0_3$-complete in the Borel hierarchy of subsets of real numbers. Similarly, the set of absolutely normal numbers is $Pi^0_3$-complete in the effective Borel hierarchy.
We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two rece
Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The HCVS se
ries of workshops aims to bring together researchers working in the two communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis. Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
