Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Fabian Vehlken, Thomas Zeume, Emilio Carrasco Bustamante, Maëlle Cornély, Lukas Pradel

TL;DR

This work proposes methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence based on both theoretical insights and existing tools, implements them, and reports on experiments testing their effectiveness on a large educational data set with>100.000 pairs of first-order formulas.

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.

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

TL;DR

This work proposes methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence based on both theoretical insights and existing tools, implements them, and reports on experiments testing their effectiveness on a large educational data set with>100.000 pairs of first-order formulas.

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.
Paper Structure (30 sections, 2 theorems, 3 equations, 5 figures, 21 tables)

This paper contains 30 sections, 2 theorems, 3 equations, 5 figures, 21 tables.

Table of Contents

  1. Introduction
  2. Setting, Equivalence, Counter Examples
  3. Explanations for Non-Equivalence
  4. Preprocessing
  5. Profiling the Use of Quantifiers.
  6. Profiling the Use of Guards.
  7. Profiling Necessary Symbols.
  8. Strategies for Explaining Non-equivalence
  9. Strategies for Symbols.
  10. Strategies for Quantifiers.
  11. Strategies for Guarding.
  12. Strategies for Boolean Operators.
  13. Evaluation
  14. RQ1: Determining Correctness of Student Attempts
  15. Setting.
  16. ...and 15 more sections

Key Result

Theorem 1

Let $\sigma, \sigma'$ be vocabularies with $\sigma \subseteq \sigma'$, let $\psi(\bar{x})$ be a first-order formula over $\sigma'$, and let $\mathcal{M}$ be a non-empty set of $\sigma'$-structures. Then the following are equivalent:

Figures (5)

  • Figure 1: A first-order logic modelling exercise in which students have to choose a first-order vocabulary, write first-order formulas for natural language specifications in this vocabulary, and infer knowledge with an inference mechanism such as resolution.
  • Figure 2: Time in milliseconds Vampire needed to determine whether pairs of formulas are equivalent or non-equivalent (blue) and time needed for equivalent pairs only (red). The blue and red lines show the percentiles for decisions made. Only distinct pairs of formulas are considered here.
  • Figure 3: Number of models witnessing non-equivalence of formulas found for each universe size by Vampire (red) and number of models found for each size by the random model generator (blue).
  • Figure 4: Time needed by Vampire's finite model builder (blue) and by the random model generator (red). The blue and red lines show the percentiles of counter examples found with respect to all distinct non-equivalent pairs of formulas.
  • Figure 5: Time in seconds needed to run all strategies (sequentially) for each distinct pair of non-equivalent formulas without a cache (blue) and with a cache (red). The blue and red lines show the percentiles for decisions made. Note that the # decisions axis is in logarithmic scale. Individual Vampire calls had a timeout of 30s, but the strategies themselves did not have an explicit timeout.

Theorems & Definitions (4)

  • Example 1
  • Theorem 1
  • Lemma 1
  • proof : Proof (of Lemma \ref{['lemma:equality-to-equivalence']})