Abstract
A flexible infrastructure for the automation of deontic and normative reasoning is presented. Our motivation is the development, study and provision of legal and moral reasoning competencies in future intelligent machines. Since there is no consensus on the “best” deontic logic formalisms and since the answer may be application specific, a flexible infrastructure is proposed in which candidate logic formalisms can be varied, assessed and compared in experimental ethics application studies. Our work thus links the historically rich research areas of classical higher-order logic, deontic logics, normative reasoning and formal ethics.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
HOL as addressed here refers to a (simply) typed logic of functions, which has been proposed by Church [2]. It provides lambda-notation, as an elegant and useful means to denote unnamed functions, predicates and sets. Types in HOL eliminate paradoxes and inconsistencies. For more information on HOL see the literature [7].
- 2.
The semantical embedding of \(out_1\) as presented here is technically still an approximative solution. For a complete embedding, x needs to be defined as a consequence of an arbitrary number of facts (instead of just i, j and k) in lines 13 and 14.
References
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)
Andrews, P.: Church’s type theory. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2014 edn (2014)
Åqvist, L.: Deontic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn, vol. 8, pp. 147–264. Kluwer Academic Publishers, Dordrecht, Holland (2002)
Benzmüller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333–353 (2017)
Benzmüller, C.: Recent successes with a meta-logical approach to universal logical reasoning (extended abstract). In: da Costa Cavalheiro, S.A., Fiadeiro, J.L. (eds.) SBMF 2017. LNCS, vol. 10623, pp. 7–11. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70848-5_2
Benzmüller, C., Farjami, A., Parent, X.: Faithful semantical embedding of a dyadic deontic logic in HOL. Technical report, CoRR (2018). https://arxiv.org/abs/1802.08454
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Handbook of the History of Logic. Computational Logic, vol. 9, pp. 215–254. North Holland, Elsevier (2014)
Benzmüller, C., Parent, X.: First experiments with a flexible infrastructure for normative reasoning. Technical report, CoRR (2018). http://arxiv.org/abs/1804.02929
Benzmüller, C., Parent, X.: I/O logic in HOL – first steps. Technical report, CoRR (2018). https://arxiv.org/abs/1803.09681
Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Log. Univers. 7(1), 7–20 (2013)
Benzmüller, C., Sultana, N., Paulson, L.C., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015)
Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-Hájek controversy. Log. Univers. 11(1), 139–151 (2017)
Benzmüller, C., Woltzenlogel Paleo, B.: The inconsistency in Gödel’s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI 2016, vol. 1–3, pp. 936–942. AAAI Press (2016)
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)
Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle - superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 345–360. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_24
Bringsjord, S., Arkoudas, K., Bello, P.: Toward a general logicist methodology for engineering ethically correct robots. IEEE Intell. Syst. 21, 38–44 (2006)
Carmo, J., Jones, A.J.I.: Deontic logic and contrary-to-duties. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 8, pp. 265–343. Springer, Dordrecht (2002). https://doi.org/10.1007/978-94-010-0387-2_4
Carmo, J., Jones, A.J.I.: Completeness and decidability results for a logic of contrary-to-duty conditionals. J. Logic Comput. 23(3), 585–626 (2013)
Dennis, L.A., Fischer, M.: Practical challenges in explicit ethical machine reasoning. In: ISAIM 2018, Fort Lauderdale, Florida, USA (2018)
Dennis, L.A., Fisher, M., Slavkovik, M., Webster, M.: Formal verification of ethical choices in autonomous systems. Rob. Auton. Syst. 77, 1–14 (2016)
Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: how it works, and how to use it. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21–24 October 2014, p. 7. IEEE (2014)
Dignum, V.: Responsible autonomy. In: IJCAI 2017, pp. 4698–4704 (2017)
Furbach, U., Schon, C., Stolzenburg, F.: Automated reasoning in deontic logic. In: Murty, M.N., He, X., Chillarige, R.R., Weng, P. (eds.) MIWAI 2014. LNCS (LNAI), vol. 8875, pp. 57–68. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-13365-2_6
Gabbay, D., Horty, J., Parent, X., van der Meyden, R., van der Torre, L. (eds.): Handbook of Deontic Logic and Normative Systems. College Publications, London (2013)
Gordon, T.: The Pleading Game: An Artificial Intelligence Model of Procedural Approach. Springer, New York (1995)
Hansen, J.: Reasoning about permission and obligation. In: Hansson, S.O. (ed.) David Makinson on Classical Methods for Non-Classical Problems. OCL, vol. 3, pp. 287–333. Springer, Dordrecht (2014). https://doi.org/10.1007/978-94-007-7759-0_14
Hansson, B.: An analysis of some deontic logics. No\(\hat{\text{u}}\)s 3(4), 373–398 (1969)
Horty, J.: Agency and Deontic Logic. OUP, London (2009)
Kirchner, D., Benzmüller, C., Zalta, E.N.: Mechanizing principia logico-metaphysica in functional type theory. CoRR (2017). https://arxiv.org/abs/1711.06542
Makinson, D., van der Torre, L.W.N.: Input/output logics. J. Philos. Logic 29(4), 383–408 (2000)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
Parent, X.: Completeness of Åqvist’s systems E and F. Rev. Symb. Logic 8(1), 164–177 (2015)
Parent, X., van der Torre, L.: Input/output logic. In: Gabbay et al. [25], pp. 499–544 (2013)
Parent, X., van der Torre, L.: Detachment in normative systems: examples, inference patterns, properties. IfCoLog J. Logics Appl. 4(9), 2295–3039 (2017)
Parent, X., van der Torre, L.: The pragmatic oddity in a norm-based semantics. In: Governatori, G. (ed.) ICAIL 2017, Proceedings, pp. 169–178. ACM, New York (2017)
Pereira, L.M., Saptawijaya, A.: Programming Machine Ethics. Studies in Applied Philosophy, Epistemology and Rational Ethics, vol. 26. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29354-7
Sartor, G.: Legal Reasoning: A Cognitive Approach to Law. Springer, Dordrecht (2005)
von Wright, G.H.: Deontic logic. Mind 60, 1–15 (1951)
Zalta, E.N.: Principia logico-metaphysica. Draft version (2016). https://mally.stanford.edu/principia.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Benzmüller, C., Parent, X., van der Torre, L. (2018). A Deontic Logic Reasoning Infrastructure. In: Manea, F., Miller, R., Nowotka, D. (eds) Sailing Routes in the World of Computation. CiE 2018. Lecture Notes in Computer Science(), vol 10936. Springer, Cham. https://doi.org/10.1007/978-3-319-94418-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-94418-0_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94417-3
Online ISBN: 978-3-319-94418-0
eBook Packages: Computer ScienceComputer Science (R0)