This project addresses machine formalization of mathematical theorems. We introduce the OCaml programming language and the HOL Light proof assistant. The original aim was to formalize the proof that tableau generation is a finite algorithm. This problem was later revised and instead the automation of the tableau method was implemented in OCaml. Tableau generation and simplification were undertaken, as well as automated tautology proving. In the end, several test cases are considered, where a known tautology or non-tautology was tested with the program, and each of them were successful.
|Uddannelser||Datalogi, (Bachelor/kandidatuddannelse) Bachelor el. kandidat|
|Udgivelsesdato||17 jun. 2010|