A Case Study in Computer-Assisted Meta-reasoning

Asta Halkjær From, Simon Tobias Lund, Jørgen Villadsen*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationDistributed Computing and Artificial Intelligence : Special Sessions: 18th International Conference
EditorsSara Rodríguez González, José Manuel Machado, Alfonso González-Briones, Jaroslaw Wikarek, Roussanka Loukanova, George Katranas, Roberto Casado-Vara
Volume2
PublisherSpringer
Publication date2022
Pages53-63
ISBN (Print)9783030868864
DOIs
Publication statusPublished - 2022
Event18th International Symposium on Distributed Computing and Artificial Intelligence - Salamanca, Spain
Duration: 6 Oct 20218 Oct 2021
https://www.dcai-conference.net/

Conference

Conference18th International Symposium on Distributed Computing and Artificial Intelligence
Country/TerritorySpain
CitySalamanca
Period06/10/202108/10/2021
Internet address
SeriesLecture Notes in Networks and Systems
Volume332
ISSN2367-3370

Bibliographical note

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Cite this