A Case Study in Computer-Assisted Meta-reasoning

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

doi:10.1007/978-3-030-86887-1_5

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 proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Distributed Computing and Artificial Intelligence : Special Sessions: 18^th International Conference
Editors	Sara Rodríguez González, José Manuel Machado, Alfonso González-Briones, Jaroslaw Wikarek, Roussanka Loukanova, George Katranas, Roberto Casado-Vara
Volume	2
Publisher	Springer
Publication date	2022
Pages	53-63
ISBN (Print)	9783030868864
DOIs	https://doi.org/10.1007/978-3-030-86887-1_5
Publication status	Published - 2022
Event	18^th International Symposium on Distributed Computing and Artificial Intelligence - Salamanca, Spain Duration: 6 Oct 2021 → 8 Oct 2021 https://www.dcai-conference.net/

Conference

Conference	18^th International Symposium on Distributed Computing and Artificial Intelligence
Country/Territory	Spain
City	Salamanca
Period	06/10/2021 → 08/10/2021
Internet address	https://www.dcai-conference.net/

Series	Lecture Notes in Networks and Systems
Volume	332
ISSN	2367-3370

Bibliographical note

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

Access to Document

10.1007/978-3-030-86887-1_5

OpenUrl availability

Full text

Cite this

From, A. H., Lund, S. T., & Villadsen, J. (2022). A Case Study in Computer-Assisted Meta-reasoning. In S. R. González, J. M. Machado, A. González-Briones, J. Wikarek, R. Loukanova, G. Katranas, & R. Casado-Vara (Eds.), Distributed Computing and Artificial Intelligence: Special Sessions: 18^th International Conference (Vol. 2, pp. 53-63). Springer. https://doi.org/10.1007/978-3-030-86887-1_5

From, Asta Halkjær ; Lund, Simon Tobias ; Villadsen, Jørgen. / A Case Study in Computer-Assisted Meta-reasoning. Distributed Computing and Artificial Intelligence: Special Sessions: 18^th International Conference. editor / Sara Rodríguez González ; José Manuel Machado ; Alfonso González-Briones ; Jaroslaw Wikarek ; Roussanka Loukanova ; George Katranas ; Roberto Casado-Vara. Vol. 2 Springer, 2022. pp. 53-63 (Lecture Notes in Networks and Systems, Vol. 332).

@inproceedings{3b1df020dba04bf09aedace4ceed8d05,

title = "A Case Study in Computer-Assisted Meta-reasoning",

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.",

author = "From, {Asta Halkj{\ae}r} and Lund, {Simon Tobias} and J{\o}rgen Villadsen",

note = "Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 18<sup>th</sup> International Symposium on Distributed Computing and Artificial Intelligence, DCAI 2021 ; Conference date: 06-10-2021 Through 08-10-2021",

year = "2022",

doi = "10.1007/978-3-030-86887-1_5",

language = "English",

isbn = "9783030868864",

volume = "2",

series = "Lecture Notes in Networks and Systems",

publisher = "Springer",

pages = "53--63",

editor = "Gonz{\'a}lez, {Sara Rodr{\'i}guez} and Machado, {Jos{\'e} Manuel} and Alfonso Gonz{\'a}lez-Briones and Jaroslaw Wikarek and Roussanka Loukanova and George Katranas and Roberto Casado-Vara",

booktitle = "Distributed Computing and Artificial Intelligence",

url = "https://www.dcai-conference.net/",

}

From, AH, Lund, ST & Villadsen, J 2022, A Case Study in Computer-Assisted Meta-reasoning. in SR González, JM Machado, A González-Briones, J Wikarek, R Loukanova, G Katranas & R Casado-Vara (eds), Distributed Computing and Artificial Intelligence: Special Sessions: 18^th International Conference. vol. 2, Springer, Lecture Notes in Networks and Systems, vol. 332, pp. 53-63, 18^th International Symposium on Distributed Computing and Artificial Intelligence, Salamanca, Spain, 06/10/2021. https://doi.org/10.1007/978-3-030-86887-1_5

A Case Study in Computer-Assisted Meta-reasoning. / From, Asta Halkjær; Lund, Simon Tobias ; Villadsen, Jørgen.
Distributed Computing and Artificial Intelligence: Special Sessions: 18^th International Conference. ed. / Sara Rodríguez González; José Manuel Machado; Alfonso González-Briones; Jaroslaw Wikarek; Roussanka Loukanova; George Katranas; Roberto Casado-Vara. Vol. 2 Springer, 2022. p. 53-63 (Lecture Notes in Networks and Systems, Vol. 332).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - A Case Study in Computer-Assisted Meta-reasoning

AU - From, Asta Halkjær

AU - Lund, Simon Tobias

AU - Villadsen, Jørgen

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-86887-1_5

DO - 10.1007/978-3-030-86887-1_5

M3 - Article in proceedings

AN - SCOPUS:85115424303

SN - 9783030868864

VL - 2

T3 - Lecture Notes in Networks and Systems

SP - 53

EP - 63

BT - Distributed Computing and Artificial Intelligence

A2 - González, Sara Rodríguez

A2 - Machado, José Manuel

A2 - González-Briones, Alfonso

A2 - Wikarek, Jaroslaw

A2 - Loukanova, Roussanka

A2 - Katranas, George

A2 - Casado-Vara, Roberto

PB - Springer

T2 - 18<sup>th</sup> International Symposium on Distributed Computing and Artificial Intelligence

Y2 - 6 October 2021 through 8 October 2021

ER -

From AH, Lund ST , Villadsen J. A Case Study in Computer-Assisted Meta-reasoning. In González SR, Machado JM, González-Briones A, Wikarek J, Loukanova R, Katranas G, Casado-Vara R, editors, Distributed Computing and Artificial Intelligence: Special Sessions: 18^th International Conference. Vol. 2. Springer. 2022. p. 53-63. (Lecture Notes in Networks and Systems, Vol. 332). doi: 10.1007/978-3-030-86887-1_5

A Case Study in Computer-Assisted Meta-reasoning

Abstract

Conference

Bibliographical note

Access to Document

OpenUrl availability

Fingerprint

Cite this