Search

Self-organizing neural network which is an unsupervised learning algorithm is to discover the inherent relationships of data. Such technique has become an important tool for data mining, machine learning and pattern recognition. Most self-organizing neural networks have a difficulty in reflecting data distributions precisely if data distributions are very complex. And meanwhile, it is also hard for these algorithms to learn new data incrementally without destroying the previous learnt data. In this paper, we propose a robust energy artificial neuron based incremental self-organizing neural network with a dynamic structure (REISOD). It can adjust the scale of network automatically to adapt the scale of the data set and learn new data incrementally with preserving the former learnt results. Moreover, several experiments show that our algorithm can reflect data distributions precisely.

Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to choose appropriate contexts (such as in which direction each equation should be oriented) when applying RI inference rules. If the choice is not appropriate, the procedure may diverge or the users have to come up with several lemmas to prove together with the main theorem. Therefore we have a good reason to consider parallel execution of several instances of the rewriting induction procedure, each in charge of a distinguished single context in search of a successful proof. In this paper, we propose a new procedure, called multi-context rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multi-completion procedure. By the experiments with a well-known problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.

In this paper, we propose a method by which frontline engineers in system development fields can readily describe the structure of the security of systems. This method, based on the assumption of the use of standard encryption technologies and existing cryptographic protocols, reveals hidden security threats and vulnerabilities of systems. It extracts only security elements that constitute the trust relationship of system components, describing the relation between the elements, and analyzing the relation. This method provides a valuable assistance tool to build secure systems, because it works as an efficient communication paradigm between stakeholders of a system to help them in understanding the security of the system and confirming that their security requirements are fulfilled.

Consensus formation models are mathematical models for obtaining potential candidates for a group when all group members pursue their individual preferences. In such models, the members often change their preferences based on the group's global preference which summarizes the overall individual preferences. Based on the theory of partially-filled reachability matrices, the Flexible Interpretive Structural Modeling (FISM) provides a method for developing structural models of complex systems and is expected to be applied to decision-making support systems. In this paper, we propose a method for simulating consensus formation in FISM and study its effectiveness through the experiments with several consensus strategies.

We describe performance enhancements that have been added to mkbTT, a modern completion tool combining multi-completion with the use of termination tools.

In equational theorem proving, convergent term rewriting systems play a crucial role. In order to compute convergent term rewriting systems, the standard completion procedure (KB) was proposed by Knuth and Bendix and has been improved in various ways. The multi-completion system MKB developed by Kurihara and Kondo accepts as input a set of reduction orders in addition to equations and efficiently simulates parallel processes each of which executes the KB procedure with one of the given orderings. Wehrman and Stump also developed a new variant of completion procedure, constraint-based completion, in which reduction orders need not be given by using automated modern termination checkers. As a result, the constraint-based procedures simulate the execution of parallel KB processes in a sequential way, but naive search algorithms sometimes cause serious inefficiency when the number of the potential reduction orders is large. In this paper, we present a new procedure, called a constraint-based multi-completion procedure MKBcs, by augmenting the constraint-based completion with the framework of the multi-completion for suppressing the combinatorial explosion by sharing inferences among the processes. The existing constraint-based system SLOTHROP, which basically employs the best-first search, is more efficient when its built-in heuristics for process selection are appropriate, but when they are not, our system is more efficient. Therefore, both systems have their role to play.

In equational theorem proving, convergent term rewriting systems play a crucial role. In order to compute convergent term rewriting systems, the standard completion procedure (KB) was proposed by Knuth and Bendix and has been improved in various ways. The multi-completion system MKB developed by Kurihara and Kondo accepts as input a set of reduction orders in addition to equations and efficiently simulates parallel processes each of which executes the KB procedure with one of the given orderings. Wehrman and Stump also developed a new variant of completion procedure, constraint-based completion, in which reduction orders need not be given by using automated modern termination checkers. As a result, the constraint-based procedures simulate the execution of parallel KB processes in a sequential way, but naive search algorithms sometimes cause serious inefficiency when the number of the potential reduction orders is large. In this paper, we present a new procedure, called a constraint-based multi-completion procedure MKBcs, by augmenting the constraint-based completion with the framework of the multi-completion for suppressing the combinatorial explosion by sharing inferences among the processes. The existing constraint-based system SLOTHROP, which basically employs the best-first search, is more efficient when its built-in heuristics for process selection are appropriate, but when they are not, our system is more efficient. Therefore, both systems have their role to play.