Vitor Greati

We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level \(\mathbf{F}_{\omega^\omega}\) of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman’s Lemma).

Most non-classical logics are subclassical, that is, every inference/theorem they validate is also valid classically. A notable exception is the three-valued propositional Logic of Ordinary Discourse (OL) proposed and extensively motivated by W.S. Cooper as a more adequate candidate for formalizing everyday reasoning (in English). OL challenges classical logic not only by rejecting some theses, but also by accepting non-classically valid principles, such as so-called Aristotle’s and Boethius’ theses. Formally, OL shows a number of unusual features – it is non-structural, connexive, paraconsistent and contradictory – making it all the more interesting for the mathematical logician. We present our recent findings on OL and its structural companion (that we call sOL). We introduce Hilbert-style multiple-conclusion calculi for OL and sOL that are both modular and analytic, and easily allow us to obtain single-conclusion axiomatizations. We prove that sOL is algebraizable and single out its equivalent semantics, which turns out to be a discriminator variety generated by a three-element algebra. Having observed that sOL can express the connectives of other three-valued logics, we prove that it is definitionally equivalent to an expansion of the three- valued logic J3 of D’Ottaviano and da Costa, itself an axiomatic extension of paraconsistent Nelson logic.

Multiple-conclusion Hilbert-style systems allow us to finitely axiomatize every logic defined by a finite matrix. Having obtained such axiomatizations for Paraconsistent Weak Kleene and Bochvar–Kleene logics, we modify them by replacing the multiple-conclusion rules with carefully selected single-conclusion ones. In this way we manage to introduce the first finite Hilbert-style single-conclusion axiomatizations for these logics.

Perfect paradefinite algebras are De Morgan algebras expanded with a perfection (or classicality) operation. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix, studied in depth by Gomes et al. (2022) from both the algebraic and the proof-theoretical perspectives. We continue hereby that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand such algebra with this connective and study the (self-extensional) Set-Set and Set-Fmla order-preserving logics, as well as the T-assertional logics of the variety induced by the new algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil’s `symmetric modal logic’. For the Set-Set logic, in particular, the axiomatization we obtain is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property.

In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Fermüller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. We discuss their main properties (related to completeness, decidability and proof search) and make a systematic comparison between both formalisms. We observe that either of the following strategies are pursued: (i) expanding the metalanguage of the formalism (via labels or types) or (ii) generalizing the usual notion of subformula property (as done in recent work by C. Caleiro and S. Marcelino) while remaining as close as possible to the original language of the logic. In both cases, desirable requirements are to guarantee the decidability of the associated symbolic procedure, as well as the possibility of an effective proof search. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.

The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional) logics determined by (non-deterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a two-dimensional logical matrix (or B-matrix) by the combination of two (possibly partial) non-deterministic logical matrices. We will show that such a combination may result in B-matrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolation, and we will use this result to show that one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a well-known logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a one-dimensional (generalized) Hilbert-style system. Then, taking advantage of a known 5-valued non-deterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a B-matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic.

The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to reason over bilateralist judgments using symmetrical two-dimensional analytical Hilbert-style calculi. We also provide a proof-search algorithm for finite analytic calculi that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned calculus.

The present study shows how any De Morgan algebra may be enriched by a ‘perfection operator’ that allows one to express the Boolean properties of negation-consistency and negation-determinedness. The corresponding variety of ‘perfect paradefinite algebras’ (PP-algebras) is shown to be term-equivalent to the variety of involutive Stone algebras, introduced by R. Cignoli and M. Sagastume, and more recently studied from a logical perspective by M. Figallo and L. Cantú. Such equivalence then plays an important role in the investigation of the 1-assertional logic and also the order-preserving logic asssociated to the PP-algebras. The latter logic, which we call PP≤, happens to be characterised by a single 6-valued matrix and consists very naturally in a Logic of Formal Inconsistency and Formal Undeterminedness. The logic PP≤ is here axiomatised, by means of an analytic finite Hilbert-style calculus, and a related axiomatization procedure is presented that covers the logics of other classes of De Morgan algebras as well as super-Belnap logics enriched by a perfection connective.

License plates are the primary source of vehicle identification data used in a wide range of applications including law enforcement, electronic tolling, and access control amongst others. License plate detection (LPD) is a critical process in automatic license plate recognition (ALPR) that reduces complexity by delimiting the search space for subsequent ALPR stages. It is complicated by unfavourable factors including environmental conditions, occlusion, and license plate variation. As such, it requires training models on substantial volumes of relevant images per use case. In 2018, the new Mercosur standard came in to effect in four South American countries. Access to large volumes of actual Mercosur license plates with sufficient presentation variety is a significant challenge for training supervised models for LPD, thereby adversely impacting the efficacy of ALPR in Mercosur countries. This paper presents a novel license plate embedding methodology for generating large volumes of accurate Mercosur license plate images sufficient for training supervised LPD. We validate this methodology with a deep learning-based ALPR using a convolutional neural network trained exclusively with synthetic data and tested with real parking lot and traffic camera images. Experiment results achieve detection accuracy of 95% and an average running time of 40 ms.

Mercosur (a.k.a. Mercosul) is a trade bloc comprising five South American countries. In 2018, a unified Mercosur license plate model was rolled out. Access to large volumes of ground truth Mercosur license plates with sufficient presentation variety is a significant challenge for training supervised models for license plate detection (LPD) in automatic license plate recognition (ALPR) systems. To address this problem, a Mercosur license plate generator was developed to generate artificial license plate images meeting the new standard with sufficient variety for ALPR training purposes. This includes images with variation due to occlusions and environmental conditions. An embedded system was developed for detecting legacy license plates in images of real scenarios and overwriting these with artificially generated Mercosur license plates. This data set comprises 3,829 images of vehicles with synthetic license plates that meet the new Mercosur standard in real scenarios, and equivalent number of text files containing label information for the images, all organized in a CSV file with compiled image file paths and associated labels.

Low vision is characterized by visual impairment even after treatment or medical correction, causing a number of impacts on the life of individuals. Thus, the use of assistive devices is essential to mitigate the effects of visual loss. Most of the different optical devices currently available are costly, which hinders their acquisition. The present study aimed at creating a wearable optical device for low vision, using low-cost 3D impression technologies. This is a descriptive experimental study, divided into 7 stages: ideation and creation, 3D modeling, 3D printing of structural parts, development of an original application, assembly, tests and calibration. During the first 3 stages, we created a head support onto which a smartphone could be attached as well as an image transmission and capturing module. Next, an application was developed to send the module images to the smartphone. Finally, the ensemble was calibrated with the help of a volunteer with low vision. A functional wearable optical device was developed in the form of an MVP (minimum viable product), which underwent tests and a number of functionality adjustments. The study resulted in the creation of an MVP that will be perfected through industrial modifications. However, the authors of this study are in the process of validating the device for use in subjects with low vision.

Industries are considered data rich but information poor environments. Mainly due to systems design restrictions, to the lack of adequate processing power and to a sector culture notably focused on collecting, selecting, storing and preserving historical series in on-demand access repositories, massive data generated in industrial operations is traditionally neglected (or simply took aside). This huge amount of unprocessed data resting in these repositories is a latent and rich source of information that could be used to improve industrial processes. This work then proposes an approach in which an elastic processing engine is designed to be plugged-in to currently installed industrial information infrastructure to provide it with the ability of performing visual analytics on massive industrial data. A case study where an interactive visualization application is made possible in real-world industrial data scenario of over 100 million records is presented to attest the effectiveness and potential of the proposed approach in enabling interactive visualizations to Industrial Big Data.

Automated license plate recognition (ALPR) technology is a powerful technology enabling more efficient and effective law enforcement, security, payment collection, and research. A common license plate standard was adopted by the member states of the Mercosur trading bloc (Argentina, Brazil, Paraguay and Uruguay) and consequently requires an upgrade to the ALPR software used by law enforcement and industry. Due to the scarcity of real license plate images, training state-of-the-art supervised detectors is unfeasible unless data augmentation techniques and synthetic training data are used. This paper presents an accurate and efficient automated Mercosur license plate detector using a Convolutional Neural Network (CNN) trained exclusively with synthetic imagery. In order to obtain the synthetic training data, Mercosur license plates were faithfully reproduced. Digital image processing techniques were employed to reduce the domain gap and a CNN with basic image manipulation was used to embed the artificial licensed plates in to realistic contexts. The trained model was then validated on real images captured from a parking lot and a publicly available traffic monitoring video stream. The results of experiments suggest detection accuracy of about 95% and an average running time of 40 milliseconds.

The treatment and recuperation of hydric resources portray recurrent challenges and demand alternative processes and technologies. The removal of hardness and metal ions from water are necessary in certain sources of human consumption and for industrial purposes. In this work, sodium-modified vermiculite was investigated toward the removal of calcium ions in aqueous medium. The effects of adsorbent dosage, contact time, initial concentration of calcium ions, initial pH, and temperature were systematically studied for both raw and modified vermiculite. pH 10 was shown to be the most appropriate to conduct the experiments. Raw, sodium-modified, and postadsorption vermiculite were characterized by microstructure analysis (scanning electron microscopy, Fourier transform infrared spectroscopy, X-ray fluorescence, and X-ray diffraction). The maximum adsorption capacity was found in sodium-modified vermiculite, resulting in about 80 mg g–1. Kinetic studies were carried out to relate the experimental data to pseudo-first-order, pseudo-second-order, and Elovich models. Isotherm models (Freundlich, Langmuir, and Redlich–Peterson) were employed to describe the softening process, and thermodynamic parameters ΔG°, ΔH°, and ΔS° were determined. Results revealed a spontaneous endothermic adsorption process with pseudo-second-order kinetics and corroborated the sodium-modified vermiculite adequacy for water softening.

Industries are generally data rich but information poor environments. Massive datagenerated in industrial operations is traditionally neglected (or simply took aside) mainly due to systems design restrictions, to the lack of adequate processing power of typically installedcomputing infrastructure and to a sector culture notably focused on collecting, selecting,storing and preserving historical series in on-demand access repositories. This huge amountof unprocessed data resting in these repositories is a latent source of information that could beused to improve industrial processes. This work then proposes an approach in which a propercomputing power processing engine is plugged-in to current industrial information infrastructureto provide it with the ability of handling massive industrial data. Testing on real-world industrialdata volumes of 5GB, 50GB and 100GB attested the effectiveness and potential of the proposedapproach in dealing with Industrial Big Data.

This paper presents an IoT platform for Smart Cities designed for the integration of security agentsin the task of locating vehicles of interest through license plate recognition and queries to external databases. The platform is composed by an Android application capable of performing real time license plate recognitionand a server executing a RESTful API designed to query external databases and integrate the application users. The adopted recognition method uses the text recognizer implemented in the Mobile Vision API by Google, and specific heuristics for results adequacy and refinement. Experiments were conducted considering four situations of movement of the users with respect to the vehicles in the field of view, represented by photographs and frames from video streams recorded in real open urban scenarios, revealing 86.6% of average accuracy. The phases oflicense plate recognition in the smartphone, communication with the API and notification of the interested users showed satisfactory efficiency, demonstrating the feasibility of the platform concept.

This paper presents a method for brazilian automatic license plate recognition considering images with good illumination and alignment conditions, with lack of illumination, with shadows and with some inclination, taken 1m to 7m far, cases rarely seen in the literature. Images were obtained in a parking lot, during the morning and the afternoon, without environment restrictions. License plate extraction is performed by a cascade of Haar-like features classifiers, built using the AdaBoost algorithm. Filters based on mathematical morphology are used to binarize the plate. Characters are segmented by connected components labelling and are recognized by template matching. Results showed 81.75% of accuracy with average processing times of 210ms and 1304ms for computers with quad-core processors in frequencies 2.2GHz (Dell Inspiron 5588) and 900MHz (Raspberry Pi 2 model B), respectively.

An architecture and an implementation of a system for vehicle monitoring in establishments based on automatic license plate recognition from camera images placed in parking access paths is proposed. The presented soft-ware architecture is adjustable to different sources of images and vehicle datato provide real time visualization and generation of reports about quantity, average cost, legal situation and frequency of a vehicle in an establishment. The collection of this data and the real time exhibition can reveal important infor-mation about the profile of the frequenters and inspire institutional and financialdecision takings in organizations.

This paper presents a method for Brazilian automatic license plate recognition for Smart Cities applications, considering images with good illumination and alignment conditions, with lack of illumination, with shadows and with some inclination, taken from a distance of lm to 7m. Images were obtained in a parking lot, during the morning and the afternoon, without environment restrictions. License plate extraction is performed by a cascade of Haar-like features classifiers, built using the AdaBoost algorithm. Filters based on mathematical morphology prepare candidate plates for binarization and a simple threshold rule segments them. Characters are extracted by connected components labelling and are recognized by template matching. Results showed 81.75% of accuracy with average processing times of 210ms and 1304ms for computers with quad-core processors in frequencies 2.2GHz (Dell Inspiron 5588) and 900MHz (Raspberry Pi 2 model B), respectively.

Unmanned aerial vehicles have shown to be very useful in different applications aimed at facil- itating and speeding up tasks on the civil context. Among them, one can mention commercial delivery as a strong application for the future, especially after promising initiatives from large companies, such as Amazon. However, the difficulty in precisely defining landing points is one of the factors that prevent the execution of these ideas. This paper presents a new visual approach to UAV autonomous landing by introducing a visual tag positioned over a helipad, composed by a color pattern in HSV space, and an algorithm responsible for providing the precise landing position to the control system, based on the images captured by a camera coupled to the UAV. These images are first filtered by a fuzzy classifier in order to eliminate pixels incompatible to the searched pattern. Then, the remaining pixels are grouped by color and proximity, creating clusters that, when considered as groups, may represent the searched tag. Finally, the algorithm calculates the center of the helipad relative to the vehicle. Experiments were performed with very limited hardware and have demonstrated that the solution is effective and quick enough for real time applications.

This paper proposes a visual approach based on a RGB/HSV tag to precise and autonomous landing of unmanned aerial vehicles (UAV). The proposed tag is correctly identified by an algorithm divided in four stages: hue filtering, clustering, matching and center location. The first stage is based on fuzzy matching and highlights the pixels with similar colors to the searched pattern, while ignores the pixels with different colors. The clustering stage is responsible for grouping the pixels by color and proximity. The matching stage compares the searched and found landing points. Finally, the last stage locates the center of the landing point in relation to the UAV location. The proposed approach is significantly different from the state-of-the art techniques, since it is able not only to correctly identify a designated landing point, but also to distinguish it from different landing points. It requires very low computational effort and is very suitable for real-time video applications. The algorithm was successfully used, in an online manner, for location of landing points in real-time, using very limited hardware.