The paper focuses on the automatic generating of the witnesses for the word equation satisfiability problem by means of specializing an interpreter which tests whether a composition of variable substitutions of a given word equation system produces its solution. We specialize such an interpreter w.r.t. the equation system, while the substitutions are unknown. We show that several variants of such interpreters, when specialized using the basic unfold/fold specialization methods, are able to construct the whole solution sets for some classes of the word equations whose left- and right-hand sides share variables. We prove that the specialization process wrt the constructed interpreters gives a simple syntactic criterion of the satisfiability of the equations considered, and show that the suggested approach can solve some equations not solvable by Z3str3 and CVC4, the widely-used SMT-solvers.
Verification of Programs via Intermediate Interpretation
我们探讨了一种方法来验证程序通过程序转换适用于解释器的程序设计语言。一种被称为Turchin超级编译的专门化技术被用来专门化程序模型的一些解释器。我们发现，几个安全属性的功能程序建模一类的缓存一致性协议可以证明由超级编译器和比较结果与我们以前的工作直接验证通过超级编译不使用中间解释。我们的方法部分受到了E. De Angelis等人（2014-2015）在约束逻辑程序专门化的背景下研究了通过程序转换和中间解释进行的验证。
Implementing WordNet Measures of Lexical Semantic Similarity in a Fuzzy Logic Programming System
本文介绍了将WordNet集成到模糊逻辑程序设计系统中的技术。由于WordNet涉及的话，但不给他们之间的关系的分级信息，我们已经实施了标准的相似性措施和新的指令，允许接近方程连接两个单词生成的近似度。近似方程是关键的语法结构，除了弱统一算法之外，它还使这种程序设计语言中灵活的查询-应答过程成为可能。这一增加拓宽了模糊逻辑编程的范围，允许某些形式的词汇推理，并加强了自然语言处理的应用。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
