×

zbMATH — the first resource for mathematics

Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. (English) Zbl 07274579
Summary: A framework and methodology – termed LogiKEy – for the design and engineering of ethical reasoners, normative theories and deontic logics is presented. The overall motivation is the development of suitable means for the control and governance of intelligent autonomous systems. LogiKEy’s unifying formal framework is based on semantical embeddings of deontic logics, logic combinations and ethico-legal domain theories in expressive classic higher-order logic (HOL). This meta-logical approach enables the provision of powerful tool support in LogiKEy: off-the-shelf theorem provers and model finders for HOL are assisting the LogiKEy designer of ethical intelligent agents to flexibly experiment with underlying logics and their combinations, with ethico-legal domain theories, and with concrete examples – all at the same time. Continuous improvements of these off-the-shelf provers, without further ado, leverage the reasoning performance in LogiKEy. Case studies, in which the LogiKEy framework and methodology has been applied and tested, give evidence that HOL’s undecidability often does not hinder efficient experimentation.
MSC:
68T Artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Malle, B. F., Integrating robot ethics and machine morality: the study and design of moral competence in robots, Ethics Inf. Technol., 18, 4, 243-256 (2016)
[2] Malle, B. F.; Scheutz, M.; Austerweil, J. L., Networks of social and moral norms in human and robot agents, (Ferreira, M. I. Aldinhas; Silva Sequeira, J.; Tokhi, M. O.; Kadar, E. E.; Virk, G. S., A World with Robots: International Conference on Robot Ethics. A World with Robots: International Conference on Robot Ethics, ICRE 2015 (2017), Springer International Publishing: Springer International Publishing Cham), 3-17
[3] (Gabbay, D.; Horty, J.; Parent, X.; van der Meyden, R.; van der Torre, L., Handbook of Deontic Logic and Normative Systems, vol. 1 (2013), College Publications: College Publications London, UK) · Zbl 1309.03001
[4] (Chopra, A.; van der Torre, L.; Verhagen, H., Handbook of Normative Multi-Agent Systems (2018), College Publications: College Publications London, UK) · Zbl 07088495
[5] Parent, X.; van der Torre, L., Introduction to Deontic Logic and Normative Systems (2018), College Publications: College Publications London, UK · Zbl 1431.03034
[6] Carnielli, W.; Coniglio, M.; Gabbay, D. M.; Paula, G.; Sernadas, C., Analysis and Synthesis of Logics, Applied Logics Series, vol. 35 (2008), Springer
[7] Gabbay, D., Many-Dimensional Modal Logics: Theory and Applications, Studies in Logic and the Foundations of Mathematics (2003), North Holland Publishing Company
[8] Benzmüller, C.; Farjami, A.; Parent, X., Åqvist’s dyadic deontic logic E in HOL, Special Issue on Reasoning for Legal AI. Special Issue on Reasoning for Legal AI, IfCoLog J. Log. Appl., 6, 5, 733-755 (2019)
[9] Benzmüller, C.; Farjami, A.; Parent, X., A dyadic deontic logic in HOL, (Broersen, J.; Condoravdi, C.; Nair, S.; Pigozzi, G., Deontic Logic and Normative Systems - 14th International Conference. Deontic Logic and Normative Systems - 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018 (2018), College Publications: College Publications Utrecht, The Netherlands), 33-50 · Zbl 1418.03069
[10] Benzmüller, C.; Farjami, A.; Meder, P.; Parent, X., I/O logic in HOL, Special Issue on Reasoning for Legal AI. Special Issue on Reasoning for Legal AI, IfCoLog J. Log. Appl., 6, 5, 715-732 (2019)
[11] Meder, P., Deontic Agency and Moral Luck (2018), Faculty of Science, Technology and Communication, University of Luxembourg, Master’s thesis
[12] Fuenmayor, D.; Benzmüller, C., Harnessing higher-order (meta-)logic to represent and reason with complex ethical theories, (Nayak, A.; Sharma, A., PRICAI 2019: Trends in Artificial Intelligence. PRICAI 2019: Trends in Artificial Intelligence, Lecture Notes in Artificial Intelligence, vol. 11670 (2019), Springer: Springer Cham), 418-432
[13] Fuenmayor, D.; Benzmüller, C., Mechanised assessment of complex natural-language arguments using expressive logic combinations, (Herzig AndreiPopescu, A., Frontiers of Combining Systems, 12th International Symposium. Frontiers of Combining Systems, 12th International Symposium, FroCoS 2019, London, September 4-6. Frontiers of Combining Systems, 12th International Symposium. Frontiers of Combining Systems, 12th International Symposium, FroCoS 2019, London, September 4-6, Lecture Notes in Artificial Intelligence, vol. 11715 (2019), Springer Nature Switzerland AG), 112-128 · Zbl 1435.68315
[14] Benzmüller, C.; Andrews, P., Church’s type theory, (Zalta, E. N., The Stanford Encyclopedia of Philosophy (2019), Metaphysics Research Lab, Stanford University), 1-62, (in pdf version)
[15] (Pratihar, D. K.; Jain, L. C., Intelligent Autonomous Systems: Foundations and Applications. Intelligent Autonomous Systems: Foundations and Applications, Studies in Computational Intelligence, vol. 275 (2010), Springer) · Zbl 1191.68716
[16] de Moura, L. M.; Kong, S.; Avigad, J.; van Doorn, F.; von Raumer, J., The Lean theorem prover (system description), (Felty, A. P.; Middeldorp, A., Automated Deduction - CADE-25-25th International Conference on Automated Deduction. Automated Deduction - CADE-25-25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Automated Deduction - CADE-25-25th International Conference on Automated Deduction. Automated Deduction - CADE-25-25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9195 (2015), Springer), 378-388 · Zbl 06515520
[17] Bertot, Y.; Casteran, P., Interactive Theorem Proving and Program Development (2004), Springer · Zbl 1069.68095
[18] Bove, A.; Dybjer, P.; Norell, U., A brief overview of Agda – a functional language with dependent types, (Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., Theorem Proving in Higher Order Logics, 22nd International Conference. Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009, Proceedings, vol. 5674 (2009), Springer: Springer Munich, Germany), 73-78 · Zbl 1252.68062
[19] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer · Zbl 0994.68131
[20] Steen, A.; Benzmüller, C., The higher-order prover Leo-III, (Galmiche, D.; Schulz, S.; Sebastiani, R., Automated Reasoning. Automated Reasoning, IJCAR 2018. Automated Reasoning. Automated Reasoning, IJCAR 2018, Lecture Notes in Computer Science, vol. 10900 (2018), Springer: Springer Cham), 108-116 · Zbl 06958095
[21] Carmo, J.; Jones, A. J.I., Deontic logic and contrary-to-duties, (Gabbay, D. M.; Guenthner, F., Handbook of Philosophical Logic, vol. 8 (2002), Springer Netherlands: Springer Netherlands Dordrecht), 265-343
[22] Liao, B.; Slavkovik, M.; van der Torre, L. W.N., Building Jiminy Cricket: an architecture for moral agreements among stakeholders, (Conitzer, V.; Hadfield, G. K.; Vallor, S., Proceedings of the 2019 AAAI/ACM Conference on AI, Ethics, and Society. Proceedings of the 2019 AAAI/ACM Conference on AI, Ethics, and Society, AIES 2019, Honolulu, HI, USA, January 27-28, 2019 (2019), ACM), 147-153
[23] Dung, P. M., On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games, Artif. Intell., 77, 2, 321-357 (1995) · Zbl 1013.68556
[24] Benzmüller, C., Universal (meta-)logical reasoning: recent successes, Sci. Comput. Program., 172, 48-62 (2019)
[25] Benzmüller, C.; Sultana, N.; Paulson, L. C.; Theiß, F., The higher-order prover LEO-II, J. Autom. Reason., 55, 4, 389-404 (2015) · Zbl 1356.68176
[26] Kontopoulos, E.; Bassiliades, N.; Governatori, G.; Antoniou, G., A modal defeasible reasoner of deontic logic for the semantic web, Int. J. Semantic Web Inf. Syst., 7, 1, 18-43 (2011)
[27] Furbach, U.; Schon, C., Deontic logic for human reasoning, (Eiter, T.; Strass, H.; Truszczynski, M.; Woltran, S., Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation. Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation, Lecture Notes in Computer Science, vol. 9060 (2015), Springer), 63-80 · Zbl 1432.03031
[28] Bringsjord, S.; Naveen Sundar, G.; Malle, B. F.; Scheutz, M., Contextual deontic cognitive event calculi for ethically correct robots, (International Symposium on Artificial Intelligence and Mathematics. International Symposium on Artificial Intelligence and Mathematics, ISAIM 2018, Fort Lauderdale, Florida, USA, January 3-5, 2018 (2018))
[29] Pereira, L. M.; Saptawijaya, A., Programming Machine Ethics, Studies in Applied Philosophy, Epistemology and Rational Ethics, vol. 26 (2016), Springer
[30] C. Benzmüller, A. Farjami, D. Fuenmayor, P. Meder, X. Parent, A. Steen, L. van der Torre, V. Zahoransky, Logikey workbench: deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset), Data in Brief (submitted for publication), 2020.
[31] Gewirth, A., Reason and Morality (1981), University of Chicago Press
[32] Gleißner, T.; Steen, A.; Benzmüller, C., Theorem provers for every normal modal logic, (Eiter, T.; Sands, D., LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, Maun, Botswana. LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, Maun, Botswana, EPiC Series in Computing, vol. 46 (2017)), 14-30 · Zbl 1403.68225
[33] Zahoransky, V., Modelling the US constitution in HOL (2019), Freie Universität Berlin, BSc thesis
[34] Fuenmayor, D.; Benzmüller, C., Formalisation and evaluation of Alan Gewirth’s proof for the principle of generic consistency in Isabelle/HOL, Arch. Formal Proofs, 1-13 (2018)
[35] Fuenmayor, D.; Benzmüller, C., Computer-supported analysis of arguments in climate engineering, (Dastani, M.; Dong, H.; van der Torre, L., CLAR 2020-3rd International Conference on Logic and Argumentation, Logic in Asia: Studia Logica Library (2020), Springer Nature Switzerland AG)
[36] Fuenmayor, D.; Benzmüller, C., A case study on computational hermeneutics: E.J. Lowe’s modal ontological argument, Special Issue on Formal Approaches to the Ontological Argument. Special Issue on Formal Approaches to the Ontological Argument, IfCoLog J. Log. Appl., 5, 7, 1567-1603 (2018)
[37] Kirchner, D.; Benzmüller, C.; Zalta, E. N., Computer science and metaphysics: a cross-fertilization, Open Philos., 2, 230-251 (2019)
[38] Kirchner, D.; Benzmüller, C.; Zalta, E. N., Mechanizing principia logico-metaphysica in functional type theory, Rev. Symb. Log. (2019), in press · Zbl 07181947
[39] Benzmüller, C.; Paulson, L. C., Quantified multimodal logics in simple type theory, Special Issue on Multimodal Logics. Special Issue on Multimodal Logics, Log. Univers., 7, 1, 7-20 (2013) · Zbl 1334.03014
[40] Gibbons, J.; Wu, N., Folding domain-specific languages: deep and shallow embeddings (functional pearl), (Jeuring, J.; Chakravarty, M. M.T., Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1-3, 2014 (2014), ACM), 339-347 · Zbl 1345.68052
[41] Svenningsson, J.; Axelsson, E., Combining deep and shallow embedding for EDSL, (Loidl, H.-W.; Peña, R., Trends in Functional Programming (2013), Springer: Springer Berlin, Heidelberg), 21-36
[42] Blanchette, J. C.; Böhme, S.; Paulson, L. C., Extending Sledgehammer with SMT solvers, J. Autom. Reason., 51, 1, 109-128 (2013) · Zbl 1314.68272
[43] Blanchette, J. C.; Nipkow, T., Nitpick: a counterexample generator for higher-order logic based on a relational model finder, (Kaufmann, M.; Paulson, L. C., Interactive Theorem Proving, First International Conference. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010, Proceedings. Interactive Theorem Proving, First International Conference. Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science (2010), Springer), 131-146 · Zbl 1291.68326
[44] Cruanes, S.; Blanchette, J. C., Extending Nunchaku to dependent type theory, (Blanchette, J. C.; Kaliszyk, C., Proceedings of the First International Workshop on Hammers for Type Theories. Proceedings of the First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016. Proceedings of the First International Workshop on Hammers for Type Theories. Proceedings of the First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016, EPTCS, vol. 210 (July 2016)), 3-12
[45] Ohlbach, H.; Nonnengart, A.; de Rijke, M.; Gabbay, D., Encoding two-valued nonclassical logics in classical logic, (Robinson, J.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 1403-1486, (in 2 volumes) · Zbl 0992.03019
[46] Frege, G., Begriffsschrift. Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (1879), Halle
[47] Benzmüller, C.; Brown, C.; Kohlhase, M., Higher-order semantics and extensionality, J. Symb. Log., 69, 4, 1027-1088 (2004) · Zbl 1071.03024
[48] Benzmüller, C.; Miller, D., Automation of higher-order logic, (Gabbay, D. M.; Siekmann, J. H.; Woods, J., Handbook of the History of Logic, vol. 9, Computational Logic (2014), North Holland, Elsevier), 215-254 · Zbl 1404.03005
[49] Andrews, P. B., General models, descriptions, and choice in type theory, J. Symb. Log., 37, 2, 385-394 (1972) · Zbl 0264.02049
[50] Henkin, L., Completeness in the theory of types, J. Symb. Log., 15, 2, 81-91 (1950) · Zbl 0039.00801
[51] von Wright, G. H., Deontic logic, Mind, 60, 1-15 (1951)
[52] Straßer, C.; Beirlaen, M.; Van De Putte, F., Adaptive logic characterizations of input/output logic, Stud. Log., 104, 5, 869-916 (2016) · Zbl 1364.03034
[53] Straßer, C., Adaptive Logics for Defeasible Reasoning: Applications in Argumentation, Normative Reasoning and Default Reasoning (2013), Springer · Zbl 1350.03003
[54] Hansson, B., An analysis of some deontic logics, Noûs, 3, 4, 373-398 (1969) · Zbl 1366.03069
[55] Åqvist, L., Deontic logic, (Gabbay, D.; Guenthner, F., Handbook of Philosophical Logic, 2nd edition, vol. 8 (2002), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht, Holland), 147-264
[56] Parent, X., Completeness of Åqvist’s systems E and F, Rev. Symb. Log., 8, 1, 164-177 (2015) · Zbl 1371.03027
[57] Kratzer, A., Modals and Conditionals: New and Revised Perspectives (2012), Oxford University Press: Oxford University Press New York · Zbl 1360.03006
[58] Carmo, J.; Jones, A. J.I., Completeness and decidability results for a logic of contrary-to-duty conditionals, J. Log. Comput., 23, 3, 585-626 (2013) · Zbl 1272.03096
[59] Alchourrón, C., Philosophical foundations of deontic logic and the logic of defeasible conditionals, (Meyer, J.-J.; Wieringa, R., Deontic Logic in Computer Science (1993), John Wiley & Sons, Inc.: John Wiley & Sons, Inc. New York), 43-84
[60] Kjos-Hanssen, B., A conflict between some semantic conditions of Carmo and Jones for contrary-to-duty obligations, Stud. Log., 105, 1, 173-178 (2017) · Zbl 1417.03154
[61] Horty, J., Agency and Deontic Logic (2009), Oxford University Press: Oxford University Press London, UK · Zbl 1119.03313
[62] Hansen, J., Reasoning about permission and obligation, (Hansson, S. O., David Makinson on Classical Methods for Non-Classical Problems (2014), Springer: Springer Dordrecht), 287-333 · Zbl 1311.03038
[63] Parent, X.; van der Torre, L., Detachment in normative systems: examples, inference patterns, properties, IfCoLog J. Log. Appl., 4, 2996-3039 (2017)
[64] Makinson, D.; van der Torre, L. W.N., Input/output logics, J. Philos. Log., 29, 4, 383-408 (2000) · Zbl 0964.03002
[65] Horty, J., Reasons as Defaults (2012), Oxford University Press
[66] Hansen, J., Prioritized conditional imperatives: problems and a new proposal, Auton. Agents Multi-Agent Syst., 17, 1, 11-35 (2008)
[67] Palmirani, M.; Governatori, G.; Rotolo, A.; Tabet, S.; Boley, H.; Paschke, A., LegalRuleML: XML-based rules and norms, (Olken, F.; Palmirani, M.; Sottara, D., Rule-Based Modeling and Computing on the Semantic Web (2011), Springer: Springer Berlin, Heidelberg), 298-312
[68] Gordon, T., The Pleading Game: An Artificial Intelligence Model of Procedural Approach (1995), Springer: Springer New York
[69] Sartor, G., Legal Reasoning: A Cognitive Approach to Law (2005), Springer
[70] Pigozzi, G.; van der Torre, L., Arguing about constitutive and regulative norms, J. Appl. Non-Class. Log., 28, 2-3, 189-217 (2018) · Zbl 1436.03141
[71] Steen, A., Higher-order theorem proving and its applications, Inf. Technol., 61, 187-191 (2019)
[72] Steen, A.; Benzmüller, C., Extensional higher-order paramodulation in Leo-III, J. Autom. Reason., 1-34 (2019), Preprint:
[73] Benzmüller, C.; Parent, X., I/O logic in HOL - first steps (2018), Tech. rep., CoRR
[74] Parent, X.; van der Torre, L. W.N., The pragmatic oddity in a norm-based deontic logic, (Keppens, J.; Governatori, G., Proceedings of the 16th edition of the International Conference on Artificial Intelligence and Law. Proceedings of the 16th edition of the International Conference on Artificial Intelligence and Law, ICAIL 2017, London, United Kingdom, June 12-16, 2017 (2017), ACM), 169-178
[75] Parent, X.; van der Torre, L. W.N., I/O logics with a consistency check, (Broersen, J. M.; Condoravdi, C.; Shyam, N.; Pigozzi, G., Deontic Logic and Normative Systems - 14th International Conference. Deontic Logic and Normative Systems - 14th International Conference, DEON 2018, Utrecht, The Netherlands, July 3-6, 2018 (2018), College Publications), 285-299 · Zbl 1418.03098
[76] Benzmüller, C., Automating quantified conditional logics in HOL, (Rossi, F., Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (2013), AAAI Press: AAAI Press Beijing, China), 746-753
[77] Benzmüller, C., Cut-elimination for quantified conditional logic, J. Philos. Log., 46, 3, 333-353 (2017) · Zbl 1417.03282
[78] Parent, X., Maximality vs. optimality in dyadic deontic logic, J. Philos. Log., 43, 6, 1101-1128 (2014) · Zbl 1321.03032
[79] Åqvist, L., An Introduction to Deontic Logic and the Theory of Normative Systems (1987), Bibliopolis: Bibliopolis Naples · Zbl 0645.03001
[80] Goble, L., Axioms for Hansson’s dyadic deontic logics, Filos. Not., 13-61 (2019)
[81] X. Parent, Preference-based semantics for dyadic deontic logics in Hansson’s tradition: a survey of axiomatisation results, in: D. Gabbay, J. Horty, X. Parent, R. van der Meyden, L. van der Torre (Eds.), Handbook of Deontic Logic and Normative Systems, vol. 2, College Publications, London, UK, in press.
[82] Lewis, D., Counterfactuals (1973), Blackwell: Blackwell Oxford · Zbl 0989.03003
[83] Govindarajulu, N. S.; Bringsjord, S., On automating the doctrine of double effect, (Sierra, C., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia (August 19-25, 2017)), 4722-4730
[84] Wisniewski, M.; Steen, A.; Benzmüller, C., LeoPARD - A generic platform for the implementation of higher-order reasoners, (Kerber, M.; Carette, J.; Kaliszyk, C.; Rabe, F.; Sorge, V., Intelligent Computer Mathematics - International Conference. Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. Intelligent Computer Mathematics - International Conference. Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, Lecture Notes in Computer Science, vol. 9150 (2015), Springer), 325-330 · Zbl 1417.68196
[85] Steen, A.; Wisniewski, M.; Benzmüller, C., Agent-based HOL reasoning, (Greuel, G.-M.; Koch, T.; Paule, P.; Sommese, A., Mathematical Software - ICMS 2016, 5th International Congress, Proceedings. Mathematical Software - ICMS 2016, 5th International Congress, Proceedings, Lecture Notes in Computer Science, vol. 9725 (2016), Springer: Springer Berlin, Germany), 75-81 · Zbl 1434.68646
[86] Chisholm, R., Contrary-to-duty imperatives and deontic logic, Analysis, 24, 33-36 (1963)
[87] Lorini, E., Temporal STIT logic and its application to normative reasoning, J. Appl. Non-Class. Log., 2013, 372-399 (2013) · Zbl 1398.03080
[88] Beyleveld, D., The Dialectical Necessity of Morality: An Analysis and Defense of Alan Gewirth’s Argument to the Principle of Generic Consistency (1991), University of Chicago Press
[89] Kaplan, D., On the logic of demonstratives, J. Philos. Log., 8, 1, 81-98 (1979) · Zbl 0415.03004
[90] Kornai, A., Bounding the impact of AGI, J. Exp. Theor. Artif. Intell., 26, 3, 417-438 (2014)
[91] Wisniewski, M.; Steen, A.; Benzmüller, C., Einsatz von Theorembeweisern in der Lehre, (Schwill, A.; Lucke, U., Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam, Commentarii informaticae didacticae. Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam, Commentarii informaticae didacticae, CID (2016), Universitätsverlag Potsdam: Universitätsverlag Potsdam Potsdam, Germany), 81-92
[92] Kaplan, D., Afterthoughts, (Almog, J.; Perry, J.; Wettstein, H., Themes from Kaplan (1989), Oxford University Press), 565-614
[93] Benzmüller, C., Universal (meta-)logical reasoning: the wise men puzzle, Data Brief, 24, Article 103774 pp. (2019)
[94] Sergot, M., Epistemic logic and ‘common knowledge’, (Lecture Course Notes (2008), Department of Computing Imperial College: Department of Computing Imperial College London) (2020)
[95] Benzmüller, C.; Otten, J.; Raths, T., Implementing and evaluating provers for first-order modal logics, (Raedt, L. D.; Bessiere, C.; Dubois, D.; Doherty, P.; Frasconi, P.; Heintz, F.; Lucas, P., ECAI 2012. ECAI 2012, Frontiers in Artificial Intelligence and Applications, vol. 242 (2012), IOS Press), 163-168 · Zbl 1327.68204
[96] Barcan, R. C., A functional calculus of first order based on strict implication, J. Symb. Log., 11, 1, 1-16 (1946) · Zbl 0063.00205
[97] Benzmüller, C.; Woltzenlogel Paleo, B., The inconsistency in Gödel’s ontological argument: a success story for AI in metaphysics, (Kambhampati, S., IJCAI-16, vol. 1-3 (2016), AAAI Press), 936-942
[98] Govindarajulu, N. S.; Bringsjord, S., Ethical regulation of robots must be embedded in their operating systems, (Trappl, R., A Construction Manual for Robots’ Ethical Systems - Requirements, Methods, Implementations, Cognitive Technologies (2015), Springer), 85-99
[99] Arkin, R. C.; Ulam, P.; Wagner, A. R., Moral decision making in autonomous systems: enforcement, moral emotions, dignity, trust, and deception, Proc. IEEE, 100, 3, 571-589 (2012)
[100] Arkin, R. C.; Ulam, P.; Duncan, B., An ethical governor for constraining lethal action in an autonomous system (2009), Georgia Institute of Technology, Tech. Rep. GIT-GVU-09-02
[101] Lowe, E. J., A modal version of the ontological argument, (Moreland, J. P.; Sweis, K. A.; Meister, C. V., Debating Christian Theism (2013), Oxford University Press), 61-71, Ch. 4
[102] Fuenmayor, D.; Benzmüller, C., A computational-hermeneutic approach for conceptual explicitation, (Nepomuceno, A.; Magnani, L.; Salguero, F.; Bares, C.; Fontaine, M., Model-Based Reasoning in Science and Technology. Inferential Models for Logic, Language, Cognition and Computation. Model-Based Reasoning in Science and Technology. Inferential Models for Logic, Language, Cognition and Computation, SAPERE, vol. 49 (2019), Springer), 441-469
[103] (Dignum, V., Special Issue: Ethics and Artificial Intelligence, Ethics and Information Technology, vol. 20 (2018)), 1-3
[104] Winfield, A. F.T.; Jirotka, M., Ethical governance is essential to building trust in robotics and artificial intelligence systems, Philos. Trans. R. Soc., Math. Phys. Eng. Sci., 376, 2133, Article 20180085 pp. (2018)
[105] Dignum, V., Responsible autonomy, (Sierra, C., Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 (2017)), 4698-4704
[106] Scheutz, M., The case for explicit ethical agents, AI Mag., 38, 57-64 (2017)
[107] Anderson, M.; Anderson, S. L., Toward ensuring ethical behavior from autonomous systems: a case-supported principle-based paradigm, Ind. Robot, 42, 4, 324-331 (2015)
[108] Wallach, W.; Allen, C.; Smit, I., Machine morality: bottom-up and top-down approaches for modelling human moral faculties, AI Soc., 22, 4, 565-582 (2008)
[109] Dennis, L. A.; Fisher, M.; Slavkovik, M.; Webster, M., Formal verification of ethical choices in autonomous systems, Robot. Auton. Syst., 77, 1-14 (2016)
[110] Otten, J., Non-clausal connection calculi for non-classical logics, (Schmidt, R. A.; Nalon, C., Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference. Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings. Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference. Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25-28, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10501 (2017), Springer), 209-227 · Zbl 06833558
[111] Schmidt, R. A.; Hustadt, U., First-order resolution methods for modal logics, (Voronkov, A.; Weidenbach, C., Programming Logics - Essays in Memory of Harald Ganzinger. Programming Logics - Essays in Memory of Harald Ganzinger, Lecture Notes in Computer Science, vol. 7797 (2013), Springer), 345-391 · Zbl 1383.03031
[112] Saptawijaya, A.; Pereira, L. M., Logic programming for modeling morality, Log. J. IGPL, 24, 4, 510-525 (2016)
[113] Pereira, L. M.; Saptawijaya, A., Counterfactuals, logic programming and agent morality, (Urbaniak, R.; Payette, G., Applications of Formal Philosophy. Applications of Formal Philosophy, Logic, Argumentation & Reasoning (Interdisciplinary Perspectives from the Humanities and Social Sciences), vol. 14 (2017), Springer: Springer Cham), 25-53
[114] Brown, C. E.; Gauthier, T.; Kaliszyk, C.; Sutcliffe, G.; Urban, J., GRUNGE: a Grand Unified ATP Challenge (2019), e-prints · Zbl 07178973
[115] Benzmüller, C.; Woltzenlogel Paleo, B., Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers, (Schaub, T.; Friedrich, G.; O’Sullivan, B., ECAI 2014. ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263 (2014), IOS Press), 93-98 · Zbl 1366.03169
[116] Gödel, K., Appendix A: Notes in Kurt Gödel’s hand, (Sobel, J., Logic and Theism (1970), Cambridge University Press), 144-145
[117] Scott, D., Appendix B: Notes in Dana Scott’s hand, (Sobel, J., Logic and Theism (1972), Cambridge University Press), 145-146
[118] Benzmüller, C.; Weber, L.; Woltzenlogel Paleo, B., Computer-assisted analysis of the Anderson-Hájek controversy, Log. Univers., 11, 1, 139-151 (2017) · Zbl 1417.03131
[119] Zalta, E. N., Principia logico-metaphysica, draft version (2020), preprint available at
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.