اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدHORPO with Computability Closure : A Reconstruction
49
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.
قيم البحث
اقرأ أيضاً
A semi-computable set S in a computable metric space need not be computable. However, in some cases, if S has certain topological properties, we can conclude that S is computable. It is known that if a semi-computable set S is a compact manifold with
boundary, then the computability of deltaS implies the computability of S. In this paper we examine the case when S is a 1-manifold with boundary, not necessarily compact. We show that a similar result holds in this case under assumption that S has finitely many components.
Predicate logic is the premier choice for specifying classes of relational structures. Homomorphisms are key to describing correspondences between relational structures. Questions concerning the interdependencies between these two means of characteri
zing (classes of) structures are of fundamental interest and can be highly non-trivial to answer. We investigate several problems regarding the homomorphism closure (homclosure) of the class of all (finite or arbitrary) models of logical sentences: membership of structures in a sentences homclosure; sentence homclosedness; homclosure characterizability in a logic; normal forms for homclosed sentences in certain logics. For a wide variety of fragments of first- and second-order predicate logic, we clarify these problems computational properties.
Volumetric models have become a popular representation for 3D scenes in recent years. One breakthrough leading to their popularity was KinectFusion, which focuses on 3D reconstruction using RGB-D sensors. However, monocular SLAM has since also been t
ackled with very similar approaches. Representing the reconstruction volumetrically as a TSDF leads to most of the simplicity and efficiency that can be achieved with GPU implementations of these systems. However, this representation is memory-intensive and limits applicability to small-scale reconstructions. Several avenues have been explored to overcome this. With the aim of summarizing them and providing for a fast, flexible 3D reconstruction pipeline, we propose a new, unifying framework called InfiniTAM. The idea is that steps like camera tracking, scene representation and integration of new data can easily be replaced and adapted to the users needs. This report describes the technical implementation details of InfiniTAM v3, the third version of our InfiniTAM system. We have added various new features, as well as making numerous enhancements to the low-level code that significantly improve our camera tracking performance. The new features that we expect to be of most interest are (i) a robust camera tracking module; (ii) an implementation of Glocker et al.s keyframe-based random ferns camera relocaliser; (iii) a novel approach to globally-consistent TSDF-based reconstruction, based on dividing the scene into rigid submaps and optimising the relative poses between them; and (iv) an implementation of Keller et al.s surfel-based reconstruction approach.
Locally finite omega languages were introduced by Ressayre in [Journal of Symbolic Logic, Volume 53, No. 4, p.1009-1026]. They generalize omega languages accepted by finite automata or defined by monadic second order sentences. We study here closure
properties of the family LOC_omega of locally finite omega languages. In particular we show that the class LOC_omega is neither closed under intersection nor under complementation, giving an answer to a question of Ressayre.
Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are
well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a topology-based approach to formal verification of spatial properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal logics, dating back to earlier logicians such as Tarski, where modalities describe neighbourhood. We lift the topological definitions to the more general setting of closure spaces, also encompassing discrete, graph-based structures. We extend the framework with a spatial surrounded operator, a propagation operator and with some collective operators. The latter are interpreted over arbitrary sets of points instead of individual points in space. We define efficient model checking procedures, both for the individual and the collective spatial fragments of the logic and provide a proof-of-concept tool.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
