We present an automated lemma generation method for equational, inductive theorem proving based on the term rewriting induction of Reddy and Aoto as well as the divergence critic framework of Walsh. The method effectively works by using the divergence-detection technique to locate differences in diverging sequences, and generates potential lemmas automatically by analyzing these differences. We have incorporated this method in the multi-context inductive theorem prover of Sato and Kurihara to overcome the strategic problems resulting from the unsoundness of the method. The experimental results show that our method is effective especially for some problems diverging with complex differences (i.e., parallel and nested differences).

The insoluble Prussian-blue (PB) pigment becomes possible to disperse in aqueous solution by covering their surfaces with ferrocyanide anions. The thin film fabricated with these water-dispersible PB nanoparticles shows evident electrochromic color changes between +0.8 V to -0.4 V on an ITO substrate. The mass change of the thin film during an electrochemical reaction is measured by means of electrochemical quartz crystal microbalance (EQCM). According to the EQCM analysis, the filling rate of water-dispersible PB nanoparticles in the film is 37.7% as compared with an assumed perfect crystal PB film.

We extend the theorem of Gramlich on modular termination of term rewriting systems, by relaxing the disjointness condition and introducing the composability instead. More precisely, we prove that if R1, R-1 are composable, terminating term rewriting systems such that their union is nonterminating then for some a {1, -1}, Ra OR is nonterminating and R-aRa is Fa-lifting. Here, OR is defined to be the special system {or(x, y) x, or(x, y) y}, Fa is the set of function symbols associated with Ra, and an Fa-lifting system contains a rule which has either a variable or a symbol from Fa at the leftmost position of its right-hand side. The extended theorem is stronger than the original one in that it relaxed the disjointness and constructor-sharing conditions and allowed the two systems to share defined symbols in common under the restriction of composability. The corollaries of the theorem show several sufficient conditions for decomposability of termination, which are useful for proving termination of term rewriting systems defined by combination of several composable modules.

Link prediction, the computational problem of determining whether there is a link between two objects, is important in machine learning and data mining. Feature-based link prediction, in which the feature vectors of the two objects are given, is of particular interest because it can also be used for various identification-related problems. Although the factorization machine and the higher-order factorization machine (HOFM) are widely used for feature-based link prediction, they use feature combinations not only across the two objects but also from the same object. Feature combinations from the same object are irrelevant to major link prediction problems such as predicting identity because using them increases computational cost and degrades accuracy. In this paper, we present novel models that use higher-order feature combinations only across the two objects. Since there were no algorithms for efficiently computing higher-order feature combinations only across two objects, we derive one by leveraging reported and newly obtained results of calculating the ANOVA kernel. We present an efficient coordinate descent algorithm for proposed models. We also improve the effectiveness of the existing one for the HOFM. Furthermore, we extend proposed models to a deep neural network. Experimental results demonstrated the effectiveness of our proposed models.

Refactoring is one of the promising techniques for improving program design by means of program transformation with preserving behavior, and is widely applied in practice. However, it is difficult for engineers to identify how and where to refactor programs, because proper knowledge and skills of a high order are required of them. In this paper, we propose the technique to instruct how and where to refactor a program by using a sequence of its modifications. We consider that the histories of program modifications reflect developers' intentions, and focusing on them allows us to provide suitable refactoring guides. Our technique can be automated by storing the correspondence of modification patterns to suitable refactoring operations. By implementing an automated supporting tool, we show its feasibility. The tool is implemented as a plug-in for Eclipse IDE. It selects refactoring operations by matching between a sequence of program modifications and modification patterns.

A term rewriting system is said to be rpoterminating if it's termination is proved with the recursive path ordering method. The direct sum R1M2 of term rewriting systems R1 and R2 is rpo-terminating iff both R1 and R2 are so.

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 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.