Combinatorial operations on sets are almost never well defined on Turing degrees, a fact so obvious that counterexamples are worth exhibiting. The case we focus on is the symmetric-difference operator; there are pairs of degrees for which the symmetric-difference operation is well defined. Some examples can be extracted from the literature, e.g. from the existence of nonzero degrees with strong minimal covers. We focus on the case of incomparable r.e. degrees for which the symmetric-difference operation is well defined.

The logic $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ was introduced in Robles and Mendéz as a paraconsistent logic which is based on Gödel’s 3-valued matrix, except that Kleene–Łukasiewicz’s negation is added to the language and is used as the main negation connective. We show that $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ is exactly the intersection of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$, the two truth-preserving 3-valued logics which are based on the same truth tables. We then construct a Hilbert-type system which has for $\to $ as its sole rule of inference, and is (...) strongly sound and complete for $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Then we show how, by adding one axiom or one new rule of inference, we get strongly sound and complete systems for $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$. Finally, we provide quasi-canonical Gentzen-type systems which are sound and complete for those logics and show that they are all analytic, by proving the cut-elimination theorem for them. (shrink)

In this paper, we show that the implication fragment of classical propositional logic is finitary for unification with parameters.

In this paper, we study two companions of a logic, viz., the left variable inclusion companion and the restricted rules companion, their nature and interrelations, especially in connection with paraconsistency. A sufficient condition for the two companions to coincide has also been proved. Two new logical systems—intuitionistic paraconsistent weak Kleene logic and paraconsistent pre-rough logic —are presented here as examples of logics of left variable inclusion. IPWK is the left variable inclusion companion of intuitionistic propositional logic and is also the (...) restricted rules companion of it. PPRL, on the other hand, is the left variable inclusion companion of pre-rough logic but differs from the restricted rules companion of it. We have discussed algebraic semantics for these logics in terms of Płonka sums. This amounts to introducing a contaminating truth value, intended to denote a state of indeterminacy. (shrink)

In this paper, we provide non-clausal tableau calculi for the maximum satisfiability problem and its variants. We discuss both basic calculi to characterize the problem and their modifications to reduce the proof size.

The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inference rules, which can be interpreted by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, (...) known as $ D_{\infty }$, to represent the $\lambda $-terms as the typical functions of set theory, where it is not allowed to apply a function to itself. Here we propose a construction of an $\infty $-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case $D_{\infty }$, and we see that the Scott topology does not provide enough information about the relationship between higher homotopies. This motivates a new line of research focused on the exploration of $\lambda $-models with the structure of a non-trivial $\infty $-groupoid to generalize the proofs of term conversion to higher-proofs in $\lambda $-calculus. (shrink)

We study the topic of realization from classical justification logics in the context of the recently introduced Gödel justification logics. We show that the standard Gödel modal logics of Caicedo and Rodriguez are not realized by the Gödel justification logics and moreover, we study possible extensions of the Gödel justification logics, which are strong enough to realize the standard Gödel modal logics. On the other hand, we study the fragments of the standard Gödel modal logics, which are realized by the (...) usual Gödel justification logics. We prove the corresponding realization theorem by using Fitting’s merging of realizations as well as appropriate hypersequent calculi on the modal side, adapting the work by Metcalfe and Olivetti. For these hypersequent calculi, we also show a cut-elimination theorem. We provide natural semantical characterizations for all of these newly introduced logics. (shrink)

We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the non-theorem. Therefore, we also obtain an embedding of the classical predicate logic of finite models into the logic of partial quasiary predicates over finite structures. As (...) a consequence, we prove that the logic of partial quasiary predicates is undecidable—more precisely, $\varSigma ^0_1$-complete—over arbitrary structures and not recursively enumerable—more precisely, $\varPi ^0_1$-complete—over finite structures. (shrink)

We prove the equivalence of the semantic version of Tarski’s theorem on the undefinability of truth with the semantic version of the diagonal lemma and also show the equivalence of a syntactic version of Tarski’s undefinability theorem with a weak syntactic diagonal lemma. We outline two seemingly diagonal-free proofs for these theorems from the literature and show that the syntactic version of Tarski’s theorem can deliver Gödel–Rosser’s incompleteness theorem.

This paper deals about dualities for bounded prelinear Hilbert algebras. In particular, we give an Esakia-style duality between the algebraic category of bounded prelinear Hilbert algebras and a category of H-spaces whose morphisms are certain continuous p-morphisms.

This article introduces some soft computing methods generally used for data analysis and flow pattern detection in fluid dynamics. These techniques decompose the original flow field as an expansion of modes, which can be either orthogonal in time, or in space or in time and space, or they can simply be selected using some sophisticated statistical techniques. The performance of these methods is tested in the turbulent wake of a wall-mounted square cylinder. This highly complex flow is suitable to show (...) the ability of the aforementioned methods to reduce the degrees of freedom of the original data by only retaining the large scales in the flow. The main result is a reduced-order model of the original flow case, based on a low number of modes. A deep discussion is carried out about how to choose the most computationally efficient method to obtain suitable reduced-order models of the flow. The techniques introduced in this article are data-driven methods that could be applied to model any type of non-linear dynamical system, including numerical and experimental databases. (shrink)

Nowadays decision making is strongly supported by the high-confident point estimations produced by deep learning algorithms. In many activities, they are sufficient for the decision-making process. However, in some other cases, confidence intervals are required too for an appropriate decision-making process. In this work, a first attempt to generate point estimations with confidence intervals for the $^{222}$Rn radiation level time series at Canfranc Underground Laboratory is presented. To predict the low-radiation periods allows correctly scheduling the unshielded periods for maintenance operations (...) in the experiments hosted in this facility. This should minimize the deposition of radioactive dust on the exposed surfaces during these unshielded periods. An approach based on deep learning with stochastic regulation is evaluated in the forecasting of point estimations and confidence intervals of the $^{222}$Rn time series and compared with a second approach based on Gaussian processes. As a consequence of this work, an evaluation of the capacity of Gaussian process and deep learning with stochastic regularization for generating point estimations and their confidence intervals for this time series is stated. (shrink)

Fall detection is a challenging task that has received the attention of the research community in the recent years. This study focuses on FD using data gathered from wearable devices with tri-axial accelerometers, developing a solution centered in elderly people living autonomously. This research includes three different ways to improve a FD method: an analysis of the event detection stage, comparing several alternatives, an evaluation of features to extract for each detected event and an appraisal of up to 6 different (...) clustering scenarios to split the samples in subsets that might enhance the classification. For each clustering scenario, a specific classification stage is defined. The experimentation includes publicly available simulated fall data sets. Results show the guidelines for defining a more robust and efficient FD method for on-wrist 3DACC wearable devices. (shrink)

Closed-loop administration of propofol for the control of hypnosis in anesthesia has evidenced an outperformance when comparing it with manual administration in terms of drug consumption and post-operative recovery of patients. Unlike other systems, the success of this strategy lies on the availability of a feedback variable capable of quantifying the current hypnotic state of the patient. However, the appearance of anomalies during the anesthetic process may result in inaccurate actions of the automatic controller. These anomalies may come from the (...) monitors, the syringe pumps, the actions of the surgeon or even from alterations in patients. This could produce adverse side effects that can affect the patient postoperative and reduce the safety of the patient in the operating room. Then, the use of anomaly detection techniques plays a significant role to avoid this undesirable situations. This work assesses different one-class intelligent techniques to detect anomalies in patients undergoing general anesthesia. Due to the difficulty of obtaining real data from anomaly situations, artificial outliers are generated to check the performance of each classifier. The final model presents successful performance. (shrink)

An intelligent model of the incremental capacity curve of an automotive lithium-ferrophosphate battery is presented. The relative heights of the two major peaks of the IC curve can be acquired from high-current discharges, thus enabling the state of health estimation of the battery while the vehicle is being operated and in certain cases, aging mechanisms can be suggested. Our model has been validated using a large dataset representing different degradation scenarios, obtained from a recently available open-source database.

An iterative learning control algorithm is presented for the force control circuit of a hydraulic cushion. A control scheme consisting of a PI controller, feed-forward and feedback-linearization is first derived. The uncertainties and nonlinearities of the proportional valve, the main system actuator, prevent the accurate tracking of the pressure reference signal. Therefore, an extra ILC FF signal is added to counteract the valve model uncertainties. The unknown valve dynamics are attenuated by adding a fourth-order low-pass filter to the iterative learning (...) control design, which is split up into two second-order low-pass filters to carry out forward and backward filtering and obtain zero-phase filtering. The addition of the ILC signal presents significant improvements in terms of settling time and overshoot of the pressure signal in the cylinder. (shrink)

The generation of synthetic data is becoming a fundamental task in the daily life of any organization due to the new protection data laws that are emerging. Because of the rise in the use of Artificial Intelligence, one of the most recent proposals to address this problem is the use of Generative Adversarial Networks. These types of networks have demonstrated a great capacity to create synthetic data with very good performance. The goal of synthetic data generation is to create data (...) that will perform similarly to the original dataset for many analysis tasks, such as classification. The problem of GANs is that in a classification problem, GANs do not take class labels into account when generating new data, it is treated as any other attribute. This research work has focused on the creation of new synthetic data from datasets with different characteristics with a Conditional Generative Adversarial Network. CGANs are an extension of GANs where the class label is taken into account when the new data is generated. The performance of our results has been measured in two different ways: firstly, by comparing the results obtained with classification algorithms, both in the original datasets and in the data generated; secondly, by checking that the correlation between the original data and those generated is minimal. (shrink)

Regression testing is applied whenever a code changes, ensuring that the modifications fixed the fault and no other faults are introduced. Due to a large number of test cases to be run, test case prioritization is one of the strategies that allows to run the test cases with the highest fault rate first. The aim of the paper is to present an optimized test case prioritization method inspired by ant colony optimization, test case prioritization–ANT. The criteria used by the optimization (...) algorithm are the number of faults not covered yet by the selected test cases and the sum of severity of the faults. The cost, i.e. time execution, for test cases is considered in the computation of the pheromone deposited on the graph’s edges. The average percentage of fault detected metric, as best selection criterion, is used to uncover maximum faults with the highest severity, and reducing the regression testing time. Several experiments are considered, detailed and discussed, comparing various algorithm parameter’s alternatives. A benchmark project is also used to validate the proposed approach. The obtained results are encouraging, being a cornerstone for new perspectives to be considered. (shrink)

Over the years, artificial neural networks have been applied successfully in many areas including IT security. Yet, neural networks can only process continuous input data. This is particularly challenging for security-related, non-continuous data like system calls of an operating system. This work focuses on five different options to preprocess sequences of system calls so that they can be processed by neural networks. These input options are based on one-hot encodings and learning word2vec, GloVe or fastText representations of system calls. As (...) an additional option, we analyse if mapping system calls to their respective kernel modules is an adequate generalization step for replacing system calls or enhancing system call data with additional information regarding their context. When performing such preprocessing steps it is important to ensure that no relevant information is lost during the process. The overall objective of system call analysis in the context of IT security is to categorize a sequence of them as benign or malicious behavior. Therefore, this scenario is used to evaluate different system call representations in a classification task. Results indicate that a broader range of attacks can be detected when enriching system call representations with corresponding kernel module information. Prior learning of embeddings does not achieve significant improvements. This work is an extension of the work by Wunderlich et al. [1] published in Advances in Intelligent Systems and Computing. (shrink)

The paper presents a novel method for the verification of security protocols’ time properties. The new method uses a translation to satisfiability modulo theories problem. In our approach, we model protocol users’ behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as a reachability property of some chosen states in an automata network. Then, the network of timed automata and the property are translated to an SMT problem and checked using an SMT-solver and a BMC algorithm. (...) We consider the most important time properties of protocol executions using specially constructed time conditions. The new method was also implemented and experimentally evaluated for six well-known SPs. We also compared our new SMT-based technique with the corresponding SAT-based approach. (shrink)

The main result proves Lyndon’s and Craig’s interpolation properties for the logic of strict implication ${\textsf{F}}$, with a purely syntactical method. A cut-free G3-style sequent calculus $ {\textsf{GF}} $ and its single-succedent variant $ \textsf{GF}_{\textsf{s}} $ are introduced. $ {\textsf{GF}} $ can be extended to a G3-variant of the sequent calculus GBPC3 for Visser’s basic logic. Also a simple syntactic proof of known embedding result of $ {\textsf{F}} $ into $ {\textsf{K}} $ is provided. An extension of $ {\textsf{F}} $, (...) namely $ \textsf{FD}, $ is considered as well. (shrink)

This paper is devoted to the problem of existence of saturated models for first-order many-valued logics. We consider a general notion of type as pairs of sets of formulas in one free variable that express properties that an element of a model should, respectively, satisfy and falsify. By means of an elementary chains construction, we prove that each model can be elementarily extended to a $\kappa $-saturated model, i.e. a model where as many types as possible are realized. In order (...) to prove this theorem we obtain, as by-products, some results on tableaux and their consistency and satisfiability and a generalization of the Tarski–Vaught theorem on unions of elementary chains. Finally, we provide a structural characterization of $\kappa $-saturation in terms of the completion of a diagram representing a certain configuration of models and mappings. (shrink)

We introduce frame-equivalence games tailored for reasoning about the size, modal depth, number of occurrences of symbols and number of different propositional variables of modal formulae defining a given frame property. Using these games, we prove lower bounds on the above measures for a number of well-known modal axioms; what is more, for some of the axioms, we show that they are optimal among the formulae defining the respective class of frames.

In this work, we propose a variant of so-called informational semantics, a technique elaborated by Voishvillo, for two infectious logics, Deutsch’s ${\mathbf{S}_{\mathbf{fde}}}$ and Szmuc’s $\mathbf{dS}_{\mathbf{fde}}$. We show how the machinery of informational semantics can be effectively used to analyse truth and falsity conditions of disjunction and conjunction. Using this technique, it is possible to claim that disjunction and conjunction can be rightfully regarded as such, a claim which was disputed in the recent literature. Both ${\mathbf{S}_{\mathbf{fde}}}$ and $\mathbf{dS}_{\mathbf{fde}}$ are formalized in (...) terms of natural deduction. This allows us to solve several problems: to develop a natural deduction calculus for ${\mathbf{S}_{\mathbf{fde}}}$ containing the standard form of disjunction elimination, to introduce the first natural deduction calculus for $\mathbf{dS}_{\mathbf{fde}}$ and to reflect the fundamental symmetry between ${\mathbf{S}_{\mathbf{fde}}}$ and $\mathbf{dS}_{\mathbf{fde}}$ on proof-theoretical level forming a convenient basis for obtaining their well-known extensions $\mathbf{K}^{\mathbf{w}}_{\mathbf{3}}$ and $\mathbf{PWK}$. (shrink)

Orthomodular posets form an algebraic formalization of the logic of quantum mechanics. A central question is how to introduce implication in such a logic. We give a positive answer whenever the orthomodular poset in question is of finite height. The crucial advantage of our solution is that the corresponding algebra, called implication orthomodular poset, i.e. a poset equipped with a binary operator of implication, corresponds to the original orthomodular poset and that its implication operator is everywhere defined. We present here (...) a complete list of axioms for implication orthomodular posets. This enables us to derive an axiomatization in Gentzen style for the algebraizable logic of orthomodular posets of finite height. (shrink)

Dynamic topological logic is a multi-modal logic that was introduced for reasoning about dynamic topological systems, i.e. structures of the form $\langle{\mathfrak{X}, f}\rangle $, where $\mathfrak{X}$ is a topological space and $f$ is a continuous function on it. The problem of finding a complete and natural axiomatization for this logic in the original tri-modal language has been open for more than one decade. In this paper, we give a natural axiomatization of $\textsf{DTL}$ and prove its strong completeness with respect to (...) the class of all dynamic topological systems. Our proof system is infinitary in the sense that it contains an infinitary derivation rule with countably many premises and one conclusion. It should be remarked that $\textsf{DTL}$ is semantically non-compact, so no finitary proof system for this logic could be strongly complete. Moreover, we provide an infinitary axiomatic system for the logic ${\textsf{DTL}}_{\mathcal{A}}$, i.e. the $\textsf{DTL}$ of Alexandrov spaces, and show that it is strongly complete with respect to the class of all dynamical systems based on Alexandrov spaces. (shrink)

Inspired by an interesting quotation from the literature, we propose four modalities, called ‘sane belief’, ‘insane belief’, ‘reliable belief’ and ‘unreliable belief’, and introduce logics with each operator as the modal primitive. We show that the four modalities constitute a square of opposition, which indicates some interesting relationships among them. We compare the relative expressivity of these logics and other related logics, including a logic of false beliefs from the literature. The four main logics are all less expressive than the (...) standard modal logic over various model classes, and the logics of sane and insane beliefs are, respectively, equally expressive as the logics of unreliable and reliable beliefs on any class of models. The logics of reliable and unreliable beliefs are then combined into a bimodal logic, which turns out to be equally expressive as the standard modal logic. Despite this, we cannot obtain a complete axiomatization of the minimal bimodal logic, by simply translating the axioms and rules of the minimal modal logic $\textbf{K}$ into the bimodal language. We then introduce a schematic modality which unifies reliable and unreliable beliefs and axiomatize it over the class of all frames and also the class of serial frames. This line of research is finally extended to unify sane and insane beliefs and some axiomatizations are given. (shrink)

A classical result by Słupecki states that a logic L is functionally complete for the 3-element set of truth-values THREE if, in addition to functionally including Łukasiewicz’s 3-valued logic Ł3, what he names the ‘$T$-function’ is definable in L. By leaning upon this classical result, we prove a general theorem for defining binary expansions of Kleene’s strong logic that are functionally complete for THREE.

Interesting as they are by themselves in philosophy and mathematics, paradoxes can be made even more fascinating when turned into proofs and theorems. For example, Russell’s paradox, which overthrew Frege’s logical edifice, is now a classical theorem in set theory, to the effect that no set contains all sets. Paradoxes can be used in proofs of some other theorems—thus Liar’s paradox has been used in the classical proof of Tarski’s theorem on the undefinability of truth in sufficiently rich languages. This (...) paradox (as well as Richard’s paradox) appears implicitly in Gödel’s proof of his celebrated first incompleteness theorem. In this paper, we study Yablo’s paradox from the viewpoint of first- and second-order logics. We prove that a formalization of Yablo’s paradox (which is second order in nature) is non-first-orderizable in the sense of George Boolos (1984). (shrink)

Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.