Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas
Logic in Computer Science
2026-02-24 v1
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.
Cite
@article{arxiv.2602.19673,
title = {Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas},
author = {Fabian Vehlken and Thomas Zeume and Emilio Carrasco Bustamante and Maëlle Cornély and Lukas Pradel},
journal= {arXiv preprint arXiv:2602.19673},
year = {2026}
}