Analysis of Automated Theorem Proving through Abstraction of Logical Expressions
Published in National Conference on Undergraduate Research (NCUR), 2025
Abstract
This presentation explores the intersection of Automated Theorem Proving (ATP) and Natural Language Processing (NLP). It discusses a novel framework for translating natural language sentences into logical expressions and subsequently into Conjunctive Normal Form (CNF) for Boolean satisfiability (SAT) solving. The talk highlights the use of fine-tuned Large Language Models (LLMs) to reduce hallucinations in this translation process, enabling more reliable automated reasoning for applications in software verification and debugging.
Presentation Details:
- Type: Oral Presentation
- Event: NCUR 2025
- Date: April 8, 2025
- Location: Pittsburgh, PA
Recommended citation: M. Pan. (2025). "Analysis of Automated Theorem Proving through Abstraction of Logical Expressions." National Conference on Undergraduate Research (NCUR). Oral Presentation.
Download Paper