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

• URL: http://arxiv.org/abs/2503.19280v1
• Date: Tue, 25 Mar 2025 02:23:08 GMT
• Title: LogicLearner: A Tool for the Guided Practice of Propositional Logic Proofs
• Authors: Amogh Inamdar, Uzay Macar, Michel Vazirani, Michael Tarnow, Zarina Mustapha, Natalia Dittren, Sam Sadeh, Nakul Verma, Ansaf Salleb-Aouissi,
• Abstract summary: We develop LogicLearner, a web application for guided logic proof practice.<n> LogicLearner consists of an interface to attempt logic proofs step-by-step and an automated proof solver to generate solutions on the fly.
• Score: 2.649019945607464
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Logical Modelling in CS Education: Bridging the Natural Language Gap [0.0]
  An important learning objective for computer science students is to learn how to formalize descriptions of real world scenarios. We propose a conceptual framework for educational tasks where students choose a vocabulary. We implement educational tasks for designing propositional and first-order vocabularies within the Iltis educational system.
  arXiv  Detail & Related papers  (2025-04-30T07:34:41Z)
• Logical Modalities within the European AI Act: An Analysis [0.0]
  The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities. It aims to prepare its formal representation within the logic-pluralistic Knowledge Engineering Framework and methodology. LogiKEy develops computational tools for normative reasoning based on formal methods.
  arXiv  Detail & Related papers  (2025-01-31T13:15:33Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  We propose Math-Minos, a natural language feedback-enhanced verifier. Our experiments reveal that a small set of natural language feedback can significantly boost the performance of the verifier.
  arXiv  Detail & Related papers  (2024-06-20T06:42:27Z)
• Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
  We propose a curriculum-based logical-aware instruction tuning framework, named LACT.<n>Specifically, we augment the arbitrary first-order logical queries via binary tree decomposition.<n> Experiments across widely used datasets demonstrate that LACT has substantial improvements(brings an average +5.5% MRR score) over advanced methods, achieving the new state-of-the-art.
  arXiv  Detail & Related papers  (2024-05-02T18:12:08Z)
• Language Models can be Logical Solvers [99.40649402395725]
  We introduce LoGiPT, a novel language model that directly emulates the reasoning processes of logical solvers. LoGiPT is fine-tuned on a newly constructed instruction-tuning dataset derived from revealing and refining the invisible reasoning process of deductive solvers.
  arXiv  Detail & Related papers  (2023-11-10T16:23:50Z)
• Empower Nested Boolean Logic via Self-Supervised Curriculum Learning [67.46052028752327]
  We find that any pre-trained language models even including large language models only behave like a random selector in the face of multi-nested logic. To empower language models with this fundamental capability, this paper proposes a new self-supervised learning method textitCurriculum Logical Reasoning (textscClr)
  arXiv  Detail & Related papers  (2023-10-09T06:54:02Z)
• Towards LogiGLUE: A Brief Survey and A Benchmark for Analyzing Logical Reasoning Capabilities of Language Models [56.34029644009297]
  Large language models (LLMs) have demonstrated the ability to overcome various limitations of formal Knowledge Representation (KR) systems. LLMs excel most in abductive reasoning, followed by deductive reasoning, while they are least effective at inductive reasoning. We study single-task training, multi-task training, and "chain-of-thought" knowledge distillation fine-tuning technique to assess the performance of model.
  arXiv  Detail & Related papers  (2023-10-02T01:00:50Z)
• LogiGAN: Learning Logical Reasoning via Adversarial Pre-training [58.11043285534766]
  We present LogiGAN, an unsupervised adversarial pre-training framework for improving logical reasoning abilities of language models. Inspired by the facilitation effect of reflective thinking in human learning, we simulate the learning-thinking process with an adversarial Generator-Verifier architecture. Both base and large size language models pre-trained with LogiGAN demonstrate obvious performance improvement on 12 datasets.
  arXiv  Detail & Related papers  (2022-05-18T08:46:49Z)
• Adversarial Learning to Reason in an Arbitrary Logic [5.076419064097733]
  Existing approaches to learning to prove theorems focus on particular logics and datasets. We propose Monte-Carlo simulations guided by reinforcement learning that can work in an arbitrarily specified logic.
  arXiv  Detail & Related papers  (2022-04-06T11:25:19Z)
• Logic Tensor Networks [9.004005678155023]
  We present Logic Networks (LTN), a neurosymbolic formalism and computational model that supports learning and reasoning. We show that LTN provides a uniform language for the specification and the computation of several AI tasks.
  arXiv  Detail & Related papers  (2020-12-25T22:30:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.