Many forms of inductive logic programming (ILP) use \emph{metarules},
second-order Horn clauses, to define the structure of learnable programs and
thus the hypothesis space. Deciding which metarules to use for a given learning
task is a major open problem and is a trade-off between efficiency and
expressivity: the hypothesis space grows given more metarules, so we wish to
use fewer metarules, but if we use too few metarules then we lose expressivity.
In this paper, we study whether fragments of metarules can be logically reduced
to minimal finite subsets. We consider two traditional forms of logical
reduction: subsumption and entailment. We also consider a new reduction
technique called \emph{derivation reduction}, which is based on SLD-resolution.
We compute reduced sets of metarules for fragments relevant to ILP and
theoretically show whether these reduced sets are reductions for more general
infinite fragments. We experimentally compare learning with reduced sets of
metarules on three domains: Michalski trains, string transformations, and game
rules. In general, derivation reduced sets of metarules outperforms subsumption
and entailment reduced sets, both in terms of predictive accuracies and
learning times.

本文研究了归纳逻辑程序（ILP）的元规则，探讨了将元规则的片段逻辑约简到最小有限子集的可行性以及利用 SLD 解析技术来进行约简的新方法，并在三个不同领域的实验中发现，基于 SLD 约简的元规则相较于 Subsumption 和 Entailment 约简具有更好的预测准确性和学习时间。

元规则的逻辑简化

Logical reduction of metarules

Optimization of Mixed-Integer Non-Linear Programming (MINLP) supports
important decisions in applications such as Chemical Process Engineering. But
current solvers have limited ability for deductive reasoning or the use of
domain-specific theories, and the management of integrality constraints does
not yet exploit automated reasoning tools such as SMT solvers. This seems to
limit both scalability and reach of such tools in practice. We therefore
present a tool, ManyOpt, for MINLP optimization that enables experimentation
with reduction techniques which transform a MINLP problem to feasibility
checking realized by an SMT solver. ManyOpt is similar to the SAT solver
ManySAT in that it runs a specified number of such reduction techniques in
parallel to get the strongest result on a given MINLP problem. The tool is
implemented in layers, which we may see as features and where reduction
techniques are feature vectors. Some of these features are inspired by known
MINLP techniques whereas others are novel and specific to SMT. Our experimental
results on standard benchmarks demonstrate the benefits of this approach. The
tool supports a variety of SMT solvers and is easily extensible with new
features, courtesy of its layered structure. For example, logical formulas for
deductive reasoning are easily added to constrain further the optimization of a
MINLP problem of interest.

本文介绍了一个名为 ManyOpt 的工具，用于 Mixed-Integer Non-Linear Programming（MINLP）优化并基于可满足性求解器（SMT solver）的可行性检查方法。该工具具有层次结构，支持多种 SMT solver，且易于添加新特性。实验表明该方法能够取得良好的效果。