{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T15:47:08Z","timestamp":1725983228316},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319944173"},{"type":"electronic","value":"9783319944180"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94418-0_6","type":"book-chapter","created":{"date-parts":[[2018,7,4]],"date-time":"2018-07-04T12:38:26Z","timestamp":1530707906000},"page":"60-69","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Deontic Logic Reasoning Infrastructure"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Parent","sequence":"additional","affiliation":[]},{"given":"Leendert","family":"van der Torre","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,3]]},"reference":[{"issue":"4","key":"6_CR1","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1108\/IR-12-2014-0434","volume":"42","author":"M Anderson","year":"2015","unstructured":"Anderson, M., Anderson, S.L.: Toward ensuring ethical behavior from autonomous systems: a case-supported principle-based paradigm. Ind. Robot 42(4), 324\u2013331 (2015)","journal-title":"Ind. Robot"},{"key":"6_CR2","unstructured":"Andrews, P.: Church\u2019s type theory. In: Zalta, E. (ed.) The Stanford Encyclopedia of Philosophy, Spring 2014 edn (2014)"},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-94-010-0387-2_3","volume-title":"Handbook of Philosophical Logic","author":"Lennart \u00c5qvist","year":"2002","unstructured":"\u00c5qvist, L.: Deontic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn, vol. 8, pp. 147\u2013264. Kluwer Academic Publishers, Dordrecht, Holland (2002)"},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10992-016-9403-0","volume":"46","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333\u2013353 (2017)","journal-title":"J. Philos. Logic"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-319-70848-5_2","volume-title":"Formal Methods: Foundations and Applications","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, 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\u201311. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70848-5_2"},{"key":"6_CR6","unstructured":"Benzm\u00fcller, 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"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/B978-0-444-51624-4.50005-8","volume-title":"Computational Logic","author":"Christoph Benzm\u00fcller","year":"2014","unstructured":"Benzm\u00fcller, 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\u2013254. North Holland, Elsevier (2014)"},{"key":"6_CR8","unstructured":"Benzm\u00fcller, C., Parent, X.: First experiments with a flexible infrastructure for normative reasoning. Technical report, CoRR (2018). http:\/\/arxiv.org\/abs\/1804.02929"},{"key":"6_CR9","unstructured":"Benzm\u00fcller, C., Parent, X.: I\/O logic in HOL \u2013 first steps. Technical report, CoRR (2018). https:\/\/arxiv.org\/abs\/1803.09681"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Log. Univers. 7(1), 7\u201320 (2013)","journal-title":"Log. Univers."},{"issue":"4","key":"6_CR11","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Sultana, N., Paulson, L.C., Thei\u00df, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s11787-017-0160-9","volume":"11","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-H\u00e1jek controversy. Log. Univers. 11(1), 139\u2013151 (2017)","journal-title":"Log. Univers."},{"key":"6_CR13","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: The inconsistency in G\u00f6del\u2019s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI 2016, vol. 1\u20133, pp. 936\u2013942. AAAI Press (2016)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"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\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"issue":"1","key":"6_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-32347-8_24","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2012","unstructured":"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\u2013360. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_24"},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MIS.2006.82","volume":"21","author":"S Bringsjord","year":"2006","unstructured":"Bringsjord, S., Arkoudas, K., Bello, P.: Toward a general logicist methodology for engineering ethically correct robots. IEEE Intell. Syst. 21, 38\u201344 (2006)","journal-title":"IEEE Intell. Syst."},{"key":"6_CR18","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-94-010-0387-2_4","volume-title":"Handbook of Philosophical Logic","author":"J Carmo","year":"2002","unstructured":"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\u2013343. Springer, Dordrecht (2002). https:\/\/doi.org\/10.1007\/978-94-010-0387-2_4"},{"issue":"3","key":"6_CR19","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1093\/logcom\/exs009","volume":"23","author":"J Carmo","year":"2013","unstructured":"Carmo, J., Jones, A.J.I.: Completeness and decidability results for a logic of contrary-to-duty conditionals. J. Logic Comput. 23(3), 585\u2013626 (2013)","journal-title":"J. Logic Comput."},{"key":"6_CR20","unstructured":"Dennis, L.A., Fischer, M.: Practical challenges in explicit ethical machine reasoning. In: ISAIM 2018, Fort Lauderdale, Florida, USA (2018)"},{"key":"6_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.robot.2015.11.012","volume":"77","author":"LA Dennis","year":"2016","unstructured":"Dennis, L.A., Fisher, M., Slavkovik, M., Webster, M.: Formal verification of ethical choices in autonomous systems. Rob. Auton. Syst. 77, 1\u201314 (2016)","journal-title":"Rob. Auton. Syst."},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"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\u201324 October 2014, p. 7. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987586"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Dignum, V.: Responsible autonomy. In: IJCAI 2017, pp. 4698\u20134704 (2017)","DOI":"10.24963\/ijcai.2017\/655"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-13365-2_6","volume-title":"Multi-disciplinary Trends in Artificial Intelligence","author":"U Furbach","year":"2014","unstructured":"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\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13365-2_6"},{"key":"6_CR25","unstructured":"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)"},{"key":"6_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-8447-0","volume-title":"The Pleading Game: An Artificial Intelligence Model of Procedural Approach","author":"T Gordon","year":"1995","unstructured":"Gordon, T.: The Pleading Game: An Artificial Intelligence Model of Procedural Approach. Springer, New York (1995)"},{"key":"6_CR27","series-title":"Outstanding Contributions to Logic","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-94-007-7759-0_14","volume-title":"David Makinson on Classical Methods for Non-Classical Problems","author":"J Hansen","year":"2014","unstructured":"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\u2013333. Springer, Dordrecht (2014). https:\/\/doi.org\/10.1007\/978-94-007-7759-0_14"},{"issue":"4","key":"6_CR28","doi-asserted-by":"publisher","first-page":"373","DOI":"10.2307\/2214372","volume":"3","author":"Bengt Hansson","year":"1969","unstructured":"Hansson, B.: An analysis of some deontic logics. No$$\\hat{\\text{u}}$$s 3(4), 373\u2013398 (1969)","journal-title":"No\u00fbs"},{"key":"6_CR29","unstructured":"Horty, J.: Agency and Deontic Logic. OUP, London (2009)"},{"key":"6_CR30","unstructured":"Kirchner, D., Benzm\u00fcller, C., Zalta, E.N.: Mechanizing principia logico-metaphysica in functional type theory. CoRR (2017). https:\/\/arxiv.org\/abs\/1711.06542"},{"issue":"4","key":"6_CR31","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1023\/A:1004748624537","volume":"29","author":"D Makinson","year":"2000","unstructured":"Makinson, D., van der Torre, L.W.N.: Input\/output logics. J. Philos. Logic 29(4), 383\u2013408 (2000)","journal-title":"J. Philos. Logic"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"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"},{"issue":"1","key":"6_CR33","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1017\/S1755020314000367","volume":"8","author":"X Parent","year":"2015","unstructured":"Parent, X.: Completeness of \u00c5qvist\u2019s systems E and F. Rev. Symb. Logic 8(1), 164\u2013177 (2015)","journal-title":"Rev. Symb. Logic"},{"key":"6_CR34","unstructured":"Parent, X., van der Torre, L.: Input\/output logic. In: Gabbay et al. [25], pp. 499\u2013544 (2013)"},{"issue":"9","key":"6_CR35","first-page":"2295","volume":"4","author":"X Parent","year":"2017","unstructured":"Parent, X., van der Torre, L.: Detachment in normative systems: examples, inference patterns, properties. IfCoLog J. Logics Appl. 4(9), 2295\u20133039 (2017)","journal-title":"IfCoLog J. Logics Appl."},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Parent, X., van der Torre, L.: The pragmatic oddity in a norm-based semantics. In: Governatori, G. (ed.) ICAIL 2017, Proceedings, pp. 169\u2013178. ACM, New York (2017)","DOI":"10.1145\/3086512.3086529"},{"key":"6_CR37","series-title":"Studies in Applied Philosophy, Epistemology and Rational Ethics","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29354-7","volume-title":"Programming Machine Ethics","author":"LM Pereira","year":"2016","unstructured":"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"},{"key":"6_CR38","volume-title":"Legal Reasoning: A Cognitive Approach to Law","author":"G Sartor","year":"2005","unstructured":"Sartor, G.: Legal Reasoning: A Cognitive Approach to Law. Springer, Dordrecht (2005)"},{"key":"6_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1093\/mind\/LX.237.1","volume":"60","author":"GH Wright von","year":"1951","unstructured":"von Wright, G.H.: Deontic logic. Mind 60, 1\u201315 (1951)","journal-title":"Mind"},{"key":"6_CR40","unstructured":"Zalta, E.N.: Principia logico-metaphysica. Draft version (2016). https:\/\/mally.stanford.edu\/principia.pdf"}],"container-title":["Lecture Notes in Computer Science","Sailing Routes in the World of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94418-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T06:15:56Z","timestamp":1571552156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94418-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944173","9783319944180"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94418-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}