Construction and evaluation of a gold standard syntax for formal logic formulas and systems

UNCG Author/Contributor (non-UNCG co-authors, if there are any, appear on document)
Larry Joshua Crotts (Creator)
Institution
The University of North Carolina at Greensboro (UNCG )
Web Site: http://library.uncg.edu/
Advisor
Stephen Tate

Abstract: Classical logic plays a significant role in computer science where formal proofs eventually make their way into a student’s curriculum via discrete mathematics, philosophy logic, or some other medium. We traditionally see propositional logic in Boolean algebra, conditional statements, program and data structure definitions and invariants, and much more. In fact, everyday language is easily expressible in first-order logic. Accordingly, a solid understanding of classical logic is paramount. Natural deduction, as the name suggests, is a method of reasoning about an argument using natural intuition, and as a result, it appears quite frequently as a topic of study in introductory logic courses. Due to its relevance, natural deduction intelligent tutors and solvers are widespread on the internet and in the classroom to improve the pedagogical appeal of logic. In this thesis, we present and solve two questions. The first is a proposed research question wherein we evaluate the efficacy of publicly-available natural deduction tutors/solvers with the prospect of determining what inherently defines understandability and difficulty in natural deduction proofs. In the second question, we investigate the problem of unnecessary intermingling of logic syntaxes. With this, we propose a gold standard language for zeroth and first-order logic with the goal and hope of tutor/proof systems adapting to said language to ease the currently laborious task of system evaluation and comparison.

Additional Information

Publication
Thesis
Language: English
Date: 2022
Keywords
Automatic Theorem Prover, First-Order Logic, Formal Logic, Logic Pedagogy, Natural Deduction, Propositional Logic
Subjects
Logic $x Study and teaching
Proof theory $x Data processing
Intelligent tutoring systems

Email this document to