Formalization of Algorithms and Logical Inference Systems in Proof Assistants

摘要

The purpose of the project is to use proof assistants, in particular Isabelle, to prove key properties about algorithms and logical inference systems. Algorithms and logic are fundamental concepts of artificial intelligence (AI) and are used to make abstract descriptions of hardware and software that one can reason about. The two disciplines date back to ancient Greece, but have become increasingly important during the last century with the invention and rise of computers.