Many problems, especially those with a composite structure, can naturally be
expressed in higher order logic. From a KR perspective modeling these problems
in an intuitive way is a challenging task. In this paper we study the graph
mining problem as an example of a higher order problem. In short, this problem
asks us to find a graph that frequently occurs as a subgraph among a set of
example graphs. We start from the problem's mathematical definition to solve it
in three state-of-the-art specification systems. For IDP and ASP, which have no
native support for higher order logic, we propose the use of encoding
techniques such as the disjoint union technique and the saturation technique.
ProB benefits from the higher order support for sets. We compare the
performance of the three approaches to get an idea of the overhead of the
higher order support.
We propose higher-order language extensions for IDP-like specification
languages and discuss what kind of solver support is needed. Native higher
order shifts the burden of rewriting specifications using encoding techniques
from the user to the solver itself.

研究高阶问题表述在知识表示方面的挑战性，并以图挖掘问题为例进行解决，提出了编码技术以及高阶语言扩展来实现高阶逻辑。此外，比较了三种不同的方法的性能，讨论了求解器的支持问题。

图挖掘的知识表示分析

Knowledge Representation Analysis of Graph Mining

I propose a system for Automated Theorem Proving in higher order logic using
deep learning and eschewing hand-constructed features. Holophrasm exploits the
formalism of the Metamath language and explores partial proof trees using a
neural-network-augmented bandit algorithm and a sequence-to-sequence model for
action enumeration. The system proves 14% of its test theorems from Metamath's
set.mm module.

使用深度学习自动证明定理的系统 Holophrasm，利用 Metamath 语言的形式化逻辑和神经网络增强的贪心算法，以及序列到序列模型进行行动枚举，可以证明 Metamath's set.mm 模块中 14% 的测试定理。