We discuss human and mechanized reasoning with regards to the use of proof assistants, in particular Isabelle/HOL. We use the development of novel NAND- and NOR-based micro provers as a case study. Current, widely available automated reasoning technology is suitable for assisting humans with certain types of reasoning, like finding proofs for well-defined theorems. Other types of reasoning, like the discovery of new theorems, are notoriously difficult for mechanized reasoning. Our case study indicates that proof assistants are well suited as development tools for assuredly correct programs in languages like Haskell.
|Title of host publication||Distributed Computing and Artificial Intelligence : Special Sessions: 18th International Conference|
|Editors||Sara Rodríguez González, José Manuel Machado, Alfonso González-Briones, Jaroslaw Wikarek, Roussanka Loukanova, George Katranas, Roberto Casado-Vara|
|Publication status||Published - 2022|
|Event||18th International Symposium on Distributed Computing and Artificial Intelligence - Salamanca, Spain|
Duration: 6 Oct 2021 → 8 Oct 2021
|Conference||18th International Symposium on Distributed Computing and Artificial Intelligence|
|Period||06/10/2021 → 08/10/2021|
|Series||Lecture Notes in Networks and Systems|
Bibliographical notePublisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.