In (Guller, 2014), we have generalised the well-known hyperresolution principle to the first-order Godel logic with truth constants. this paper is a continuation of our work. We propose a hyperresolution calculus suit...
详细信息
In (Guller, 2014), we have generalised the well-known hyperresolution principle to the first-order Godel logic with truth constants. this paper is a continuation of our work. We propose a hyperresolution calculus suitable for automated deduction in a useful expansion of Godel logic by intermediate truth constants and the equality, =, strict order, -1 ◇ ε 2 where ε i is an atom or a quantified atom, and 0 is the connective = or -
In this study, we analyzed the fuzzy approximate reasoning using t-norm calculation. We apply theoretical results to fuzzy optimal control. the input of the IF-thEN rules is conducted using fuzzy numbers instead of cr...
详细信息
In this study, we analyzed the fuzzy approximate reasoning using t-norm calculation. We apply theoretical results to fuzzy optimal control. the input of the IF-thEN rules is conducted using fuzzy numbers instead of crisp numbers. We concluded that there is continuity in approximate reasoning, as well as compactness in the set of membership functions for fuzzy inference. In addition, the existence of a minimum value of the function that evaluates non-linear control is presented.
In this paper, we propose a model to recommend related products to users. Our model combines the metrits of latent factor model and probabilistic topic model such as latent Dirichlet allocation(LDA), aiming to learn l...
详细信息
In this paper, we propose a model to recommend related products to users. Our model combines the metrits of latent factor model and probabilistic topic model such as latent Dirichlet allocation(LDA), aiming to learn latent user factors from observed reviews rating and latent items factors from reviews text. It provides an interpretable latent factor for users and items. Experiments on a realworld dataset show that our model outperform state-of-the-art methods on the task of recommender system.
Intrusion Detection System (IDS) is an essential component of the network security infrastructure. It detects malicious activities by monitoring network traffic. there are two main classes of IDS: the anomaly-based ID...
详细信息
Intrusion Detection System (IDS) is an essential component of the network security infrastructure. It detects malicious activities by monitoring network traffic. there are two main classes of IDS: the anomaly-based IDS and signature-based IDS. An important challenge, for signature-based IDS, is automating attack signature writing from traffic logs, which can be very hard to be established for human administrator. In this paper, we propose a solution addressing this challenge. We propose cloud-based signature learning service using Inductive logicprogramming (ILP). Learning service generates rule describing properties shared by packets labelled as malicious and that do not cover normal packets. the system uses a background knowledge composed of predicates used to describe network attack signature. the cloud architecture of our IDS enables it to have specialized nodes. Preliminary experimentations show that the proposed system is able to reproduce automatically SNORT signature.
Codatatypes are absent from many programming and specification languages. We make a case for their importance by revisiting a classical result: the completeness theorem for first-order logic established through a Gent...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Codatatypes are absent from many programming and specification languages. We make a case for their importance by revisiting a classical result: the completeness theorem for first-order logic established through a Gentzen system. the core of the proof establishes an abstract property of possibly infinite derivation trees, independently of the concrete syntax or inference rules. this separation of concerns simplifies the presentation. the abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first-order logic. the corresponding Isabelle/HOL formalization demonstrates the recently introduced support for codatatypes and the Haskell code generator.
there is a phenomenon that hardware technology has developed ahead of software technology in recent years. Companies lack of software techniques that can fully utilize the modern multi-core computing resources, mainly...
详细信息
there is a phenomenon that hardware technology has developed ahead of software technology in recent years. Companies lack of software techniques that can fully utilize the modern multi-core computing resources, mainly due to the difficulty of investigating the inherent parallelism inside a software. this problem exists in products ranging from energy-sensitive smartphones to performance-eager data centers. In this paper, we present a case study on the parallelization of the complex industry standard H.264 HDTV decoder application in multi-core systems. An optimal schedule of the tasks is obtained and implemented by a carefully-defined software parallelization framework (SPF). the parallel software framework is proposed together with a set of rules to direct parallel software programming (PSPR). A pre-processing phase based on the rules is applied to the source code to make the SPF applicable. the task-level parallel version of the H.264 decoder is implemented and tested extensively on a workstation running Linux. Significant performance improvement is observed for a set of benchmarks composed of 720p videos. the SPF and the PSPR will together serve as a reference for future parallel software implementations and direct the development of automated tools.
this paper considers real-time cluster-based wireless sensor networks where the nodes harvest energy from the environment. We target performance sensitive applications that have to collectively send their information ...
详细信息
this paper considers real-time cluster-based wireless sensor networks where the nodes harvest energy from the environment. We target performance sensitive applications that have to collectively send their information to cluster head by a predefined deadline, such as in distributed real-time monitoring and detection. the nodes are equipped with Dynamic Modulation Scaling (DMS) capable wireless radios. the problem is to determine the time slots and modulation levels that will be used by each node while communicating withthe cluster-head in order to achieve energy-neutral (perpetual) operation and maximize energy reserves. We propose a solution that adjusts underlying TDMA slots that enables high energy nodes to compensate by transmitting faster producing larger slack for dark nodes, while meeting the performance constraint. We present an optimal mixed integer linear programming based solution. We also develop fast heuristics that are shown to provide approximate solutions through comprehensive experiments with actual solar energy harvesting profiles.
Interval Temporal logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little too...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Interval Temporal logic (ITL) is a powerful formalism to reason about sequences of events that can occur simultaneously and in an overlapping fashion. Despite its importance for various application domains, little tool support for automated ITL reasoning is available, possibly also owed to ITL's undecidability. We consider bounded satisfiability which approximates finite satisfiability and is only NP-complete. We provide an encoding into SAT that is designed to use the power of modern incremental SAT solvers. We present a tool that tests an ITL specification for finite satisfiability.
Generating the prime implicates of a formula consists in finding its most general consequences. this has many fields of application in automatedreasoning, like planning and diagnosis, and although the subject has bee...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Generating the prime implicates of a formula consists in finding its most general consequences. this has many fields of application in automatedreasoning, like planning and diagnosis, and although the subject has been extensively studied (and still is) in propositional logic, very few have approached the problem in more expressive logics because of its intrinsic complexity. this paper presents one such approach for flat ground equational logic. Aiming at efficiency, it intertwines an existing method to generate all prime implicates of a formula with a rewriting technique that uses atomic equations to simplify the problem by removing constants during the search. the soundness, completeness and termination of the algorithm are proven. the algorithm has been implemented and an experimental analysis is provided.
We describe an implementation of a new theorem prover for Intuitionistic Propositional logic based on a sequent calculus with histories due to Corsi and Tassi. the main novelty of the prover lies in its use of depende...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We describe an implementation of a new theorem prover for Intuitionistic Propositional logic based on a sequent calculus with histories due to Corsi and Tassi. the main novelty of the prover lies in its use of dependency directed backtracking for global caching. We analyse the performance of the prover, and various optimisations, in comparison to current state of the art theorem provers and show that it produces competitive results on many classes of formulae.
暂无评论