A Theorem Proving Approach to Formal Verification of a Cognitive Agent

Alexander Birch Jensen

doi:10.1007/978-3-030-86261-9_1

A Theorem Proving Approach to Formal Verification of a Cognitive Agent

Alexander Birch Jensen^*

^*Corresponding author for this work

Department of Applied Mathematics and Computer Science

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

Abstract

Theorem proving approaches have successfully been applied to verify various traditional software and hardware systems. However, it has not been explored how theorem proving can be applied to verify agent systems. We formalize a framework for verification of cognitive agent programs in a proof assistant. This enables access to powerful automation and provides assurance that our results are correct.

Original language	English
Title of host publication	Distributed Computing and Artificial Intelligence
Editors	Kenji Matsui, Sigeru Omatu, Tan Yigitcanlar, Sara Rodríguez González
Publisher	Springer
Publication date	2022
Pages	1-11
ISBN (Print)	9783030862602
DOIs	https://doi.org/10.1007/978-3-030-86261-9_1
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	327 LNNS
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-86261-9_1

OpenUrl availability

Full text

Cite this

@inproceedings{5c32d1f5d4054d7d8002312bc1bcfdf0,

title = "A Theorem Proving Approach to Formal Verification of a Cognitive Agent",

abstract = "Theorem proving approaches have successfully been applied to verify various traditional software and hardware systems. However, it has not been explored how theorem proving can be applied to verify agent systems. We formalize a framework for verification of cognitive agent programs in a proof assistant. This enables access to powerful automation and provides assurance that our results are correct.",

author = "Jensen, {Alexander Birch}",

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-86261-9_1",

language = "English",

isbn = "9783030862602",

series = "Lecture Notes in Networks and Systems",

publisher = "Springer",

pages = "1--11",

editor = "Kenji Matsui and Sigeru Omatu and Tan Yigitcanlar and Gonz{\'a}lez, {Sara Rodr{\'i}guez}",

booktitle = "Distributed Computing and Artificial Intelligence",

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

}

Jensen, AB 2022, A Theorem Proving Approach to Formal Verification of a Cognitive Agent. in K Matsui, S Omatu, T Yigitcanlar & SR González (eds), Distributed Computing and Artificial Intelligence. Springer, Lecture Notes in Networks and Systems, vol. 327 LNNS, pp. 1-11, 18^th International Symposium on Distributed Computing and Artificial Intelligence, Salamanca, Spain, 06/10/2021. https://doi.org/10.1007/978-3-030-86261-9_1

A Theorem Proving Approach to Formal Verification of a Cognitive Agent. / Jensen, Alexander Birch.

Distributed Computing and Artificial Intelligence. ed. / Kenji Matsui; Sigeru Omatu; Tan Yigitcanlar; Sara Rodríguez González. Springer, 2022. p. 1-11 (Lecture Notes in Networks and Systems, Vol. 327 LNNS).

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

TY - GEN

T1 - A Theorem Proving Approach to Formal Verification of a Cognitive Agent

AU - Jensen, Alexander Birch

PY - 2022

Y1 - 2022

N2 - Theorem proving approaches have successfully been applied to verify various traditional software and hardware systems. However, it has not been explored how theorem proving can be applied to verify agent systems. We formalize a framework for verification of cognitive agent programs in a proof assistant. This enables access to powerful automation and provides assurance that our results are correct.

AB - Theorem proving approaches have successfully been applied to verify various traditional software and hardware systems. However, it has not been explored how theorem proving can be applied to verify agent systems. We formalize a framework for verification of cognitive agent programs in a proof assistant. This enables access to powerful automation and provides assurance that our results are correct.

U2 - 10.1007/978-3-030-86261-9_1

DO - 10.1007/978-3-030-86261-9_1

M3 - Article in proceedings

AN - SCOPUS:85115221627

SN - 9783030862602

T3 - Lecture Notes in Networks and Systems

SP - 1

EP - 11

BT - Distributed Computing and Artificial Intelligence

A2 - Matsui, Kenji

A2 - Omatu, Sigeru

A2 - Yigitcanlar, Tan

A2 - González, Sara Rodríguez

PB - Springer

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

Y2 - 6 October 2021 through 8 October 2021

ER -

A Theorem Proving Approach to Formal Verification of a Cognitive Agent

Abstract

Conference

Bibliographical note

Access to Document

OpenUrl availability

Fingerprint

Cite this