Conference paper
A Case Study in Computer-Assisted Meta-reasoning
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2022 |
Pages: | 53-63 |
Proceedings: | 18<sup>th</sup> International Symposium on Distributed Computing and Artificial Intelligence |
Series: | Lecture Notes in Networks and Systems |
Journal subtitle: | Special Sessions: 18<sup>th</sup> International Conference |
ISBN: | 3030868869 , 3030868877 , 9783030868864 and 9783030868871 |
ISSN: | 23673370 |
Types: | Conference paper |
DOI: | 10.1007/978-3-030-86887-1_5 |
ORCIDs: | From, Asta Halkjær and Villadsen, Jørgen |