Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas

TL;DR

This paper introduces methods for testing equivalence and explaining non-equivalence of first-order logic formulas, combining theoretical insights and tools, validated on a large educational dataset.

Contribution

It presents novel methods for (non-)equivalence testing and explanation in first-order logic, supported by implementation and experimental validation.

Findings

Effective testing of formula equivalence demonstrated

Successful explanation of non-equivalence cases

Validated on over 100,000 formula pairs

Abstract

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.