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...
Main Authors: | , , |
---|---|
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 |