On Quantified Modal Theorem Proving for Modeling Ethics

In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used fo...

Full description

Bibliographic Details
Main Authors: Naveen Sundar Govindarajulu, Selmer Bringsjord, Matthew Peveler
Format: Article
Language:English
Published: Open Publishing Association 2019-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1912.12959v1
_version_ 1819080130642837504
author Naveen Sundar Govindarajulu
Selmer Bringsjord
Matthew Peveler
author_facet Naveen Sundar Govindarajulu
Selmer Bringsjord
Matthew Peveler
author_sort Naveen Sundar Govindarajulu
collection DOAJ
description In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Meeting these requirements necessitates investigation of new approaches for proof automation. Particularly, a quantified modal logic, the deontic cognitive event calculus (DCEC), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DCEC, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation for DCEC.
first_indexed 2024-12-21T19:40:00Z
format Article
id doaj.art-97603d6d044f450ca37e1095da42fe6c
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-12-21T19:40:00Z
publishDate 2019-12-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-97603d6d044f450ca37e1095da42fe6c2022-12-21T18:52:29ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-12-01311Proc. ARCADE 2019434910.4204/EPTCS.311.7:9On Quantified Modal Theorem Proving for Modeling EthicsNaveen Sundar Govindarajulu0Selmer Bringsjord1Matthew Peveler2 Rensselaer AI and Reasoning Lab Rensselaer Polytechnic Institute Rensselaer Polytechnic Institute In the last decade, formal logics have been used to model a wide range of ethical theories and principles with the goal of using these models within autonomous systems. Logics for modeling ethical theories, and their automated reasoners, have requirements that are different from modal logics used for other purposes, e.g. for temporal reasoning. Meeting these requirements necessitates investigation of new approaches for proof automation. Particularly, a quantified modal logic, the deontic cognitive event calculus (DCEC), has been used to model various versions of the doctrine of double effect, akrasia, and virtue ethics. Using a fragment of DCEC, we outline these distinct characteristics and present a sketches of an algorithm that can help with some aspects proof automation for DCEC.http://arxiv.org/pdf/1912.12959v1
spellingShingle Naveen Sundar Govindarajulu
Selmer Bringsjord
Matthew Peveler
On Quantified Modal Theorem Proving for Modeling Ethics
Electronic Proceedings in Theoretical Computer Science
title On Quantified Modal Theorem Proving for Modeling Ethics
title_full On Quantified Modal Theorem Proving for Modeling Ethics
title_fullStr On Quantified Modal Theorem Proving for Modeling Ethics
title_full_unstemmed On Quantified Modal Theorem Proving for Modeling Ethics
title_short On Quantified Modal Theorem Proving for Modeling Ethics
title_sort on quantified modal theorem proving for modeling ethics
url http://arxiv.org/pdf/1912.12959v1
work_keys_str_mv AT naveensundargovindarajulu onquantifiedmodaltheoremprovingformodelingethics
AT selmerbringsjord onquantifiedmodaltheoremprovingformodelingethics
AT matthewpeveler onquantifiedmodaltheoremprovingformodelingethics