Anthropomorphic Proof System for First-Order Logic
Abdul Rahim Nizamani · Chalmers Publication Library (Chalmers University of Technology) · 2010
This thesis presents a computer-based experiment conducted to study the human rea-soning in first-order logic. Fifty questions of FOL with accompanying graph models were presented to participants, who were asked to determine which questions were true and vice versa. The questions appeared randomly and with a fixed time limit, and the response times were recorded for all the right answers. A suggested proof system for FOL with bounded cognitive resources is analyzed using the results from this experiment. Results show that the proposed proof system models the human reasoning much better for some problems but not for all. With some shortcomings and space for improvement, the system gives a working concept for better proof formalisms with limited cognitive resources, which can generate proofs that are easier to comprehend than the purely mathematical proof strategies used today. ii Acknowledgements First of all, I thank my supervisor Claes Stranneg̊ard who trusted me for this research work and entrusted to me the work in his project of anthropomorphic artificial intelligence at the IT University of Göteborg. This project is in continuation to his previous works in the same area, and indeed the work presented herein is based on his proposed topic. Next, I thank the participants in this research work, including Fredrik Engström and Simon Ulfsbäcker. I am grateful to Lance Rips, professor of cognitive psychology, NorthWestern University USA, who helped us in the design of the experiment. I am also grateful to all the participants in the experiments with whose volunteer help we have been able to produce the results. Without them, this project could never be realised.