Paper published in a book (Scientific congresses, symposiums and conference proceedings)
A Deontic Logic Reasoning Infrastructure
Benzmüller, Christoph; Parent, Xavier; van der Torre, Leon
2018 • In Sailing Routes in the World of Computation, 14th Conference on Computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018, Proceedings
[en] 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.
Disciplines :
Computer science
Author, co-author :
Benzmüller, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Parent, Xavier ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
van der Torre, Leon ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
External co-authors :
yes
Language :
English
Title :
A Deontic Logic Reasoning Infrastructure
Publication date :
2018
Event name :
CiE 2018
Event place :
Kiel, Germany
Event date :
from 30-07-2018 to 03-08-2018
Main work title :
Sailing Routes in the World of Computation, 14th Conference on Computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018, Proceedings
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)
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û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)
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)
