OpenRaiser/Intern-Atlas huggingface dataset:
Deriving Theorems in Implicational Linear Logic, Declaratively
Venue: arXiv cs.LO 2020
Year: 2020

The problem we want to solve is how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. We start by filtering for linearity the proof terms associated by our Prolog-based theorem prover for Implicational Intuitionistic Logic. This works, but using for each formula a PSPACE-complete algorithm limits it to very small formulas. We take a few walks back and forth over the bridge between proof terms and theorems, provided by the Curry-Howard isomorphism, and derive step-by-step an efficient algorithm requiring a low polynomial effort per generated theorem. The resulting Prolog program runs in O(N) space for terms of size N and generates in a few hours 7,566,084,686 theorems in the implicational fragment of Linear Intuitionistic Logic together with their proof terms in normal form. As applications, we generate datasets for correctness and scalability testing of linear logic theorem provers and training data for neural networks working on theorem proving challenges. The results in the paper, organized as a literate Prolog program, are fully replicable. Keywords: combinatorial generation of provable formulas of a given size, intuitionistic and linear logic theorem provers, theorems of the implicational fragment of propositional linear intuitionistic logic, Curry-Howard isomorphism, efficient generation of linear lambda terms in normal form, Prolog programs for lambda term generation and theorem proving.
Tabling Optimization for Contextual Abduction
Venue: arXiv cs.AI 2020
Year: 2020

Tabling for contextual abduction in logic programming has been introduced as a means to store previously obtained abductive solutions in one context to be reused in another context. This paper identifies a number of issues in the existing implementations of tabling in contextual abduction and aims to mitigate the issues. We propose a new program transformation for integrity constraints to deal with their proper application for filtering solutions while also reducing the table memory usage. We further optimize the table memory usage by selectively picking predicates to table and by pragmatically simplifying the representation of the problem. The evaluation of our proposed approach, on both artificial and real world problems, shows that they improve the scalability of tabled abduction compared to previous implementations.
Continuous Reasoning for Managing Next-Gen Distributed Applications
Venue: arXiv cs.DC 2020
Year: 2020

Continuous reasoning has proven effective in incrementally analysing changes in application codebases within Continuous Integration/Continuous Deployment (CI/CD) software release pipelines. In this article, we present a novel declarative continuous reasoning approach to support the management of multi-service applications over the Cloud-IoT continuum, in particular when infrastructure variations impede meeting application's hardware, software, IoT or network QoS requirements. We show how such an approach brings considerable speed-ups compared to non-incremental reasoning.
Enhancing Linear Algebraic Computation of Logic Programs Using Sparse Representation
Venue: arXiv cs.LO 2020
Year: 2020

Algebraic characterization of logic programs has received increasing attention in recent years. Researchers attempt to exploit connections between linear algebraic computation and symbolic computation in order to perform logical inference in large scale knowledge bases. This paper proposes further improvement by using sparse matrices to embed logic programs in vector spaces. We show its great power of computation in reaching the fixpoint of the immediate consequence operator from the initial vector. In particular, performance for computing the least models of definite programs is dramatically improved in this way. We also apply the method to the computation of stable models of normal programs, in which the guesses are associated with initial matrices, and verify its effect when there are small numbers of negation. These results show good enhancement in terms of performance for computing consequences of programs and depict the potential power of tensorized logic programs.
Research Summary on Implementing Functional Patterns by Synthesizing Inverse Functions
Venue: arXiv cs.PL 2020
Year: 2020

In this research summary we present our recent work on implementing functional patterns with inverse functions in the lazy functional-logic programming language Curry. Our goal is the synthesis of the inverse of any given function in Curry itself. The setting of a functional-logic language especially allows the inversion of non-injective functions. In general, inverse computation is a non-trivial problem in lazy programming languages due to their non-strict semantics. We are so far able to directly derive the inverse function for a limited class of functions, namely those consisting of rules that do not involve both extra variables and non-linear right-hand sides. Because the synthesized definitions are based on standard code, known optimizations techniques can be applied to them. For all other functions we can still provide an inverse function by using non-strict unification.
Model-Driven Requirements for Humans-on-the-Loop Multi-UAV Missions
Venue: arXiv cs.SE 2020
Year: 2020

The use of semi-autonomous Unmanned Aerial Vehicles (UAVs or drones) to support emergency response scenarios, such as fire surveillance and search-and-rescue, has the potential for huge societal benefits. Onboard sensors and artificial intelligence (AI) allow these UAVs to operate autonomously in the environment. However, human intelligence and domain expertise are crucial in planning and guiding UAVs to accomplish the mission. Therefore, humans and multiple UAVs need to collaborate as a team to conduct a time-critical mission successfully. We propose a meta-model to describe interactions among the human operators and the autonomous swarm of UAVs. The meta-model also provides a language to describe the roles of UAVs and humans and the autonomous decisions. We complement the meta-model with a template of requirements elicitation questions to derive models for specific missions. We also identify common scenarios where humans should collaborate with UAVs to augment the autonomy of the UAVs. We introduce the meta-model and the requirements elicitation process with examples drawn from a search-and-rescue mission in which multiple UAVs collaborate with humans to respond to the emergency. We then apply it to a second scenario in which UAVs support first responders in fighting a structural fire. Our results show that the meta-model and the template of questions support the modeling of the human-on-the-loop human interactions for these complex missions, suggesting that it is a useful tool for modeling the human-on-the-loop interactions for multi-UAVs missions.
An Incentive Mechanism for Federated Learning in Wireless Cellular network: An Auction Approach
Venue: arXiv cs.LG 2020
Year: 2020

Federated Learning (FL) is a distributed learning framework that can deal with the distributed issue in machine learning and still guarantee high learning performance. However, it is impractical that all users will sacrifice their resources to join the FL algorithm. This motivates us to study the incentive mechanism design for FL. In this paper, we consider a FL system that involves one base station (BS) and multiple mobile users. The mobile users use their own data to train the local machine learning model, and then send the trained models to the BS, which generates the initial model, collects local models and constructs the global model. Then, we formulate the incentive mechanism between the BS and mobile users as an auction game where the BS is an auctioneer and the mobile users are the sellers. In the proposed game, each mobile user submits its bids according to the minimal energy cost that the mobile users experiences in participating in FL. To decide winners in the auction and maximize social welfare, we propose the primal-dual greedy auction mechanism. The proposed mechanism can guarantee three economic properties, namely, truthfulness, individual rationality and efficiency. Finally, numerical results are shown to demonstrate the performance effectiveness of our proposed mechanism.
Distributed Structured Actor-Critic Reinforcement Learning for Universal Dialogue Management
Venue: arXiv cs.CL 2020
Year: 2020

The task-oriented spoken dialogue system (SDS) aims to assist a human user in accomplishing a specific task (e.g., hotel booking). The dialogue management is a core part of SDS. There are two main missions in dialogue management: dialogue belief state tracking (summarising conversation history) and dialogue decision-making (deciding how to reply to the user). In this work, we only focus on devising a policy that chooses which dialogue action to respond to the user. The sequential system decision-making process can be abstracted into a partially observable Markov decision process (POMDP). Under this framework, reinforcement learning approaches can be used for automated policy optimization. In the past few years, there are many deep reinforcement learning (DRL) algorithms, which use neural networks (NN) as function approximators, investigated for dialogue policy.
A Constraint Programming-based Job Dispatcher for Modern HPC Systems and Applications
Venue: arXiv cs.AI 2020
Year: 2020

Constraint Programming (CP) is a well-established area in AI as a programming paradigm for modelling and solving discrete optimization problems, and it has been been successfully applied to tackle the on-line job dispatching problem in HPC systems including those running modern applications. The limitations of the available CP-based job dispatchers may hinder their practical use in today's systems that are becoming larger in size and more demanding in resource allocation. In an attempt to bring basic AI research closer to a deployed application, we present a new CP-based on-line job dispatcher for modern HPC systems and applications. Unlike its predecessors, our new dispatcher tackles the entire problem in CP and its model size is independent of the system size. Experimental results based on a simulation study show that with our approach dispatching performance increases significantly in a large system and in a system where allocation is nontrivial.
Visual Methods for Sign Language Recognition: A Modality-Based Review
Venue: arXiv cs.CV 2020
Year: 2020

Sign language visual recognition from continuous multi-modal streams is still one of the most challenging fields. Recent advances in human actions recognition are exploiting the ascension of GPU-based learning from massive data, and are getting closer to human-like performances. They are then prone to creating interactive services for the deaf and hearing-impaired communities. A population that is expected to grow considerably in the years to come. This paper aims at reviewing the human actions recognition literature with the sign-language visual understanding as a scope. The methods analyzed will be mainly organized according to the different types of unimodal inputs exploited, their relative multi-modal combinations and pipeline steps. In each section, we will detail and compare the related datasets, approaches then distinguish the still open contribution paths suitable for the creation of sign language related services. Special attention will be paid to the approaches and commercial solutions handling facial expressions and continuous signing.
A Fuzzy Logic Controller for Tasks Scheduling Using Unreliable Cloud Resources
Venue: arXiv cs.DC 2020
Year: 2020

The Cloud infrastructure offers to end users a broad set of heterogenous computational resources using the pay-as-you-go model. These virtualized resources can be provisioned using different pricing models like the unreliable model where resources are provided at a fraction of the cost but with no guarantee for an uninterrupted processing. However, the enormous gamut of opportunities comes with a great caveat as resource management and scheduling decisions are increasingly complicated. Moreover, the presented uncertainty in optimally selecting resources has also a negatively impact on the quality of solutions delivered by scheduling algorithms. In this paper, we present a dynamic scheduling algorithm (i.e., the Uncertainty-Driven Scheduling - UDS algorithm) for the management of scientific workflows in Cloud. Our model minimizes both the makespan and the monetary cost by dynamically selecting reliable or unreliable virtualized resources. For covering the uncertainty in decision making, we adopt a Fuzzy Logic Controller (FLC) to derive the pricing model of the resources that will host every task. We evaluate the performance of the proposed algorithm using real workflow applications being tested under the assumption of different probabilities regarding the revocation of unreliable resources. Numerical results depict the performance of the proposed approach and a comparative assessment reveals the position of the paper in the relevant literature.
Football and externalities: Using mathematical modelling to predict the changing fortunes of Newcastle United
Venue: arXiv cs.CY 2020
Year: 2020

The Public Investment Fund (PIF), is Saudi Arabia's sovereign wealth fund. It is one of the world's largest sovereign wealth funds, with an estimated net capital of $382 billion. It was established to invest funds on behalf of the Government of Saudi Arabia. Saudi Arabia is aiming to transfer the PIF from a mere local authority to the world's largest sovereign fund. Thus, PIF is working to manage $400 billion worth of assets by 2020. It was with this Public Investment Fund that Saudi Arabia decided to buy out the football club- Newcastle United FC- a mid-table club of the premier league. In this paper, we aim to forecast the investment levels and the subsequent improve in the league position of Newcastle United FC using the model of another premier league club- Manchester City as the base. We employ the DiD approach of logistical regression through Python. Keywords: Regression, Investment, Football, Forecasting
When Deep Reinforcement Learning Meets Federated Learning: Intelligent Multi-Timescale Resource Management for Multi-access Edge Computing in 5G Ultra Dense Network
Venue: arXiv cs.NI 2020
Year: 2020

Ultra-dense edge computing (UDEC) has great potential, especially in the 5G era, but it still faces challenges in its current solutions, such as the lack of: i) efficient utilization of multiple 5G resources (e.g., computation, communication, storage and service resources); ii) low overhead offloading decision making and resource allocation strategies; and iii) privacy and security protection schemes. Thus, we first propose an intelligent ultra-dense edge computing (I-UDEC) framework, which integrates blockchain and Artificial Intelligence (AI) into 5G ultra-dense edge computing networks. First, we show the architecture of the framework. Then, in order to achieve real-time and low overhead computation offloading decisions and resource allocation strategies, we design a novel two-timescale deep reinforcement learning (\textit{2Ts-DRL}) approach, consisting of a fast-timescale and a slow-timescale learning process, respectively. The primary objective is to minimize the total offloading delay and network resource usage by jointly optimizing computation offloading, resource allocation and service caching placement. We also leverage federated learning (FL) to train the \textit{2Ts-DRL} model in a distributed manner, aiming to protect the edge devices' data privacy. Simulation results corroborate the effectiveness of both the \textit{2Ts-DRL} and FL in the I-UDEC framework and prove that our proposed algorithm can reduce task execution time up to 31.87%.
An Enhanced Geo Location Technique for Social Network Communication System
Venue: arXiv cs.CY 2020
Year: 2020

Social networks have become very popular in recent years because of the increasing large number and affordability of internet enabled gadgets such as personal computers, mobile devices and internet tablets. It has been observed that the tempo of fraud in social media these days is over alarming most especially in Nigeria. As a result of this, there is need to fortify the social network services in order to secure e-mail communication and reinforce data security. This paper advocates for an advanced and secured approach for improving communication in a social Network with the use of geo-location technique. The system was designed using an Object-Oriented software development methodology and implemented using the server-based scripting language - PHP, Cascading Style Sheets (CSS) and back-end with MySQL. The proposed system will help the government and security agencies fight recent security challenges in the country.
TSV Extrusion Morphology Classification Using Deep Convolutional Neural Networks
Venue: arXiv cs.CV 2020
Year: 2020

In this paper, we utilize deep convolutional neural networks (CNNs) to classify the morphology of through-silicon via (TSV) extrusion in three dimensional (3D) integrated circuits (ICs). TSV extrusion is a crucial reliability concern which can deform and crack interconnect layers in 3D ICs and cause device failures. Herein, the white light interferometry (WLI) technique is used to obtain the surface profile of the extruded TSVs. We have developed a program that uses raw data obtained from WLI to create a TSV extrusion morphology dataset, including TSV images with 54x54 pixels that are labeled and categorized into three morphology classes. Four CNN architectures with different network complexities are implemented and trained for TSV extrusion morphology classification application. Data augmentation and dropout approaches are utilized to realize a balance between overfitting and underfitting in the CNN models. Results obtained show that the CNN model with optimized complexity, dropout, and data augmentation can achieve a classification accuracy comparable to that of a human expert.
H.264/SVC Mode Decision Based on Mode Correlation and Desired Mode List
Venue: arXiv cs.MM 2020
Year: 2020

The design of video encoders involves the implementation of fast mode decision (FMD) algorithm to reduce computation complexity while maintaining the performance of the coding. Although H.264/scalable video coding (SVC) achieves high scalability and coding efficiency, it also has high complexity in implementing its exhaustive computation. In this paper, a novel algorithm is proposed to reduce the redundant candidate modes by making use of the correlation among layers. The desired mode list is created based on the probability to be the best mode for each block in the base layer and a candidate mode selection in the enhancement layer by the correlations of modes among the reference frame and current frame. Our algorithm is implemented in joint scalable video model (JSVM) 9.19.15 reference software and the performance is evaluated based on the average encoding time, peak signal to noise ratio (PSNR) and bit rate. The experimental results show 41.89% improvement in encoding time with minimal loss of 0.02dB in PSNR and 0.05% increase in bit rate.
On Hybrid-ARQ-Based Intelligent Reflecting Surface-Assisted Communication System
Venue: arXiv cs.IT 2020
Year: 2020

The intelligent reflecting surface (IRS) is an emerging technique to extend the wireless coverage. In this letter, the performance of hybrid automatic repeat request (hybrid-ARQ) for an IRS-assisted system is analyzed. More specifically, the outage performance of the IRS-aided system using hybrid-ARQ protocol with chase combining is studied. Asymptotic analysis also shows that the outage performance improves better than linearly by increasing number of reflectors of the IRS-aided system. The results also verify the potential of combining the ARQ scheme in the link layer of the IRS-aided system and demonstrate that very small change of path loss condition can impact the performance largely.
ORACLE: Collaboration of Data and Control Planes to Detect DDoS Attacks
Venue: arXiv cs.NI 2020
Year: 2020

The possibility of programming the control and data planes, enabled by the Software-Defined Networking (SDN) paradigm, represents a fertile ground on top of which novel operation and management mechanisms can be fully explored, being Distributed Denial of Service (DDoS) attack detection based on machine learning techniques the focus of this work. To carry out the detection, this paper proposes ORACLE: cOllaboRation of dAta and Control pLanEs to detect DDoS attacks, an architecture that promotes the coordination of control and data planes to detect network attacks. As its first contribution, this architecture delegates to the data plane the extraction and processing of traffic information collected per flow. This is done in order to ease the calculation and classification of the feature set used in the attack detection, as the needed flow information is already processed when it arrives at the control plane. Besides, as the second contribution, this architecture breaks the limitations to calculate some features that are not possible to implement in a traditional OpenFlow-based environment. In the evaluation of ORACLE, we obtained up to 96% of accuracy in the testing phase, using a K-Nearest Neighbor model.
A Hybrid Model for Learning Embeddings and Logical Rules Simultaneously from Knowledge Graphs
Venue: arXiv cs.AI 2020
Year: 2020

The problem of knowledge graph (KG) reasoning has been widely explored by traditional rule-based systems and more recently by knowledge graph embedding methods. While logical rules can capture deterministic behavior in a KG they are brittle and mining ones that infer facts beyond the known KG is challenging. Probabilistic embedding methods are effective in capturing global soft statistical tendencies and reasoning with them is computationally efficient. While embedding representations learned from rich training data are expressive, incompleteness and sparsity in real-world KGs can impact their effectiveness. We aim to leverage the complementary properties of both methods to develop a hybrid model that learns both high-quality rules and embeddings simultaneously. Our method uses a cross feedback paradigm wherein, an embedding model is used to guide the search of a rule mining system to mine rules and infer new facts. These new facts are sampled and further used to refine the embedding model. Experiments on multiple benchmark datasets show the effectiveness of our method over other competitive standalone and hybrid baselines. We also show its efficacy in a sparse KG setting and finally explore the connection with negative sampling.
Bounded Game-Theoretic Semantics for Modal Mu-Calculus and Some Variants
Venue: arXiv cs.LO 2020
Year: 2020

We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. For example, they have already been successfully used as a basis for an approach leading to a natural formula size game for the logic. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models, and we also use the GTS to identify new alternative variants of the mu-calculus with PTime model checking.