Towards Automated Natural Deduction in Prolog

Lijnzaad, Flip (2021) Towards Automated Natural Deduction in Prolog. Bachelor's Thesis, Artificial Intelligence.

Preview	Text bAI_2021_LijnzaadFJA.pdf Download (465kB) | Preview
	Text Toestemming.pdf Restricted to Registered users only Download (126kB)

Abstract

We present a theorem prover for propositional logic that uses Fitch-style natural deduction to find formal proofs that are similar to how a human would make them. We chose the logic programming language Prolog to implement this system because the logical representation is a natural choice for a theorem prover, and because the language has a powerful reasoning engine. Prolog employs an unbounded depth-first search strategy in its proof search, and the search space of natural deduction proofs is infinite; to combat this issue, the prover uses iterative deepening to arrive at a shortest proof. Several heuristics are put into place to cut unneeded branches of the search tree and thus improve the performance of the system. Lastly, a parsing system that uses Prolog and Python turns the proof into LaTeX code to display the full proof in Fitch format, and provides other functionalities for input and output. The theorem prover was tested with 9 exercises in natural deduction from Introduction to Logic examinations, ranging from 5 to 9 proof steps needed to solve. The prover was able to solve 6 out of the 9 exercises within a time limit of 10 minutes per proof. The prover was not able to prove 3 out of these 9 exercises because of reasons other than computational limitations; this suggests an incompleteness in the search strategy of the system.

Item Type:	Thesis (Bachelor's Thesis)
Supervisor name:	Gattinger, B.R.M.
Degree programme:	Artificial Intelligence
Thesis type:	Bachelor's Thesis
Language:	English
Date Deposited:	30 Jul 2021 09:14
Last Modified:	30 Jul 2021 09:14
URI:	https://fse.studenttheses.ub.rug.nl/id/eprint/25522

Actions (login required)

View Item