Formally Verifying History using Theorem Proving

Abstract

History is considered as an essential part of our life, as it decides our present and future which is primarily based on historical facts. Historical facts are usually documented in books and are justified by the use of informal arguments, which has been acquired through lengthy procedures by historians and they are quite difficult to understand. Despite of the conventional techniques/ methods used by historians to acquire data there is no clear distinction between true historical events and myths. Thus, its a great challenge to ascertain the correctness of reasoning behind a historical fact. A traditional historical procedure comprises of the twelve primitive axioms to ensure the veracity of a historical event. In this thesis, we overcome this issue by presenting a formal reasoning approach to analyze historical facts. In particular, the approach is based on the formalization of twelve primitive axioms. Using higher-order logic this formalization can in turn be used to reason about the correctness of historical facts within the sound core of a theorem prover. For illustration, the developed reasoning support has been used to reason about some wellknown historical facts i.e., three hours blackout at the time of Christ’s death.