Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LogicLearner: A Tool for the Guided Practice of Propositional Logic Proofs

Amogh Inamdar, Uzay Macar, Michel Vazirani, Michael Tarnow, Zarina Mustapha, Natalia Dittren, Sam Sadeh, Nakul Verma, Ansaf Salleb-Aouissi

TL;DR

This work targets the challenge of learning propositional logic proofs by offering guided, on-demand practice with immediate AI-assisted feedback. It introduces LogicLearner, a web-based tool that models logic proofs as a graph over Boolean expressions encoded with a CFG, and provides two-level hints via time-bound A* search using a learned heuristic ensemble. The system is evaluated through a two-semester student study and a set of AI experiments, showing reduced student anxiety, higher confidence, and modest exam gains, while outperforming general LLM-based QA tools like ChatGPT for multi-step proofs. By delivering an open-source, end-to-end proof-practice environment, the paper demonstrates a practical path toward democratizing formal reasoning education in CS curricula.

Abstract

The study of propositional logic -- fundamental to the theory of computing -- is a cornerstone of the undergraduate computer science curriculum. Learning to solve logical proofs requires repeated guided practice, but undergraduate students often lack access to on-demand tutoring in a judgment-free environment. In this work, we highlight the need for guided practice tools in undergraduate mathematics education and outline the desiderata of an effective practice tool. We accordingly develop LogicLearner, a web application for guided logic proof practice. LogicLearner consists of an interface to attempt logic proofs step-by-step and an automated proof solver to generate solutions on the fly, allowing users to request guidance as needed. We pilot LogicLearner as a practice tool in two semesters of an undergraduate discrete mathematics course and receive strongly positive feedback for usability and pedagogical value in student surveys. To the best of our knowledge, LogicLearner is the only learning tool that provides an end-to-end practice environment for logic proofs with immediate, judgment-free feedback.

LogicLearner: A Tool for the Guided Practice of Propositional Logic Proofs

TL;DR

This work targets the challenge of learning propositional logic proofs by offering guided, on-demand practice with immediate AI-assisted feedback. It introduces LogicLearner, a web-based tool that models logic proofs as a graph over Boolean expressions encoded with a CFG, and provides two-level hints via time-bound A* search using a learned heuristic ensemble. The system is evaluated through a two-semester student study and a set of AI experiments, showing reduced student anxiety, higher confidence, and modest exam gains, while outperforming general LLM-based QA tools like ChatGPT for multi-step proofs. By delivering an open-source, end-to-end proof-practice environment, the paper demonstrates a practical path toward democratizing formal reasoning education in CS curricula.

Abstract

The study of propositional logic -- fundamental to the theory of computing -- is a cornerstone of the undergraduate computer science curriculum. Learning to solve logical proofs requires repeated guided practice, but undergraduate students often lack access to on-demand tutoring in a judgment-free environment. In this work, we highlight the need for guided practice tools in undergraduate mathematics education and outline the desiderata of an effective practice tool. We accordingly develop LogicLearner, a web application for guided logic proof practice. LogicLearner consists of an interface to attempt logic proofs step-by-step and an automated proof solver to generate solutions on the fly, allowing users to request guidance as needed. We pilot LogicLearner as a practice tool in two semesters of an undergraduate discrete mathematics course and receive strongly positive feedback for usability and pedagogical value in student surveys. To the best of our knowledge, LogicLearner is the only learning tool that provides an end-to-end practice environment for logic proofs with immediate, judgment-free feedback.

Paper Structure

This paper contains 25 sections, 1 theorem, 23 figures, 10 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Automated logic problem solvers
  4. The pedagogy of propositional logic
  5. Methods
  6. User Experience
  7. User Interface
  8. Database
  9. Application Back-end and Proof Solving
  10. Validating user input
  11. Modeling the logic proof
  12. Finding a search frontier
  13. Solving proofs with A* Search
  14. Extensions: question generation and neural embeddings
  15. Results
  16. ...and 10 more sections

Key Result

Lemma 1

In every problem, the target expression $e_t$ is always reachable from any expression $e_c$ that a student derives from the premise $e_s$.

Figures (23)

  • Figure 1: is a holistic environment for guided logic proof practice.
  • Figure 2: The user flow diagram of shows that students have a linear decision making process, enabling ease of use.
  • Figure 3: generates a 'frontier' of all possible next steps from the current expression, and subsequently a full proof for hints. User input is checked for syntax and membership in the frontier. The user receives feedback on incorrect inputs and can request a hint at any time.
  • Figure 4: (a) A users attempts a logic proof on and requests hints when stuck. (b) Search trees are calculated at every step of the proof attempt. The trees for the two requested hints in part (a) are as depicted here as numbered.
  • Figure 5: Confidence scores for solving logic problems under various scenarios, aggregated across two semesters of a discrete mathematics course
  • ...and 18 more figures

Theorems & Definitions (2)

  • Lemma 1
  • proof