China
Africa
Explore chapters and articles related to this topic
Replacing Turing Tape with a Fractal Tape
Published in Anirban Bandyopadhyay, Nanobrain, 2020
Undecidability, Halting problem and the necessity of self-programmable algorithm: The most arrogant statement about the universe is the following: anything that can be “computed” can be computed by some Turing machine. Turing himself in 1938 started to find the limitations of the Turing machine (Turing, 1939). Undecidability is not possible to resolve using Turing machines. One example problem is a question, how much time would require to find all prime numbers? Now, once this question is asked, the Turing machine is not designed to simulate the future and accordingly create an algorithm (self-taught software), estimate computing time feasibility of solution making and halt if it cannot finish within finite time (halting problem). Each clock in the time crystal is an infinite loop, thus, an infinite loop cannot fall into an infinite loop and get locked.
D
Published in Phillip A. Laplante, Dictionary of Computer Science, Engineering, and Technology, 2017
decidability a property of sets for which one can determine whether something is a member in a finite number of steps. Decidability is an important concept in computability theory. A set is said to be “decidable” if a program can be written to determine whether an element is in the set and the program will always terminate with an answer YES or NO after a finite number of steps.
Bracketing backward reach sets of a dynamical system
Published in International Journal of Control, 2020
Thomas Le Mézo, Luc Jaulin, Benoît Zerr
Lyapunov-based methods (Barreiro, Aracil, & Pagano, 2002; Delanoue, Jaulin, & Cottenceau, 2006; Gonzaga, Jungers, & Daafouz, 2012; Ratschan & She, 2010), level-set methods (Biemond & Michiels, 2014; Mitchell, Bayen, & Tomlin, 2001), or barrier functions (Bouissou, Chapoutot, Djaballah, & Kieffer, 2014; Esterhuizen & Lévine, 2016) can also be considered as Eulerian since they only check the constraints on the state space and do not need to perform any integration through time. Now, these methods require a parametric expression for candidate Lyapunov-like functions (She & Xue, 2013). When the state-equation is polynomial, due to decidability of the theory of real-closed fields (Tarski, 1951), there is an algorithm that, for a given polynomial with parametric coefficients, decides whether there exist some consistent instantiations of these parameters. For the resolution of the problem, several methods exist, such as the ones based on the sum of squares (Parrilo & Lall, 2003) or on Linear Matrix Inequalities (Henrion, Lasserre, & Lofberg, 2009). When the parametric model for the Lyapunov function is nonpolynomial, interval methods which take into account some quantifier eliminations (Ratschan, 2002) can also be used.
Lattice logic as a fragment of (2-sorted) residuated modal logic
Published in Journal of Applied Non-Classical Logics, 2019
Section 5 introduces the correspondence language for PLL, by composing the modal translation of PLL into ML with the standard translation of the latter into FOL and it derives some consequences of the reduction. We derive another proof of decidability via the finite model property of the two-variable fragment of first-order logic (which was known for PLL, established in Greco and Palmigiano (2017) via a Cut elimination argument). The finite model property (FMP) is new for PLL and, as usual for FMP arguments, it leads to a high complexity bound for the satisfiability problem. However, turning to the reduction into single-sorted RML (Theorem 4.5), we can apply directly Ladner's theorem Ladner (1977), which ensures pspace complexity for PLL. The Löwenheim-Skolem property for PLL is also proven, as a consequence of the Löwenheim-Skolem property for sorted first-order logic, see Enderton (1972), or of unsorted first-order logic, after applying standard sort reduction, cf. Enderton (1972). Similarly, compactness of PLL is derived, as a consequence of compactness of (sorted, or not) first-order logic Enderton (1972). The significance of the reduction is that it provides a direct methodology for obtaining similar results for extensions of PLL with various operators, based on discrete dualities for e.g. modal lattices Hartonas (2018b) (but also for implicative, or for residuated and co-residuated lattices).
Transformation of UML class diagram into OWL Ontology
Published in Journal of Information and Telecommunication, 2020
Minh Hoang Lien Vo, Quang Hoang
The OWL2 is an ontology language for the Semantic Web. It is considered as an extension of OWL DL by adding the syntax to the representation without losing its decidability. In particular, OWL2 is capable of representing the key of a class in an ontology similar to the key of an entity type in the ER model. For ontology editing, Stanford University has introduced the open source Protégé tool, which defines ontological concepts such as classes, properties, semantic categories, and different restrictions.