First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence. We propose such methods based on both theoretical insights and existing tools, implement them, and report on experiments testing their effectiveness on a large educational data set with > 100.000 pairs of first-order formulas.

翻译：一阶逻辑是众多知识表示形式化方法的基础。为支持从自然语言规约学习书写一阶公式的技术需求，需要能够检测公式（非）等价性并提供非等价解释的方法。我们基于理论洞见与现有工具提出了此类方法，完成了系统实现，并在包含超过10万对一阶公式的大规模教育数据集上通过实验验证了其有效性。