Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this thesis, we tackle the problems of SMT and VMT over the theories of polynomials over the reals (NRA), over the integers (NIA), and of NRA augmented with transcendental functions (NTA). We propose a new abstraction-refinement approach called Incremental Linearization. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract domain limited to linear arithmetic with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the MathSAT SMT solver, and in the nuXmv VMT model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach. Moreover, the proposed technique is an enabler for the (nonlinear) VMT problems arising in practical scenarios with design environments such as Simulink. This capability has been achieved by integrating nuXmv with Simulink using a compilation-based approach and is evaluated on an industrial-level case study.

Approximation theory is a fundamental tool in order to study the representation theory of a ring R. Roughly speaking, it consists in determining suitable additive or abelian subcategories of the whole module category Mod-R with nice enough functorial properties. For example, torsion theory is a well suited incarnation of approximation theory. Of course, such an idea has been generalised to the additive setting itself, so that both Mod-R and other interesting categories related with R may be linked functorially. By the seminal work of Beilinson, Bernstein and Deligne (1982), the derived category of the ring turns out to admit useful torsion theories, called t-structures: they are pairs of full subcategories of D(R) whose intersection, called the heart, is always an abelian category. The so-called standard t-structure of D(R) has as its heart the module category Mod-R itself. Since then a lot of results devoted to the module theoretic characterisation of the hearts have been achieved, providing evidence of the usefulness of the t-structures in the representation theory of R. In 2020, following a research line promoted by many other authors, Saorin and Stovicek proved that the heart of any compactly generated t-structure is always a locally finitely presented Grothendieck categories (actually, this is true for any t-structure in a triangulated category with coproducts). Essentially, this means that the hearts of D(R) come equipped with a finiteness condition miming that one valid in Mod-R. In the present thesis we tackle the problem of characterising when the hearts of certain compactly generated t-structures of a commutative ring are even locally coherent. In this commutative context, after the works of Neeman and Alonso, Jeremias and Saorin, compactly generated t-structures turned out to be very interesting over a noetherian ring, for they are in bijection with the Thomason filtrations of the prime spectrum. In other words, they are classified by geometric objects, moreover their constituent subcategories have a precise cohomological description. However, if the ascending chain condition lacks, such classification is somehow partial, though provided by Hrbek. The crucial point is that the constituents of the t-structures have a different description w.r.t. that available in the noetherian setting, yet if one copies the latter for an arbitrary ring still obtains a t-structure, but it is not clear whether it must be compactly generated. Consequently, pursuing the study of the local coherence of the hearts given by a Thomason filtration, we ended by considering two t-structures. Our technique in order to face the lack of the ascending chain condition relies on a further approximation of the hearts by means of suitable torsion theories. The main results of the thesis are the following: we prove that for the so-called weakly bounded below Thomason filtrations the two t-structures have the same heart (therefore it is always locally finitely presented), and we show that they coincide if and only they are both compactly generated. Moreover, we achieve a complete characterisation of the local coherence for the hearts of the Thomason filtrations of finite length.

Semantic Image Interpretation (SII) is the process of generating a structured description of the content of an input image. This description is encoded as a labelled direct graph where nodes correspond to objects in the image and edges to semantic relations between objects. Such a detailed structure allows a more accurate searching and retrieval of images. In this thesis, we propose two well-founded methods for SII. Both methods exploit background knowledge, in the form of logical constraints of a knowledge base, about the domain of the images. The first method formalizes the SII as the extraction of a partial model of a knowledge base. Partial models are built with a clustering and reasoning algorithm that considers both low-level and semantic features of images. The second method uses the framework Logic Tensor Networks to build the labelled direct graph of an image. This framework is able to learn from data in presence of the logical constraints of the knowledge base. Therefore, the graph construction is performed by predicting the labels of the nodes and the relations according to the logical constraints and the features of the objects in the image. These methods improve the state-of-the-art by introducing two well-founded methodologies that integrate low-level and semantic features of images with logical knowledge. Indeed, other methods, do not deal with low-level features or use only statistical knowledge coming from training sets or corpora. Moreover, the second method overcomes the performance of the state-of-the-art on the standard task of visual relationship detection.

Given an elliptic curve E over Fp and an integer e ≥ 1, we define a new object, called “elliptic loop”, as the set of plane projective points over Z/p^e Z lying over E, endowed with an operation inherited by the curve addition. This object is proved to be a power-associative abelian algebraic loop. Its substructures are investigated by means of other algebraic cubics defined over the same ring, which we named “shadow curve” and “layers”. When E has trace 1, a distinctive behavior is detected and employed for producing an isomorphism attack to the discrete logarithm on this family of curves. Stronger properties are derived for small values of e, which lead to an explicit description of the infinity part and to characterizing the geometry of rational |E|-torsion points. / Data una curva ellittica E su Fp ed un intero e ≥ 1, definiamo un nuovo oggetto, chiamato "loop ellittico", come l'insieme dei punti nel piano proiettivo su Z/p^e Z che stanno sopra ad E, dotato di una operazione ereditata dalla somma di punti sulla curva. Questo oggetto si prova essere un loop algebrico con associatività delle potenze. Le sue sotto-strutture sono investigate utilizzando altre cubiche definite sullo stesso anello, che abbiamo chiamato "curva ombra" e "strati". Quando E ha traccia 1, un comportamento speciale viene notato e sfruttato per produrre un attacco di isomorfismo al problema del logaritmo discreto su questa famiglia di curve. Migliori proprietà vengono trovate per bassi valori di e, che portano ad una descrizione esplicita della parte all'infinito e alla caratterizzazione della geometria dei punti razionali di |E|-torsione.

In 2020 Parusiński and Rond proved that every algebraic set X ⊂ R^n is homeomorphic to an algebraic set X’ ⊂ R^n which is described globally (and also locally) by polynomial equations whose coefficients are real algebraic numbers. In general, the following problem was widely open: Open Problem. Is every real algebraic set homeomorphic to a real algebraic set defined by polynomial equations with rational coefficients? The aim of my PhD thesis is to provide classes of real algebraic sets that positively answer to above Open Problem. In Chapter 1 I introduce a new theory of real and complex algebraic geometry over subfields recently developed by Fernando and Ghiloni. In particular, the main notion to outline is the so called R|Q-regularity of points of a Q-algebraic set X ⊂ R^n. This definition suggests a natural notion of a Q-nonsingular Q-algebraic set X ⊂ R^n. The study of Q-nonsingular Q-algebraic sets is the main topic of Chapter 2. Then, in Chapter 3 I introduce Q-algebraic approximation techniques a là Akbulut-King developed in collaboration with Ghiloni and the main consequences we proved, that are, versions ‘over Q’ of the classical and the relative Nash-Tognoli theorems. Last results can be found in in Chapters 3 & 4, respectively. In particular, we obtained a positive answer to above Open Problem in the case of compact nonsingular algebraic sets. Then, after extending ‘over Q’ the Akbulut-King blowing down lemma, we are in position to give a complete positive answer to above Open Problem also in the case of compact algebraic sets with isolated singularities in Chapter 4. After algebraic Alexandroff compactification, we obtained a positive answer also in the case of non-compact algebraic sets with isolated singularities. Other related topics are investigated in Chapter 4 such as the existence of Q-nonsingular Q-algebraic models of Nash manifolds over every real closed field and an answer to the Q-algebrization problem for germs of an isolated algebraic singularity. Appendices A & B contain results on Nash approximation and an evenness criterion for the degree of global smoothings of subanalytic sets, respectively.