diff --git a/thys/GoedelGod/ROOT b/thys/GoedelGod/ROOT
--- a/thys/GoedelGod/ROOT
+++ b/thys/GoedelGod/ROOT
@@ -1,7 +1,8 @@
chapter AFP
session "GoedelGod" (AFP) = "HOL" +
options [timeout = 600]
theories GoedelGod
document_files
"root.tex"
+ "root.bib"
diff --git a/thys/GoedelGod/document/root.bib b/thys/GoedelGod/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/GoedelGod/document/root.bib
@@ -0,0 +1,2167 @@
+@article{J52,
+ Author = {Christoph Benzm\"uller and David Fuenmayor},
+ Journal = {Bulletin of the Section of Logic},
+ Publisher = {Department of Logic, University of Lodz},
+ Keywords = {own, Ontological Argument, Computational
+ Metaphysics, Higher Order Logic, Semantic Embedding,
+ Modal Logics, Automated Reasoning, Ontology
+ Reasoning},
+ Title = {Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of {G\"odel's} Ontological Argument},
+ OPTUrl = {https://czasopisma.uni.lodz.pl/bulletin/},
+ Year = 2020,
+ Volume = {49},
+ Number = {2},
+ Doi = {10.18778/0138-0680.2020.08},
+ OPTAddendum = {Preprint: \url{https://www.researchgate.net/publication/336742445}},
+ Pages = {127-148},
+}
+
+@InProceedings{C85,
+ Keywords = {own, Ontological Argument, Computational
+ Metaphysics, Higher Order Logic, Semantic Embedding,
+ Modal Logics, Automated Reasoning, Ontology
+ Reasoning},
+ title = {{A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument}},
+ author = {Benzmüller, Christoph},
+ booktitle = {{Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020}},
+ pages = {779--789},
+ year = {2020},
+ month = {9},
+ doi = {10.24963/kr.2020/80},
+ url = {https://doi.org/10.24963/kr.2020/80},
+ publisher = {{IJCAI} organization},
+}
+
+@article{J48,
+Author = {Benzm{\"u}ller, Christoph and Parent, Xavier and van
+ der Torre, Leendert},
+ Keywords = {own, Normative Reasoning, Deontic Logic, Machine Ethics, Formal Methods, Automated Reasoning, ProoF Assistants, Explainable AI},
+Journal = {Artificial Intelligence (accepted for publication)},
+Publisher = {Elsevier},
+Title = {Designing Normative Theories for Ethical and Legal Reasoning:
+ LogiKEy Framework, Methodology, and Tool Support},
+Year = 2020,
+Pages = {1--50},
+Addendum = {Preprint: \url{https://www.researchgate.net/publication/331986665}},
+}
+
+
+@InCollection{odifreddi00:_ultraf_dictat_gods,
+ author = {Piergiorgio Odifreddi},
+ title = {Ultrafilters, Dictators, and Gods},
+ booktitle = {Finite Versus Infinite. Discrete Mathematics and Theoretical Computer Science},
+ publisher = {Springer, London},
+ year = 2000,
+ editor = {Cristian Calude and Gheorghe Paun},
+ pages = {239-245}}
+
+@book{1965proslogion,
+ title={Proslogion},
+ author={Charlesworth, M.J.},
+ lccn=65005321,
+ url={https://books.google.lu/books?id=TtFDAQAAMAAJ},
+ year=1965,
+ publisher={Clarendon Press}
+}
+
+@Article{bjoerdal18,
+ author = {Frode Alfson Bj{\o}rdal},
+ title = {All Properties are Divine or God Exists -- The Sacred Thesis and its Ontological Argument},
+ journal = {Logic and Logical Philosophy},
+ year = 2018,
+ volume = 27,
+ number = 3}
+
+@Unpublished{Swietorzecka19,
+ author = {Kordula \'Swi\c etorzecka},
+ title = {Identity or equality of {Gödelian} God},
+ note = {Draft paper, private communication},
+ month = {May},
+ year = 2019}
+
+@article{J35,
+ Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
+ Journal = {Archive of Formal Proofs},
+ Keywords = {own, Automated Reasoning, Interactive Proof,
+ Ontology Reasoning, Higher Order Logic,
+ Computational Metaphysics},
+ Note = {Note: verified data publication},
+ Title = {{Types, Tableaus and G{\"o}del's God in
+ Isabelle/HOL}},
+ Url =
+ {http://afp.sourceforge.net/entries/Types_Tableaus_and_Goedels_God.shtml},
+ Year = 2017,
+ Pages = {1--34},
+}
+
+
+
+@inproceedings{R74,
+ Author = {Benzm{\"u}ller, Christoph},
+ Title = {Computational Metaphysics: New Insights on {G{\"o}del's} Ontological Argument and Modal Collapse},
+ Editor = {Sr\'{e}cko Kova\v{c} and Kordula Swietorzecka},
+ Booktitle = {Formal Methods and Science in Philosophy III, Informal Proceedings},
+ Year = 2019,
+ Pages = {3--4},
+ Address = {Dubrovnik, Croatia},
+ Url = {http://christoph-benzmueller.de/papers/2019-FMSPh-Proceedings.pdf},
+}
+
+@incollection{Kovacs2012,
+ year = 2012,
+ editor = {Miroslaw Szatkowski},
+ pages = {50--323},
+ author = {Sr\'{e}cko Kova\v{c}},
+ booktitle = {Ontological Proofs Today},
+ publisher = {Ontos Verlag},
+ title = {Modal Collapse in {G\"odel's} Ontological Proof}
+}
+
+@InCollection{sep-logic-modal,
+ author = {Garson, James},
+ title = {Modal Logic},
+ booktitle = {The Stanford Encyclopedia of Philosophy},
+ editor = {Edward N. Zalta},
+ howpublished = {\url{https://plato.stanford.edu/archives/fall2018/entries/logic-modal/}},
+ year = {2018},
+ edition = {Fall 2018},
+ publisher = {Metaphysics Research Lab, Stanford University}
+}
+
+@article{J47,
+Author = {Kirchner, Daniel and Benzm{\"u}ller, Christoph and Zalta, Edward N.},
+Journal = {Open Philosophy},
+Title = {Computer Science and Metaphysics: A Cross-Fertilization},
+Editor = {Patrick Grim},
+Year = 2019,
+Volume = 2,
+Issue = 1,
+Pages = {230–251},
+Doi = {10.1515/opphil-2019-0015},
+OPTNote = {Preprint: \url{http://doi.org/10.13140/RG.2.2.25229.18403}},
+OPTUrl = {https://arxiv.org/abs/1905.00787},
+}
+
+@InCollection{J43,
+ author = {Benzm\"uller, Christoph and Andrews, Peter},
+ title = {Church's Type Theory},
+ booktitle = {The Stanford Encyclopedia of Philosophy},
+ editor = {Edward N. Zalta},
+ howpublished = {\url{https://plato.stanford.edu/entries/type-theory-church/}},
+ year = 2019,
+ edition = {Summer 2019},
+ OPTpages = {pp.~1--62 (in pdf version)},
+ publisher = {Metaphysics Research Lab, Stanford University},
+ url = {https://plato.stanford.edu/entries/type-theory-church/},
+}
+
+@InCollection{Lowe2013,
+ author= {Lowe, Edward Jonathan},
+ editor= {Moreland, J. P. and Sweis, K. A. and Meister, C. V.},
+ title= {A Modal Version of the Ontological Argument},
+ booktitle = {Debating Christian Theism},
+ publisher = {Oxford University Press},
+ year = {2013},
+ chapter= {4},
+ pages= {61--71},
+ isbn = {9780199981434}
+}
+
+@article{zalta1999,
+ Author = {Edward N. Zalta},
+ Title = {{Natural Numbers and Natural Cardinals as Abstract Objects:
+A Partial Reconstruction of {Frege's} Grundgesetze in Object
+Theory}},
+ Journal = {Journal of Philosophical Logic},
+ volume = {28},
+ number = {6},
+ year = {1999},
+ pages = {619--660}
+}
+
+@article{zalta1993,
+ Author = {Edward N. Zalta},
+ Title = {{Twenty-Five Basic Theorems in Situation and World Theory}},
+ Journal = {Journal of Philosophical Logic},
+ volume = {22},
+ number = {4},
+ year = {1993},
+ pages = {385--428}
+}
+
+@article{OppenheimerZalta1991,
+ author = {Paul E. Oppenheimer and Edward N. Zalta},
+ title = {On the Logic of the Ontological Argument},
+ volume = {5},
+ journal = {Philosophical Perspectives},
+ year = {1991},
+ pages = {509--529}
+}
+
+@article{PelletierZalta,
+ Author = {Francis J. Pelletier and Edward N. Zalta},
+ Title = {{How to Say Goodbye to the Third Man}},
+ Journal = {No\^us},
+ volume = {34},
+ number = {2},
+ year = {2000},
+ pages = {165--202}
+}
+
+
+
+@inproceedings{C74,
+ Author = {Christoph Benzm{\"u}ller and Fuenmayor, David},
+ Booktitle = {Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science \& Spiritual Quest (AISSQ), 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India},
+ Editor = {Gosh, Sudipto and Uppalari, Ramgopal and Rao, K. Vasudeva and Agarwal, Varun and Sharma, Sushant},
+ Keywords = {own, Ontological Argument, Computational Metaphysics, Higher Order Logic, Semantic Embedding, Modal Logics, Automated Reasoning, Ontology Reasoning},
+ Publisher = {The Bhaktivedanta Institute, Kolkata, \url{www.binstitute.org}},
+ Title = {Can Computers Help to Sharpen our Understanding of Ontological Arguments?},
+ Url = {http://christoph-benzmueller.de/papers/C74.pdf},
+ pages = {195-226},
+ isbn = {81-89635-31-X},
+ Comment = {DOI (preprint): 10.13140/RG.2.2.31921.84323},
+ Doi = {10.13140/RG.2.2.31921.84323},
+ Year = 2018,
+}
+
+@inproceedings{HuffmanK13,
+ author = {Brian Huffman and
+ Ondrej Kuncar},
+ title = {Lifting and Transfer: {A} Modular Design for Quotients in {Isabelle/HOL}},
+ booktitle = {Certified Programs and Proofs --- Third International Conference, {CPP}
+ 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
+ pages = {131--146},
+ year = {2013},
+ editor = {Georges Gonthier and
+ Michael Norrish},
+ series = {Lecture Notes in Computer Science},
+ volume = {8307},
+ publisher = {Springer},
+}
+
+
+@inproceedings{C70,
+ Author = {Alexander Steen and Christoph Benzm{\"u}ller},
+ Booktitle = {Automated Reasoning. IJCAR 2018},
+ Editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
+ Keywords = {own, Higher Order Logic, Automated Reasoning, LEO Prover},
+ Publisher = {Springer, Cham},
+ Series = {Lecture Notes in Computer Science},
+ Title = {The Higher-Order Prover {Leo-III}},
+ Url = {http://christoph-benzmueller.de/papers/C70.pdf},
+ volume = 10900,
+ pages = {108-116},
+ doi = {10.1007/978-3-319-94205-6_8},
+ isbn = {978-3-319-94204-9},
+ Year = 2018,
+}
+
+@article{J30,
+ Author = {Christoph Benzm{\"u}ller and Nik Sultana and Lawrence C. Paulson and Frank Thei{\ss}},
+ Doi = {10.1007/s10817-015-9348-y},
+ Journal = {Journal of Automated Reasoning},
+ Keywords = {own, Automated Reasoning, Interactive Proof, Ontology Reasoning, LEO Prover, Higher Order Logic, DFG-2501-Selected},
+ Number = 4,
+ Pages = {389-404},
+ Title = {The Higher-Order Prover {LEO-II}},
+ Url = {http://christoph-benzmueller.de/papers/J30.pdf},
+ Volume = 55,
+ Year = 2015,
+}
+
+@inproceedings{Nunchaku,
+ author = {Cruanes, Simon and
+ Blanchette, Jasmin C.},
+ title = {Extending Nunchaku to Dependent Type Theory},
+ booktitle = {Proceedings First International Workshop on Hammers for Type Theories,
+ HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016.},
+ pages = {3--12},
+ year = {2016},
+ doi = {10.4204/EPTCS.210.3},
+ series = {{EPTCS}},
+ volume = {210},
+ url = {https://doi.org/10.4204/EPTCS.210},
+}
+
+
+@misc{W62,
+ Author = {Benzm\"uller, Christoph and Farjami, Ali and Parent, Xavier},
+ OPTBooktitle = {MIREL 2018},
+ OPTEditor = {},
+ Keywords = {own, Dyadic Deontic Logic E, Preference Models, Higher Order Logic, Semantic Embedding, Automated Reasoning},
+ Note = {MIREL 2018 workshop on MIning and REasoning with Legal texts; available online at \url{http://orbilu.uni.lu/handle/10993/37014}},
+ Url = {http://orbilu.uni.lu/handle/10993/37014},
+ Title = {Aqvist's Dyadic Deontic Logic {E} in {HOL}},
+ Year = 2018,
+}
+
+
+@misc{W63,
+ Author = {Farjami, Ali and Meder, Paul and Parent, Xavier and Benzm\"uller, Christoph},
+ OPTBooktitle = {MIREL 2018},
+ OPTEditor = {},
+ Keywords = {own, Input/Output Logic, Higher Order Logic, Semantic Embedding, Automated Reasoning, General Data Protection Regulation},
+ Note = {MIREL 2018 workshop on MIning and REasoning with Legal texts; available online at \url{http://orbilu.uni.lu/handle/10993/37013}},
+ Title = { {I/O} Logic in {HOL}},
+ Year = 2018,
+}
+
+@inproceedings{C71,
+ Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and Parent, Xavier},
+ Booktitle = {Deontic Logic and Normative Systems --- 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018},
+ Editor = {Jan Broersen and Cleo Condoravdi and Shyam Nair and Gabriella Pigozzi},
+ Keywords = {own, Higher Order Logic, Deontic Logic,
+ Automated Reasoning, Universal Reasoning},
+ Publisher = {College Publications},
+ pages = {33-50},
+ OPTSeries = {},
+ Title = {A Dyadic Deontic Logic in {HOL}},
+ Url = {http://christoph-benzmueller.de/papers/C71.pdf},
+ OPTVolume = 9706,
+ Year = 2018,
+ isbn = {978-1-84890-278-7},
+ note = {(John-Jules Meyer Best Paper Award)},
+}
+
+@article{J41,
+ author = {Christoph Benzm{\"u}ller},
+ title = {Universal (Meta-)Logical Reasoning: Recent Successes},
+ journal = {Science of Computer Programming},
+ year = 2019,
+ volume = 172,
+ month = {3},
+ pages = {48-62},
+ OPTnote = {DOI (preprint): \url{http://dx.doi.org/10.13140/RG.2.2.11039.61609/2}},
+ doi = {10.1016/j.scico.2018.10.008},
+ url = {https://doi.org/10.1016/j.scico.2018.10.008}
+}
+
+
+@inproceedings{C47,
+ Address = {Berlin, Germany},
+ Author = {Christoph Benzm{\"u}ller and Maximilian Claus and Nik Sultana},
+ Booktitle = {PxTP 2015},
+ Comment = {slides},
+ Doi = {10.4204/EPTCS.186.5},
+ Editor = {Cezary Kaliszyk and Andrei Paskevich},
+ Issn = {2075-2180},
+ Keywords = {own, Automated Reasoning, Interactive Proof, Ontology Reasoning, LEO Prover, Higher Order Logic},
+ Pages = {27-41},
+ Publisher = {EPTCS},
+ Title = {Systematic Verification of the Modal Logic Cube in {Isabelle/HOL}},
+ Url = {http://christoph-benzmueller.de/papers/C47.pdf},
+ Volume = 186,
+ Year = 2015,
+}
+
+@inproceedings{C72,
+ Author = {Benzm{\"u}ller, Christoph},
+ Booktitle = {Deontic Logic and Normative Systems --- 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018},
+ Editor = {Jan Broersen and Cleo Condoravdi and Shyam Nair and Gabriella Pigozzi},
+ Keywords = {own, Higher Order Logic, Deontic Logic,
+ Automated Reasoning, Universal Reasoning},
+ Publisher = {College Publications},
+ pages = 7,
+ Title = {A Flexible Infrastructure for Normative Reasoning (invited keynote abstract)},
+ Url = {http://christoph-benzmueller.de/papers/C72.pdf},
+ Volume = 9706,
+ Year = 2018,
+ isbn = {978-1-84890-278-7},
+}
+
+@inproceedings{C44,
+ Author = {Christoph Benzm{\"{u}}ller and Woltzenlogel Paleo, Bruno},
+ Booktitle = {Computer Science --- Theory and Applications --- 10th International Computer Science Symposium in Russia, {CSR} 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings},
+ Doi = {10.1007/978-3-319-20297-6_25},
+ Editor = {Lev D. Beklemishev and Daniil V. Musatov},
+ Keywords = {own, Automated Reasoning, Interactive Proof, Ontology Reasoning, LEO Prover, Higher Order Logic, Computational Metaphysics},
+ Pages = {398--411},
+ Publisher = {Springer},
+ Series = {Lecture Notes in Computer Science},
+ Title = {Interacting with Modal Logics in the {Coq} Proof Assistant},
+ Url = {http://christoph-benzmueller.de/papers/C44.pdf},
+ Volume = 9139,
+ Year = 2015
+}
+
+@article{B17,
+ Author = {David Fuenmayor and Christoph Benzm\"uller},
+ Journal = {Journal of Applied Logic - IfCoLoG Journal of Logics
+ and their Applications (special issue on Formal
+ Approaches to the Ontological Argument)},
+ Volume = 5,
+ Number = 7,
+ Pages = {1567-1603},
+ Editors = {Silvestre, Ricardo and B\'{e}ziau, Jean-Yves},
+ Keywords = {own, Automated Reasoning, Interactive Proof,
+ Ontology Reasoning, Higher Order Logic,
+ Computational Metaphysics},
+ Title = {A Case Study On Computational Hermeneutics:
+ {E.~J.~Lowe's} Modal Ontological Argument},
+ Year = 2018,
+}
+
+
+
+@book{lambek86:_introd_higher_order_categ_logic,
+ author = {Lambek, J. and Scott, P.J.},
+ publisher = {Cambridge University Press},
+ title = {Introduction to Higher Order Categorical Logic},
+ year = {1986},
+}
+
+@book{jacobs99:_categ_logic_type_theor,
+ author = {B. Jacobs},
+ publisher = {North Holland, Elsevier},
+ series = {Studies in Logic and the Foundations of Mathematics},
+ title = {Categorical Logic and Type Theory},
+ volume = {141},
+ year = {1999},
+}
+
+@book{andreka17:_univer_algeb_logic,
+ author = {Andreka, H. and N\'emeti, I. and Sain, I.},
+ publisher = {Birkh\"auser Basel},
+ series = {Studies in Universal Logic},
+ title = {Universal Algebraic Logic},
+ year = {2017},
+}
+
+@article{moss99:_coalg_logic,
+ author = {L.S. Moss},
+ journal = {Annals of Pure and Applied Logic},
+ number = {1-3},
+ pages = {277-317},
+ title = {Coalgebraic Logic},
+ volume = {96},
+ year = {1999},
+}
+
+@article{rutten00:_univer,
+ author = {J.J.M.M. Rutten},
+ journal = {Theoretical Computer Science},
+ number = {1},
+ pages = {3-80},
+ title = {Universal coalgebra: a theory of systems},
+ volume = {249},
+ year = {2000},
+}
+
+@inproceedings{DBLP:conf/icfem/GuttmannSW11,
+ author = {Walter Guttmann and Georg Struth and Tjark Weber},
+ booktitle = {Proc. of ICFEM 2011},
+ editor = {Shengchao Qin and Zongyan Qiu},
+ pages = {617-632},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {Automating Algebraic Methods in {Isabelle}},
+ volume = {6991},
+ year = {2011},
+}
+
+@article{foster15:_fine_struc_regul_algeb,
+ author = {S. Foster and G. Struth},
+ journal = {Journal of Automated Reasoning},
+ number = {2},
+ pages = {165-197},
+ title = {On the Fine-Structure of Regular Algebra},
+ volume = {54},
+ year = {2015},
+}
+
+@article{Church40,
+ author = {Alonzo Church},
+ journal = {Journal of Symbolic Logic},
+ pages = {56--68},
+ title = {A Formulation of the Simple Theory of Types},
+ volume = {5},
+ year = {1940},
+}
+
+@InCollection{AndrewsSEP,
+ author = {Andrews, Peter},
+ title = {Church's Type Theory},
+ booktitle = {The Stanford Encyclopedia of Philosophy},
+ editor = {Edward N. Zalta},
+ howpublished = {\url{https://plato.stanford.edu/archives/sum2018/entries/type-theory-church/}},
+ year = {2018},
+ edition = {Summer 2018},
+ publisher = {Metaphysics Research Lab, Stanford University}
+}
+
+@incollection{B5,
+ author = {Christoph Benzm{\"u}ller and Dale Miller},
+ booktitle = {Handbook of the History of Logic, Volume 9 ---
+ Computational Logic},
+ editor = {Gabbay, Dov M. and Siekmann, J\"org H. and
+ Woods, John},
+ pages = {215-254},
+ publisher = {North Holland, Elsevier},
+ title = {Automation of Higher-Order Logic},
+ year = {2014},
+ doi = {10.1016/B978-0-444-51624-4.50005-8},
+ isbn = {978-0-444-51624-4},
+ OPTurl = {http://christoph-benzmueller.de/papers/B5.pdf},
+}
+
+@article{J23,
+ author = {Christoph Benzm{\"u}ller and Lawrence Paulson},
+ journal = {Logica Universalis},
+ number = {1},
+ pages = {7-20},
+ title = {Quantified Multimodal Logics in Simple Type Theory},
+ volume = {7},
+ year = {2013},
+ doi = {10.1007/s11787-012-0052-y},
+ OPTurl = {http://christoph-benzmueller.de/papers/J23.pdf},
+}
+
+@book{frege79:_begrif,
+ author = {Gottlob Frege},
+ publisher = {Halle},
+ title = {Begriffsschrift. Eine der arithmetischen
+ nachgebildete Formelsprache des reinen Denkens},
+ year = {1879},
+}
+
+@article{J6,
+ author = {Christoph Benzm{\"u}ller and Chad Brown and
+ Michael Kohlhase},
+ journal = {Journal of Symbolic Logic},
+ number = {4},
+ pages = {1027-1088},
+ title = {Higher-Order Semantics and Extensionality},
+ volume = {69},
+ year = {2004},
+ doi = {10.2178/jsl/1102022211},
+ OPTurl = {http://christoph-benzmueller.de/papers/J6.pdf},
+}
+
+@book{andrews2002introduction,
+ author = {Peter B Andrews},
+ publisher = {Springer},
+ series = {Applied Logic Series},
+ title = {An Introduction to Mathematical Logic and Type
+ Theory: To Truth Through Proof},
+ volume = {27},
+ year = {2002},
+}
+
+@book{Isabelle2,
+ author = {Nipkow, Tobias and Paulson, Lawrence C. and
+ Wenzel, Makarius},
+ volume = {2283},
+ publisher = {Springer},
+ series = {LNCS},
+ title = {{{Isabelle/HOL: A Proof Assistant for Higher-Order
+ Logic}}},
+ year = {2002},
+}
+
+@book{Coq,
+ author = {Bertot, Y. and Casteran, P.},
+ publisher = {Springer},
+ title = {{Interactive Theorem Proving and Program
+ Development}},
+ year = {2004},
+}
+
+
+
+
+@inproceedings{Satallax,
+ author = {Chad E. Brown},
+ booktitle = {Automated Reasoning --- 6th International Joint
+ Conference, {IJCAR} 2012, Manchester, UK, June 26-29,
+ 2012. Proceedings},
+ editor = {Bernhard Gramlich and Dale Miller and Uli Sattler},
+ pages = {111--117},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {Satallax: An Automatic Higher-Order Prover},
+ volume = {7364},
+ year = {2012},
+ isbn = {978-3-642-31364-6},
+}
+
+@inproceedings{Nitpick,
+ author = {Jasmin C. Blanchette and Tobias Nipkow},
+ booktitle = {Interactive Theorem Proving --- {ITP} 2010},
+ editor = {M.~Kaufmann and L.~C.~Paulson},
+ pages = {131--146},
+ publisher = {Springer},
+ series = {LNCS},
+ title = {Nitpick: {A} Counterexample Generator for
+ Higher-Order Logic Based on a Relational Model
+ Finder},
+ volume = {6172},
+ year = {2010},
+}
+
+@article{Sledgehammer,
+ author = {Blanchette, Jasmin C. and B\"ohme, Sascha and
+ Paulson, Lawrence C.},
+ journal = {Journal of Automated Reasoning},
+ number = {1},
+ pages = {109-128},
+ publisher = {Springer},
+ title = {Extending {Sledgehammer} with {SMT} Solvers},
+ volume = {51},
+ year = {2013},
+ issn = {0168-7433},
+ language = {English},
+}
+
+@inproceedings{E,
+ author = {Stephan Schulz},
+ booktitle = {Logic for Programming, Artificial Intelligence, and
+ Reasoning -- 19th International Conference, LPAR-19,
+ Stellenbosch, South Africa, December 14-19, 2013.
+ Proceedings},
+ editor = {Kenneth L. McMillan and Aart Middeldorp and
+ Andrei Voronkov},
+ pages = {735--743},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {System Description: {E} 1.8},
+ volume = {8312},
+ year = {2013},
+ doi = {10.1007/978-3-642-45221-5},
+ isbn = {978-3-642-45220-8},
+ OPTurl = {http://dx.doi.org/10.1007/978-3-642-45221-5},
+}
+
+@inproceedings{CVC4,
+ author = {Morgan Deters and Andrew Reynolds and Tim King and
+ Clark W. Barrett and Cesare Tinelli},
+ booktitle = {Formal Methods in Computer-Aided Design, {FMCAD}
+ 2014, Lausanne, Switzerland, October 21-24, 2014},
+ editor = {Koen Claessen and Viktor Kuncak},
+ pages = {7},
+ publisher = {{IEEE}},
+ title = {A tour of {CVC4:} {How} it works, and how to use it},
+ year = {2014},
+ isbn = {978-0-9835678-4-4},
+}
+
+@InProceedings{Z3,
+author="de Moura, Leonardo
+and Bj{\o}rner, Nikolaj",
+editor="Ramakrishnan, C. R.
+and Rehof, Jakob",
+title="Z3: An Efficient SMT Solver",
+booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
+year="2008",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="337--340",
+abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.",
+isbn="978-3-540-78800-3"
+}
+
+@inproceedings{Spass,
+ author = {Jasmin C. Blanchette and Andrei Popescu and
+ Daniel Wand and Christoph Weidenbach},
+ booktitle = {Interactive Theorem Proving --- Third International
+ Conference, {ITP} F2012, Princeton, NJ, USA, August
+ 13-15, 2012. Proceedings},
+ editor = {Lennart Beringer and Amy P. Felty},
+ pages = {345--360},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {{More {SPASS} with Isabelle -- Superposition with
+ Hard Sorts and Configurable Simplification}},
+ volume = {7406},
+ year = {2012},
+ isbn = {978-3-642-32346-1},
+}
+
+@inproceedings{Vampire,
+ author = {Laura Kov{\'{a}}cs and Andrei Voronkov},
+ booktitle = {Computer Aided Verification - 25th International
+ Conference, {CAV} 2013, Saint Petersburg, Russia,
+ July 13-19, 2013. Proceedings},
+ editor = {Natasha Sharygina and Helmut Veith},
+ pages = {1--35},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {{First-Order Theorem Proving and Vampire}},
+ volume = {8044},
+ year = {2013},
+ isbn = {978-3-642-39798-1},
+}
+
+@phdthesis{BaldoniPhD,
+ author = {Matteo Baldoni},
+ note = {(Revised version dated July 9, 2003)},
+ school = {Dipartimento di Informatica, Universit\'a degli Studi
+ di Torino},
+ title = {Normal Multimodal Logics: Automatic Deduction and
+ Logic Programming Extension},
+ year = {2003},
+}
+
+@book{fagin04:_reason_about_knowl,
+ author = {Ronald Fagin and Halpern, Joseph Y. and Yoram Moses and
+ Moshe Vardi},
+ publisher = {The MIT Press},
+ title = {Reasoning About Knowledge},
+ year = {2004},
+}
+
+@incollection{DBLP:books/el/RV01/OhlbachNRG01,
+ author = {Ohlbach, H.J. and Nonnengart, A. and de Rijke, M. and
+ Gabbay, D.M.},
+ booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
+ editor = {J.A. Robinson and A. Voronkov},
+ pages = {1403--1486},
+ publisher = {Elsevier and {MIT} Press},
+ title = {Encoding Two-Valued Nonclassical Logics in Classical
+ Logic},
+ year = {2001},
+}
+
+@article{J25,
+ author = {Christoph Benzm{\"u}ller},
+ journal = {Annals of Mathematics and Artificial Intelligence},
+ number = {1--2},
+ pages = {103-128},
+ title = {Combining and Automating Classical and Non-Classical
+ Logics in Classical Higher-Order Logic},
+ volume = {62},
+ year = {2011},
+ doi = {10.1007/s10472-011-9249-7},
+ OPTurl = {http://christoph-benzmueller.de/papers/J25.pdf},
+}
+
+@misc{sergot08:_epist_logic_common_knowl,
+ author = {Marek Sergot},
+ howpublished = {Lecture Course Notes, Department of Computing
+ Imperial College, London,
+ \url{https://www.doc.ic.ac.uk/~mjs/teaching/ModalTemporal499/Epistemic_499_v0809_2up.pdf}},
+ title = {Epistemic Logic and ‘Common Knowledge’},
+ year = {2008},
+}
+
+@incollection{sep-dynamic-epistemic,
+ author = {Baltag, Alexandru and Renne, Bryan},
+ booktitle = {The Stanford Encyclopedia of Philosophy},
+ edition = {Winter 2016},
+ editor = {Edward N. Zalta},
+ howpublished =
+ {\url{https://plato.stanford.edu/archives/win2016/entries/dynamic-epistemic/}},
+ publisher = {Metaphysics Research Lab, Stanford University},
+ title = {Dynamic Epistemic Logic},
+ year = {2016},
+}
+
+@article{J22,
+ author = {Geoff Sutcliffe and Christoph Benzm{\"u}ller},
+ journal = {Journal of Formalized Reasoning},
+ number = {1},
+ pages = {1-27},
+ title = {Automated Reasoning in Higher-Order Logic using the
+ {TPTP THF} Infrastructure},
+ volume = {3},
+ year = {2010},
+ issn = {1972-5787},
+ OPTurl = {http://christoph-benzmueller.de/papers/J22.pdf},
+}
+
+@article{J5,
+ author = {Christoph Benzm{\"u}ller},
+ journal = {Synthese},
+ number = {1-2},
+ pages = {203-235},
+ title = {Comparing Approaches to Resolution based Higher-Order
+ Theorem Proving},
+ volume = {133},
+ year = {2002},
+ abstract = {We investigate several approaches to resolution based
+ automated theorem proving in classical higher-order
+ logic (based on Church's simply typed lambda
+ calculus) and discuss their requirements with respect
+ to Henkin completeness and full extensionality. In
+ particular we focus on Andrews' higher-order
+ resolution [Andrews71], Huet's constrained resolution
+ [Huet72], higher-order $E$-resolution, and
+ extensional higher-order resolution
+ [BenzmuellerKohlhase98]. With the help of examples we
+ illustrate the parallels and differences of the
+ extensionality treatment of these approaches and
+ demonstrate that extensional higher-order resolution
+ is the sole approach that can completely avoid
+ additional extensionality axioms.},
+ doi = {10.1023/A:1020840027781},
+ issn = {0039-7857},
+ OPTurl = {http://christoph-benzmueller.de/papers/J5.pdf},
+}
+
+@article{J12,
+ author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
+ Serge Autexier},
+ journal = {Journal of Applied Logic},
+ number = {4},
+ pages = {533-559},
+ title = {Computer Supported Mathematics with {OMEGA}},
+ volume = {4},
+ year = {2006},
+ doi = {10.1016/j.jal.2005.10.008},
+ OPTurl = {http://christoph-benzmueller.de/papers/J12.pdf},
+}
+
+@incollection{B10,
+ author = {Serge Autexier and Christoph Benzm\"uller and
+ Dominik Dietrich and J\"org Siekmann},
+ booktitle = {Resource-Adaptive Cognitive Processes},
+ editor = {Matthew W. Crocker and J\"org Siekmann},
+ pages = {389-423},
+ publisher = {Springer},
+ series = {Cognitive Technologies},
+ title = {{OMEGA}: Resource-Adaptive Processes in an Automated
+ Reasoning Systems},
+ year = {2010},
+ doi = {10.1007/978-3-540-89408-7_17},
+ isbn = {978-3-540-89407-0},
+ OPTurl = {http://christoph-benzmueller.de/papers/B10.pdf},
+}
+
+@incollection{B1,
+ author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
+ Armin Fiedler and Andreas Meier and Immanuel Normann and
+ Martin Pollet},
+ booktitle = {Thirty Five Years of Automating Mathematics},
+ editor = {Fairouz Kamareddine},
+ pages = {271-314},
+ publisher = {Kluwer Academic Publishers},
+ series = {Applied Logic series (28)},
+ title = {Proof Development in {OMEGA}: The Irrationality of
+ Square Root of 2},
+ year = {2003},
+ doi = {10.1007/978-94-017-0253-9_11},
+ isbn = {978-1-402-01656-1},
+ OPTurl = {http://christoph-benzmueller.de/papers/B1.pdf},
+}
+
+@incollection{B11,
+ author = {Christoph Benzm\"uller and Marvin Schiller and
+ J\"org Siekmann},
+ booktitle = {Resource-Adaptive Cognitive Processes},
+ editor = {Matthew W. Crocker and J\"org Siekmann},
+ pages = {291-311},
+ publisher = {Springer},
+ series = {Cognitive Technologies},
+ title = {Resource-Bounded Modelling and Analysis of
+ Human-Level Interactive Proofs},
+ year = {2010},
+ doi = {10.1007/978-3-540-89408-7_13},
+ isbn = {978-3-540-89407-0},
+ OPTurl = {http://christoph-benzmueller.de/papers/B11.pdf},
+}
+
+@article{J27,
+ author = {Christoph Benzm{\"u}ller and Adam Pease},
+ journal = {Journal of Web Semantics},
+ pages = {104-117},
+ title = {Higher-order Aspects and Context in {SUMO}},
+ volume = {12-13},
+ year = {2012},
+ doi = {10.1016/j.websem.2011.11.008},
+ OPTurl = {http://christoph-benzmueller.de/papers/J27.pdf},
+}
+
+@incollection{B9,
+ author = {Christoph Benzm{\"u}ller and Lawrence Paulson},
+ booktitle = {Reasoning in Simple Type Theory --- Festschrift in
+ Honor of {Peter B. Andrews} on His 70th Birthday},
+ editor = {Christoph Benzm{\"u}ller and Chad Brown and
+ J{\"o}rg Siekmann and Richard Statman},
+ note = {(Superseded by 2013 article in Logica Universalis)},
+ pages = {386-406},
+ publisher = {College Publications},
+ series = {Studies in Logic, Mathematical Logic and Foundations},
+ title = {Exploring Properties of Normal Multimodal Logics in
+ Simple Type Theory with {LEO-II}},
+ year = {2008},
+ isbn = {978-1-904987-70-3},
+ OPTurl = {http://christoph-benzmueller.de/papers/B9.pdf},
+}
+
+@article{J21,
+ author = {Christoph Benzm{\"u}ller and Lawrence Paulson},
+ journal = {The Logic Journal of the IGPL},
+ number = {6},
+ pages = {881-892},
+ title = {Multimodal and Intuitionistic Logics in Simple Type
+ Theory},
+ volume = {18},
+ year = {2010},
+ doi = {10.1093/jigpal/jzp080},
+ OPTurl = {http://christoph-benzmueller.de/papers/J21.pdf},
+}
+
+@unpublished{zalta16:_princ_logic_metap,
+ author = {Edward N. Zalta},
+ note = {Preprint available at
+ \url{https://mally.stanford.edu/principia.pdf}},
+ title = {{Principia Logico-Metaphysica (Draft/Excerpt)}},
+ year = {2018},
+}
+
+@book{stalnaker12:_mere_possin,
+ author = {Robert C. Stalnaker},
+ publisher = {Princeton University Press},
+ title = {Mere Possibilities: Metaphysical Foundations of Modal
+ Semantics},
+ year = {2012},
+}
+
+@book{williamson13,
+ author = {T. Williamson},
+ publisher = {Oxford:OUP},
+ title = {Modal Logic as Metaphysics},
+ year = {2013},
+}
+
+@article{FitelsonZalta,
+ author = {Branden Fitelson and Edward N. Zalta},
+ journal = {Journal Philosophical Logic},
+ number = {2},
+ pages = {227--247},
+ title = {Steps Toward a Computational Metaphysics},
+ volume = {36},
+ year = {2007},
+ doi = {10.1007/s10992-006-9038-7},
+}
+
+@article{OppenheimerZalta2011,
+ author = {P. E. Oppenheimer and Edward N. Zalta},
+ journal = {Australasian Journal of Philosophy},
+ number = {2},
+ pages = {333-349},
+ title = {A Computationally-Discovered Simplification of the
+ Ontological Argument},
+ volume = {89},
+ year = {2011},
+}
+
+@inproceedings{AlamaZalta2015,
+ author = {Jesse Alama and Oppenheimer, Paul E. and
+ Zalta, Edward N.},
+ booktitle = {Automated Deduction -- {CADE-25}},
+ OPTeditor = {A.~P.~Felty and A.~Middeldorp},
+ pages = {73--97},
+ publisher = {Springer},
+ series = {LNCS},
+ title = {Automating Leibniz's Theory of Concepts},
+ volume = {9195},
+ year = {2015},
+}
+
+
+@inproceedings{C40,
+ author = {Christoph Benzm{\"u}ller and
+ Woltzenlogel Paleo, Bruno},
+ booktitle = {ECAI 2014},
+ OPTeditor = {T. Schaub and et al.},
+ pages = {93--98},
+ publisher = {IOS Press},
+ series = {Frontiers in Artificial Intelligence and
+ Applications},
+ title = {Automating {G\"{o}del's} Ontological Proof of {God}'s
+ Existence with Higher-order Automated Theorem
+ Provers},
+ volume = {263},
+ year = {2014},
+ doi = {10.3233/978-1-61499-419-0-93},
+ OPTurl = {http://christoph-benzmueller.de/papers/C40.pdf},
+}
+
+@inproceedings{C55,
+ author = {Christoph Benzm{\"u}ller and
+ Woltzenlogel Paleo, Bruno},
+ booktitle = {{IJCAI} 2016},
+ editor = {S.~Kambhampati},
+ pages = {936-942},
+ publisher = {AAAI Press},
+ title = {The Inconsistency in {G{\"o}del's} Ontological
+ Argument: A Success Story for {AI} in Metaphysics},
+ volume = {1-3},
+ year = {2016},
+ isbn = {978-1-57735-770-4},
+ url = {http://www.ijcai.org/Proceedings/16/Papers/137.pdf},
+}
+
+@inproceedings{C60,
+ address = {Berlin, Germany},
+ author = {Christoph Benzm{\"u}ller and
+ Woltzenlogel Paleo, Bruno},
+ booktitle = {{KI 2016}: Advances in Artificial Intelligence,
+ Proceedings},
+ editor = {Malte Helmert and Franz Wotawa},
+ pages = {244-250},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {An Object-Logic Explanation for the Inconsistency in
+ {G\"odel's} Ontological Theory (Extended Abstract,
+ Sister Conferences)},
+ year = {2016},
+ doi = {10.1007/978-3-319-46073-4},
+ OPTurl = {http://christoph-benzmueller.de/papers/C60.pdf},
+}
+
+@inCollection{GoedelNotes,
+ author = {Kurt G\"odel},
+ OPTbooktitle = {Logic and Theism: Arguments for and Against Beliefs
+ in God},
+ editor = {Sobel, J.H.},
+ pages = {144--145},
+ OPTpublisher = {Cambridge University Press},
+ title = {{Appendix A. Notes in Kurt G\"odel's Hand}},
+ OPTchapter = {Appendix A. Notes in Kurt G\"odel's Hand},
+ year = {1970},
+ isbn = {9781139449984},
+ crossref = {sobel2004logic},
+}
+
+@inCollection{ScottNotes,
+ author = {Dana S. Scott},
+ OPTbooktitle = {Logic and Theism: Arguments for and Against Beliefs
+ in God},
+ editor = {Sobel, J.H.},
+ pages = {145-146},
+ OPTpublisher = {Cambridge U. Press},
+ title = {{Appendix B: Notes in Dana Scott's Hand}},
+ OPTchapter = {Appendix B: Notes in Dana Scott's Hand},
+ year = 1972,
+ isbn = 9781139449984,
+ crossref = {sobel2004logic},
+}
+
+@book{BC04,
+ author = {Bertot, Y. and Casteran, P.},
+ publisher = {Springer},
+ series = {Texts in Theoretical Computer Science},
+ title = {{Interactive Theorem Proving and Program Development
+ - Coq'Art: The Calculus of Inductive Constructions}},
+ year = {2004},
+}
+
+@incollection{Sobel,
+ author = {Sobel, Jordan H.},
+ booktitle = {{On Being and Saying. Essays for Richard Cartwright}},
+ editor = {Judith Jarvis Tomson},
+ pages = {241-261},
+ publisher = {{MIT Press}},
+ title = {G\"odel's Ontological Proof},
+ year = {1987},
+}
+
+@article{Anderson90,
+ author = {C. Anthony Anderson},
+ journal = {Faith and Philosophy},
+ number = {3},
+ title = {Some emendations of {G{\"o}del's} ontological proof},
+ volume = {7},
+ year = {1990},
+ pages = {291--303}
+}
+
+@incollection{AndersonGettings,
+ author = {Anderson, C. Anthony and Gettings, M.},
+ booktitle = {{G\"odel'96: Logical Foundations of Mathematics,
+ Computer Science, and Physics: Lecture Notes in Logic
+ 6}},
+ pages = {167-172},
+ publisher = {{Springer}},
+ title = {{G\"odel}'s Ontological Proof Revisited},
+ year = {1996},
+}
+
+@incollection{Hajek1,
+ author = {H\'ajek, Petr},
+ booktitle = {Logic and algebra},
+ editor = {A. Ursini and P. Agliano},
+ pages = {125–135},
+ publisher = {Dekker, New York etc.},
+ title = {Magari and others on {G\"odel’s} ontological proof},
+ year = {1996},
+}
+
+@incollection{Hajek2,
+ author = {H\'ajek, Petr},
+ booktitle = {{Kurt G{\"o}del. Wahrheit und Beweisbarkeit}},
+ editor = {Buldt et al., B.},
+ note = {ISBN 3-209-03835-X},
+ pages = {325-336},
+ publisher = {öbv \& hpt Verlagsgesellschaft mbH, Wien},
+ title = {{Der Mathematiker und die Frage der Existenz Gottes}},
+ year = {2001},
+}
+
+@article{Hajek3,
+ author = {Petr H{\'{a}}jek},
+ journal = {Studia Logica},
+ number = {2},
+ pages = {149--164},
+ title = {A New Small Emendation of {G{\"{o}}del's} Ontological
+ Proof},
+ volume = {71},
+ year = {2002},
+}
+
+@incollection{Bjordal,
+ author = {F. Bj{\o}rdal},
+ booktitle = {The Logica Yearbook 1998},
+ editor = {T. Childers},
+ publisher = {Filosofia},
+ title = {Understanding {G\"{o}del’s} Ontological Argument},
+ pages = {214-217},
+ year = {1999},
+}
+
+@article{J32,
+ author = {Benzm{\"u}ller, Christoph and Weber, Leon and
+ Woltzenlogel Paleo, Bruno},
+ journal = {Logica Universalis},
+ number = {1},
+ pages = {139-151},
+ title = {Computer-Assisted Analysis of the
+ {Anderson-H\'{a}jek} Controversy},
+ volume = {11},
+ year = {2017},
+ doi = {10.1007/s11787-017-0160-9},
+ OPTurl = {http://christoph-benzmueller.de/papers/J32.pdf},
+}
+
+
+@Article{J36,
+ Keywords = {own, Automated Reasoning, Intensional Higher-Order Modal
+ Logic, Higher Order Logic},
+ author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
+ Bruno},
+ title = {Experiments in {Computational Metaphysics}:
+ {G\"odel's} Proof of {God's} Existence},
+ journal = {Savijnanam: scientific exploration for a spiritual
+ paradigm. Journal of the Bhaktivedanta Institute},
+ year = 2017,
+ volume = 9,
+ pages = {43-57},
+ OPTurl =
+ {https://sites.google.com/binstitute.org/journal/article-3-page-43},
+ issn = {0972-6586},
+}
+
+
+@inproceedings{C50,
+ address = {Wroclaw, Poland},
+ author = {Christoph Benzm{\"u}ller},
+ booktitle = {TABLEAUX 2015},
+ editor = {Hans De Nivelle},
+ pages = {213-220},
+ publisher = {Springer},
+ series = {LNAI},
+ title = {Invited Talk: On a (Quite) Universal Theorem Proving
+ Approach and Its Application in Metaphysics},
+ volume = {9323},
+ year = {2015},
+ doi = {10.1007/978-3-319-24312-2_15},
+ OPTurl = {http://christoph-benzmueller.de/papers/C50.pdf},
+}
+
+@inproceedings{C46,
+ address = {Berlin, Germany},
+ author = {Christoph Benzm{\"u}ller and
+ Woltzenlogel Paleo, Bruno},
+ booktitle = {Reasoning Web 2015},
+ editor = {Adrian Paschke and Wolfgang Faber},
+ number = {9203},
+ pages = {32-74},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {Higher-Order Modal Logics: Automation and
+ Applications},
+ year = {2015},
+ doi = {10.1007/978-3-319-21768-0_2},
+ OPTurl = {http://christoph-benzmueller.de/papers/C46.pdf},
+}
+
+
+
+@article{J28,
+ author = {Christoph Benzm\"uller and Woltzenlogel Paleo, Bruno},
+ journal = {Archive of Formal Proofs},
+ OPTnote = {This publication is machine verified with
+ Isabelle/HOL, but comparably mildly human reviewed},
+ title = {{G{\"o}del's God in Isabelle/HOL}},
+ volume = {2013},
+ year = {2013},
+ url = {http://afp.sourceforge.net/entries/GoedelGod.shtml},
+}
+
+@inproceedings{W55,
+ address = {Sinaia, Romania},
+ author = {Christoph Benzm{\"u}ller and
+ Woltzenlogel Paleo, Bruno},
+ booktitle = {Recent Trends in Algebraic Development Techniques:
+ 22nd International Workshop, WADT 2014, Sinaia,
+ Romania, September 4-7, 2014, Revised Selected
+ Papers},
+ editor = {Codescu, Mihai and Diaconescu, Razvan and
+ Tutu, Ionut},
+ number = {9563},
+ pages = {3-6},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {On Logic Embeddings and {G\"odel's} {God}},
+ year = {2015},
+ doi = {10.1007/978-3-319-28114-8_1},
+ isbn = {978-3-319-28114-8},
+ OPTurl = {http://christoph-benzmueller.de/papers/W55.pdf},
+}
+
+@incollection{B15,
+ author = {Benzm{\"u}ller, Christoph and
+ Woltzenlogel Paleo, Bruno},
+ booktitle = {The Square of Opposition: A Cornerstone of Thought
+ (Collection of papers related to the World Congress
+ on the Square of Opposition IV, Vatican, 2014)},
+ note = {\url{http://www.springer.com/us/book/9783319450612}},
+ editor = {B\'{e}ziau, Jean-Yves and Basti, Gianfranco},
+ pages = {307-313},
+ publisher = {Springer International Publishing Switzerland},
+ series = {Studies in Universal Logic},
+ title = {The Modal Collapse as a Collapse of the Modal Square
+ of Opposition},
+ year = {2016},
+ doi = {10.1007/978-3-319-45062-9_18},
+ OPTurl = {http://christoph-benzmueller.de/papers/B15.pdf},
+}
+
+
+
+@inproceedings{C56,
+ address = {Berlin, Germany},
+ author = {Alexander Steen and Max Wisniewski and
+ Christoph Benzm{\"u}ller},
+ booktitle = {Mathematical Software -- ICMS 2016, 5th International
+ Congress, Proceedings},
+ editor = {G.-M. Greuel and T. Koch and P. Paule and A. Sommese},
+ pages = {75-81},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {Agent-Based {HOL} Reasoning},
+ volume = {9725},
+ year = {2016},
+ doi = {10.1007/978-3-319-42432-3_10},
+ isbn = {978-3-319-42431-6},
+ OPTurl = {http://christoph-benzmueller.de/papers/C56.pdf},
+}
+
+@book{fitting02:_types_tableaus_god,
+ author = {Melvin Fitting},
+ publisher = {Kluwer},
+ title = {Types, Tableaus, and {G}{\"o}del's God},
+ year = {2002},
+}
+
+@book{Principia,
+ author = {Alfred North Whitehead and Bertrand Russell},
+ publisher = {Cambridge: Cambridge University Press. Second
+ edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Abridged as
+ Principia Mathematica to *56, Cambridge: Cambridge
+ University Press, 1962.},
+ title = {Principia Mathematica, 3 vols},
+ year = {1910, 1912, 1913},
+}
+
+@book{zalta1988intensional,
+ author = {Edward N. Zalta},
+ publisher = {MIT Press},
+ series = {A Bradford book},
+ title = {Intensional Logic and the Metaphysics of
+ Intentionality},
+ year = {1988},
+ isbn = {9780262240277},
+}
+
+@article{zalta1988validity,
+ author = {Edward N. Zalta},
+ journal = {The Journal of Philosophy},
+ title = {Logical and Analytic Truths That Are Not Necessary},
+ year = {1988},
+ volume = {85},
+ number = {2},
+ pages = {57--74},
+}
+
+@book{zalta1983abstract,
+ author = {Edward N. Zalta},
+ publisher = {D. Reidel},
+ title = {Abstract Objects: An Introduction to Axiomatic
+ Metaphysics},
+ city = {Dordrecht},
+ year = {1983},
+ isbn = {9789027714749},
+ OPTurl = {https://books.google.de/books?id=voCSP6k3FCcC},
+}
+
+@article{DBLP:journals/logcom/OppenheimerZ11,
+ author = {Paul E. Oppenheimer and Edward N. Zalta},
+ journal = {Journal of Logic and Computation},
+ number = 2,
+ pages = {351--374},
+ title = {Relations Versus Functions at the Foundations of
+ Logic: Type-Theoretic Considerations},
+ volume = 21,
+ year = 2011,
+ doi = {10.1093/logcom/exq017},
+ url = {http://dx.doi.org/10.1093/logcom/exq017},
+}
+
+
+
+@article{DBLP:journals/afp/Kirchner17,
+ author = {Daniel Kirchner},
+ journal = {Archive of Formal Proofs},
+ title = {Representation and Partial Automation of the
+ Principia Logico-Metaphysica in {Isabelle/HOL}},
+ volume = {2017},
+ year = {2017},
+ url = {https://www.isa-afp.org/entries/PLM.html},
+}
+
+@techreport{R60,
+ author = {Kirchner, Daniel and Benzm{\"u}ller, Christoph and
+ Edward N. Zalta},
+ institution = {CoRR},
+ note = {Preprint of submitted article},
+ title = {{Mechanizing Principia Logico-Metaphysica in
+ Functional Type Theory}},
+ year = {2017},
+ url = {https://arxiv.org/abs/1711.06542},
+}
+
+@book{link08:_one_hundr_years_russel_parad,
+ editor = {Link, Godehard},
+ publisher = {De Gruyter},
+ title = {One Hundred Years of Russell's Paradox},
+ year = {2008},
+}
+
+@book{Frege1879,
+ author = {Gottlob Frege},
+ note = {Translated in \cite{vanHeijenoort67}},
+ publisher = {Halle},
+ title = {Begriffsschrift, eine der arithmetischen
+ nachgebildete Formelsprache des reinen Denkens},
+ year = {1879},
+}
+
+@inproceedings{Lambert60,
+ author = {Karel Lambert},
+ booktitle = {Abstracts: The International Congress for Logic,
+ Methodology and Philosophy of Science},
+ publisher = {Stanford: Stanford University Press},
+ title = {The Definition of E(xistence)! in Free Logic},
+ year = {1960},
+}
+
+@incollection{Scott67,
+ author = {Dana S. Scott},
+ booktitle = {Bertrand Russell: Philosopher of the Century},
+ editor = {R. Schoenman},
+ note = {(Reprinted with additions in: Philosophical
+ Application of Free Logic, edited by K. Lambert.
+ Oxford Universitry Press, 1991, pp. 28 - 48)},
+ pages = {181-200},
+ publisher = {George Allen \& Unwin, London},
+ title = {Existence and description in formal logic},
+ year = {1967},
+}
+
+@book{lambert02:_free_logic,
+ author = {Karel Lambert},
+ publisher = {Cambridge: Cambridge University Press},
+ title = {Free Logic: Selected Essays},
+ year = {2002},
+}
+
+@InCollection{sep-logic-free,
+ author = {Nolt, John},
+ title = {Free Logic},
+ booktitle = {The Stanford Encyclopedia of Philosophy},
+ editor = {Edward N. Zalta},
+ howpublished = {\url{https://plato.stanford.edu/archives/fall2018/entries/logic-free/}},
+ year = {2018},
+ edition = {Fall 2018},
+ publisher = {Metaphysics Research Lab, Stanford University}
+}
+
+
+@techreport{R58,
+ author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
+ institution = {CoRR},
+ title = {Axiomatizing Category Theory in Free Logic},
+ year = {2016},
+ url = {http://arxiv.org/abs/1609.01493},
+}
+
+@inproceedings{C57,
+ address = {Berlin, Germany},
+ author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
+ booktitle = {Mathematical Software -- ICMS 2016, 5th International
+ Congress, Proceedings},
+ editor = {G.-M. Greuel and T. Koch and P. Paule and A. Sommese},
+ pages = {43-50},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {Automating Free Logic in {Isabelle/HOL}},
+ volume = {9725},
+ year = {2016},
+ doi = {10.1007/978-3-319-42432-3_6},
+ isbn = {978-3-319-42431-6},
+ OPTurl = {http://christoph-benzmueller.de/papers/C57.pdf},
+}
+
+
+@article{J39,
+ author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
+ title = {Axiom Systems for Category Theory in Free Logic},
+ journal = {Archive of Formal Proofs},
+ month = may,
+ year = 2018,
+ note = {\url{http://isa-afp.org/entries/AxiomaticCategoryTheory.html},
+ Formal proof development},
+ ISSN = {2150-914x},
+}
+
+@book{FreydScedrov90,
+ author = {Peter Freyd and Andre Scedrov},
+ publisher = {North Holland},
+ title = {Categories, Allegories},
+ year = {1990},
+}
+
+@incollection{Scott79,
+ author = {Scott, Dana S.},
+ booktitle = {Applications of Sheaves: Proceedings of the Research
+ Symposium on Applications of Sheaf Theory to Logic,
+ Algebra, and Analysis, Durham, July 9--21, 1977},
+ editor = {Fourman, Michael and Mulvey, Christopher and
+ Scott, Dana},
+ pages = {660--696},
+ publisher = {Springer},
+ series = {Lecture Notes in Mathematics},
+ title = {Identity and existence in intuitionistic logic},
+ volume = {752},
+ year = {1979},
+}
+
+@article{J31,
+ author = {Christoph Benzm{\"u}ller},
+ journal = {Journal of Philosophical Logic},
+ number = {3},
+ pages = {333-353},
+ title = {Cut-Elimination for Quantified Conditional Logic},
+ volume = {46},
+ year = {2017},
+ doi = {10.1007/s10992-016-9403-0},
+ OPTurl = {http://christoph-benzmueller.de/papers/J31.pdf},
+}
+
+@incollection{Stalnaker68,
+ author = {Robert C. Stalnaker},
+ booktitle = {Studies in Logical Theory},
+ pages = {98--112},
+ publisher = {Blackwell},
+ title = {A Theory of Conditionals},
+ year = {1968},
+}
+
+@article{Chellas75,
+ author = {Chellas, B.F.},
+ journal = {Journal of Philosophical Logic},
+ number = {2},
+ pages = {133-153},
+ title = {Basic Conditional Logic},
+ volume = {4},
+ year = {1975},
+}
+
+@article{delgrande98,
+ author = {J.P. Delgrande},
+ journal = {Artificial Intelligence},
+ number = {1-2},
+ pages = {105-137},
+ title = {On First-Order Conditional Logics},
+ volume = {105},
+ year = {1998},
+}
+
+@article{delgrande87,
+ author = {J.P. Delgrande},
+ journal = {Artificial Intelligence},
+ number = {1},
+ pages = {105-130},
+ title = {A First-Order Conditional Logic for Prototypical
+ Properties},
+ volume = {33},
+ year = {1987},
+}
+
+@article{DBLP:journals/tocl/FriedmanHK00,
+ author = {N. Friedman and J.Y. Halpern and D. Koller},
+ journal = {ACM Transactions on Computational Logic},
+ number = {2},
+ pages = {175-207},
+ title = {First-order conditional logic for default reasoning
+ revisited},
+ volume = {1},
+ year = {2000},
+}
+
+@article{DBLP:journals/corr/abs-1011-3479,
+ author = {Dirk Pattinson and Lutz Schr{\"{o}}der},
+ journal = {Logical Methods in Computer Science},
+ number = {1},
+ title = {Generic Modal Cut Elimination Applied to Conditional
+ Logics},
+ volume = {7},
+ year = {2011},
+ bibOPTurl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1011-
+ 3479},
+ doi = {10.2168/LMCS-7(1:4)2011},
+}
+
+@article{DBLP:journals/apal/Rasga07,
+ author = {Jo{\~{a}}o Rasga},
+ journal = {Ann. Pure Appl. Logic},
+ number = {1-3},
+ pages = {81--99},
+ title = {Sufficient conditions for cut elimination with
+ complexity analysis},
+ volume = {149},
+ year = {2007},
+ bibOPTurl = {http://dblp.uni-trier.de/rec/bib/journals/apal/Rasga07},
+ doi = {10.1016/j.apal.2007.08.001},
+}
+
+@inproceedings{C37,
+ address = {Beijing, China},
+ author = {Christoph Benzm{\"u}ller},
+ booktitle = {23rd International Joint Conference on Artificial
+ Intelligence ({IJCAI-13})},
+ editor = {Francesca Rossi},
+ pages = {746-753},
+ publisher = {AAAI Press},
+ title = {Automating Quantified Conditional Logics in {HOL}},
+ year = {2013},
+ isbn = {978-1-57735-633-2},
+ OPTurl = {http://christoph-benzmueller.de/papers/C37.pdf},
+}
+
+@article{J18,
+ author = {Christoph Benzm{\"u}ller and Chad Brown and
+ Michael Kohlhase},
+ journal = {Logical Methods in Computer Science},
+ number = {1:6},
+ pages = {1-21},
+ title = {Cut-Simulation and Impredicativity},
+ volume = {5},
+ year = {2009},
+ doi = {10.2168/LMCS-5(1:6)2009},
+ OPTurl = {http://christoph-benzmueller.de/papers/J18.pdf},
+}
+
+@inproceedings{C58,
+ OPTaddress = {Potsdam},
+ author = {Max Wisniewski and Alexander Steen and
+ Christoph Benzm{\"u}ller},
+ booktitle = {Hochschuldidaktik der Informatik: 7. Fachtagung des
+ GI-Fachbereichs Informatik und Ausbildung/Didaktik
+ der Informatik},
+ editor = {Andreas Schwill and Ulrike Lucke},
+ pages = {81-92},
+ publisher = {Universit{\"a}tsverlag Potsdam},
+ series = {Commentarii informaticae didacticae (CID)},
+ title = {{Einsatz von Theorembeweisern in der Lehre}},
+ year = {2016},
+ isbn = {978-3-86956-376-3},
+ issn = {1868-0844},
+ OPTurl = {https://publishup.uni-potsdam.de/opus4-ubp/frontdoor/index/
+ index/docId/9485},
+}
+
+@unpublished{R57,
+ author = {Christoph Benzm{\"u}ller and Max Wisniewski and
+ Alexander Steen},
+ note = {This lecture course proposal received the 2015
+ central teaching award of FU Berlin},
+ title = {{Computational Metaphysics}},
+ year = {2015},
+ url = {http://christoph-benzmueller.de/papers/R57.pdf},
+}
+
+@incollection{B16,
+ author = {Bentert, Matthias and Benzm{\"u}ller, Christoph and
+ Streit, David and Woltzenlogel Paleo, Bruno},
+ booktitle = {Death and Anti-Death, Volume 14: Four Decades after
+ Michael Polanyi, Three Centuries after G.W. Leibniz},
+ editor = {Tandy, Charles},
+ note = {Preprint:
+ \url{https://www.researchgate.net/publication/311456135}},
+ publisher = {Ria University Press},
+ title = {Analysis of an Ontological Proof Proposed by
+ {Leibniz}},
+ year = {2016},
+ isbn = {978-1934297254},
+ OPTurl = {https://philpapers.org/rec/TANDAA-10},
+}
+
+@inproceedings{C63,
+ author = {David Fuenmayor and Christoph Benzm{\"u}ller and
+ Alexander Steen and Max Wisniewski},
+ booktitle = {Handbook of the 2nd World Congress on Logic and
+ Religion, Warsaw, Poland},
+ editor = {Stanislaw Krajewski and Piotr Balcerowicz},
+ pages = {3},
+ title = {The Virtues of Automated Theorem Proving in
+ Metaphysics --- A Case Study: {E. J. Lowe's} Modal
+ Ontological Argument},
+ year = {2017},
+ OPTurl = {http://christoph-benzmueller.de/papers/C63.pdf},
+}
+
+@inproceedings{C65,
+ author = {David Fuenmayor and Christoph Benzm{\"u}ller},
+ booktitle = {KI 2017: Advances in Artificial Intelligence},
+ pages = {114-127},
+ publisher = {Springer},
+ series = {LNAI},
+ title = {Automating Emendations of the Ontological Argument in
+ Intensional Higher-Order Modal Logic},
+ volume = {10505},
+ year = {2017},
+ doi = {10.1007/978-3-319-67190-1_9},
+ isbn = {978-3-319-67189-5},
+ OPTurl = {http://christoph-benzmueller.de/papers/C65.pdf},
+}
+
+
+@article{J37,
+ author = {David Fuenmayor and Christoph Benzm\"uller},
+ journal = {Archive of Formal Proofs},
+ OPTnote = {This publication is machine verified with
+ Isabelle/HOL, but comparably mildly human reviewed},
+ title = {{Computer-assisted Reconstruction and Assessment of
+ E. J. Lowe's Modal Ontological Argument}},
+volume = {2017},
+ year = {2017},
+ url = {https://www.isa-afp.org/entries/Lowe_Ontological_Argument.html},
+}
+
+
+
+@MastersThesis{BScMakarenko,
+ author = {Irina Makarenko},
+ school = {Department of Mathematics and Computer Science, Freie
+ Universit{\"a}t Berlin},
+ type = {Bachelor's Thesis},
+ title = {Automatisierung von freier Logik in Logik h{\"o}herer
+ Stufe},
+ year = {2016},
+}
+
+@MastersThesis{BScFuenmayor,
+ author = {David Fuenmayor},
+ school = {Department of Philosophy, Freie Universit{\"a}t
+ Berlin},
+ type = {Bachelor's Thesis},
+ title = {Computational Hermeneutics: Using Computers to
+ Understand Philosophical Arguments},
+ year = {2017},
+}
+
+@MastersThesis{BScGleissner,
+ author = {Tobias Gleissner},
+ school = {Department of Mathematics and Computer Science, Freie
+ Universit{\"a}t Berlin},
+ type = {Bachelor's Thesis},
+ title = {Converting Higher-Order Modal Logic Problems into
+ Classical Higher-Order Logic},
+ year = {2017},
+}
+
+@MastersThesis{MScSchuetz,
+ author = {Fabian Sch{\"u}tz},
+ school = {Department of Mathematics and Computer Science, Freie
+ Universit{\"a}t Berlin},
+ type = {Master's Thesis},
+ title = {{Wahrhaftiger Toren Zorn - Repr{\"a}sentation und
+ Interpretation von Argumenten}},
+ year = {2017},
+}
+
+@article{J33,
+ author = {Steen, Alexander and Benzm{\"u}ller, Christoph},
+ journal = {Logic and Logical Philosophy},
+ pages = {535-554},
+ title = {Sweet {SIXTEEN}: Automation via Embedding into
+ Classical Higher-Order Logic},
+ volume = {25},
+ year = {2016},
+ doi = {10.12775/LLP.2016.021},
+ issn = {1425-3305},
+ OPTurl = {http://christoph-benzmueller.de/papers/J33.pdf},
+}
+
+@inproceedings{wisniewski14:_embed_quant_higher_order_nomin,
+ author = {Max Wisniewski and Alexander Steen},
+ booktitle = {1st International Workshop on Automated Reasoning in
+ Quantified Non-Classical Logics (ARQNL 2014), Vienna,
+ Austria, Proceedings},
+ editor = {Christoph Benzm\"uller and Jens Otten},
+ pages = {59-64},
+ publisher = {EasyChair Publications},
+ series = {EasyChair Proceedings in Computing},
+ title = {Embedding of Quantified Higher-Order Nominal Modal
+ Logic into Classical Higher-Order Logic},
+ volume = {33},
+ year = {2014},
+}
+
+@MastersThesis{MScClaus,
+ author = {Maximilian Claus},
+ school = {Department of Mathematics and Computer Science, Freie
+ Universit{\"a}t Berlin},
+ type = {Master's Thesis},
+ title = {Software Model Checking With Higher-Order Automated
+ Theorem Provers: A Logic Embedding Approach},
+ year = {2015},
+}
+
+@book{boolos93:_logic_provab,
+ author = {George Boolos},
+ publisher = {Cambridge University Press},
+ title = {The Logic of Provability},
+ year = {1993},
+}
+
+@article{bostrom03:_are_we_livin_comput_simul,
+ author = {Nick Bostrom},
+ journal = {The Philosophical Quarterly},
+ number = {211},
+ pages = {243–255},
+ title = {Are We Living in a Computer Simulation?},
+ volume = {53},
+ year = {2003},
+ doi = {10.1111/1467-9213.00309},
+}
+
+@techreport{R59,
+ author = {Christoph Benzm{\"u}ller},
+ institution = {CoRR},
+ title = {Universal Reasoning, Rational Argumentation and
+ Human-Machine Interaction},
+ year = {2017},
+ url = {http://arxiv.org/abs/1703.09620},
+}
+
+@book{gabbay13:_handb_deont_logic_normat_system,
+ editor = {Dov Gabbay and John Horty and Xavier Parent and
+ van der Meyden, Ron and van der Torre, Leendert},
+ publisher = {College Publications},
+ title = {Handbook of Deontic Logic and Normative Systems},
+ year = {2013},
+}
+
+@article{DBLP:journals/jphil/MakinsonT00,
+ author = {David Makinson and Leendert W. N. van der Torre},
+ journal = {Journal of Philosophical Logic},
+ number = {4},
+ pages = {383--408},
+ title = {Input/Output Logics},
+ volume = {29},
+ year = {2000},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/jphil/
+ MakinsonT00},
+ doi = {10.1023/A:1004748624537},
+ OPTurl = {http://dx.doi.org/10.1023/A:1004748624537},
+}
+
+@article{DBLP:journals/logcom/CarmoJ13,
+ author = {Jos{\'{e}} Carmo and Andrew J. I. Jones},
+ journal = {Journal of Logic and Computation},
+ number = {3},
+ pages = {585--626},
+ title = {Completeness and decidability results for a logic of
+ contrary-to-duty conditionals},
+ volume = {23},
+ year = {2013},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/logcom/CarmoJ13},
+ doi = {10.1093/logcom/exs009},
+ OPTurl = {http://dx.doi.org/10.1093/logcom/exs009},
+}
+
+@inproceedings{C69,
+ author = {Benzm{\"u}ller, Christoph and Parent, Xavier and
+ van der Torre, Leendert},
+ booktitle = {14th Conference on Computability in Europe, CiE 2018,
+ Kiel, Germany, July 30-August, 2018, Proceedings},
+ editor = {Manea, Florin and Miller, Russell G. and
+ Nowotka, Dirk},
+ pages = {60-69},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {A Deontic Logic Reasoning Infrastructure},
+ volume = {10936},
+ year = {2018},
+ doi = {10.1007/978-3-319-94418-0_6},
+ isbn = {978-3-319-67189-5},
+ OPTurl = {http://christoph-benzmueller.de/papers/C69.pdf},
+}
+
+@techreport{R66,
+ author = {Benzm{\"u}ller, Christoph and Parent, Xavier},
+ institution = {CoRR},
+ title = {First Experiments with a Flexible Infrastructure for
+ Normative Reasoning},
+ year = {2018},
+ url = {http://arxiv.org/abs/1804.02929},
+}
+
+@techreport{R65,
+ author = {Benzm{\"u}ller, Christoph and Parent, Xavier},
+ institution = {CoRR},
+
+ title = {{I/O} Logic in {HOL} --- First Steps},
+ year = {2018},
+ url = {http://arxiv.org/abs/1803.09681},
+}
+
+@techreport{R63,
+ author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
+ Parent, Xavier},
+ institution = {CoRR},
+ title = {Faithful Semantical Embedding of a Dyadic Deontic
+ Logic in {HOL}},
+ year = {2018},
+ url = {https://arxiv.org/abs/1802.08454},
+}
+
+@inproceedings{C62,
+ address = {Maun, Botswana},
+ author = {Tobias Glei{\ss}ner and Alexander Steen and
+ Christoph Benzm{\"u}ller},
+ booktitle = {LPAR-21. 21st International Conference on Logic for
+ Programming, Artificial Intelligence and Reasoning},
+ editor = {Thomas Eiter and David Sands},
+ pages = {14-30},
+ publisher = {EasyChair},
+ series = {EPiC Series in Computing},
+ title = {Theorem Provers for Every Normal Modal Logic},
+ volume = {46},
+ year = {2017},
+ doi = {10.29007/jsb9},
+ issn = {2398-7340},
+ OPTurl = {https://easychair.org/publications/paper/340346},
+}
+
+@inproceedings{W56,
+ author = {Max Wisniewski and Alexander Steen and
+ Christoph Benzm\"uller},
+ booktitle = {ARQNL 2016. Automated Reasoning in Quantified
+ Non-Classical Logics},
+ editor = {Christoph Benzm{\"u}ller and Jens Otten},
+ pages = {51-65},
+ publisher = {CEUR Workshop Proceedings, http://ceur-ws.org},
+ title = {{TPTP} and Beyond: Representation of Quantified
+ Non-Classical Logics},
+ volume = {1770},
+ year = {2016},
+ OPTurl = {http://ceur-ws.org/Vol-1770/},
+}
+
+@inproceedings{C38,
+ address = {Stellenbosch, South Africa},
+ author = {Christoph Benzm{\"u}ller and Thomas Raths},
+ booktitle = {Proceedings of the 19th International Conference on
+ Logic for Programming, Artificial Intelligence and
+ Reasoning (LPAR)},
+ editor = {Kenneth L. McMillan and Aart Middeldorp and
+ Andrei Voronkov},
+ pages = {127-136},
+ publisher = {Springer},
+ series = {Lecture Notes in Computer Science},
+ title = {{HOL} based First-order Modal Logic Provers},
+ volume = {8312},
+ year = {2013},
+ doi = {10.1007/978-3-642-45221-5_9},
+ isbn = {978-3-642-45220-8},
+ OPTurl = {http://christoph-benzmueller.de/papers/C38.pdf},
+}
+
+@inproceedings{C34,
+ address = {Montpellier, France},
+ author = {Christoph Benzm{\"u}ller and Jens Otten and
+ Thomas Raths},
+ booktitle = {ECAI 2012},
+ editor = {Luc De Raedt and Christian Bessiere and Didier Dubois and
+ Patrick Doherty and Paolo Frasconi and Fredrik Heintz and
+ Peter Lucas},
+ pages = {163-168},
+ publisher = {IOS Press},
+ series = {Frontiers in Artificial Intelligence and
+ Applications},
+ title = {Implementing and Evaluating Provers for First-order
+ Modal Logics},
+ volume = {242},
+ year = {2012},
+ doi = {10.3233/978-1-61499-098-7-163},
+ isbn = {978-1-61499-097-0},
+ OPTurl = {http://christoph-benzmueller.de/papers/C34.pdf},
+}
+
+@inproceedings{C64,
+ address = {Maun, Botswana},
+ author = {Christoph Benzm{\"u}ller and Alexander Steen and
+ Max Wisniewski},
+ booktitle = {IWIL@LPAR 2017 Workshop and {LPAR-21} Short
+ Presentations, Maun, Botswana, May 7-12, 2017},
+ editor = {Thomas Eiter and David Sands and Geoff Sutcliffe and
+ Andrei Voronkov},
+ pages = {11-61},
+ publisher = {EasyChair},
+ series = {Kalpa Publications in Computing},
+ title = {{Leo-III} Version 1.1 (System description)},
+ volume = {1},
+ year = {2017},
+ OPTurl = {http://www.easychair.org/publications/paper/342979},
+}
+
+@inproceedings{W57,
+ address = {Maun, Botswana},
+ author = {Alexander Steen and Max Wisniewski and
+ Christoph Benzm{\"u}ller},
+ booktitle = {IWIL@LPAR 2017 Workshop and {LPAR-21} Short
+ Presentations, Maun, Botswana, May 7-12, 2017},
+ editor = {Thomas Eiter and David Sands and Geoff Sutcliffe and
+ Andrei Voronkov},
+ pages = {100-112},
+ publisher = {EasyChair},
+ series = {Kalpa Publications in Computing},
+ title = {Going Polymorphic - {TH1} Reasoning for {Leo-III}},
+ volume = {1},
+ year = {2017},
+ OPTurl = {http://www.easychair.org/publications/paper/346851},
+}
+
+@book{vanHeijenoort67,
+ address = {Cambridge, MA},
+ author = {Jean van Heijenoort},
+ edition = {3rd printing, 1997},
+ publisher = {Harvard Univ. Press},
+ series = {Source books in the history of the sciences series},
+ title = {From {F}rege to {G}{\"o}del: {A} Source Book in
+ Mathematics, 1879-1931},
+ year = {1967},
+ isbn = {0-674-32450-1},
+}
+
+@article{J38,
+ Author = {David Fuenmayor and Christoph Benzm\"uller},
+ Journal = {Journal of Applied Logic - IfCoLoG Journal of Logics and their Applications (special issue on Formal Approaches to the Ontological Argument)},
+ Editors = {Silvestre, Ricardo and B\'{e}ziau, Jean-Yves},
+ Keywords = {own, Automated Reasoning, Interactive Proof, Ontology
+ Reasoning, Higher Order Logic, Computational
+ Metaphysics},
+ Title = {A Case Study On Computational Hermeneutics: {E.J. Lowe's Modal} Ontological Argument},
+ Year = 2018,
+ Url = {http://christoph-benzmueller.de/papers/J38.pdf},
+ Note = {Accepted for publication; to be published also as chapter in the book 'Beyond Faith and Rationality: Essays on Logic, Religion and Philosophy' printed in the Springer book series 'Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures'},
+}
+
+@Article{MacLane48,
+ author = {Saunders MacLane},
+ title = {Groups, Categories and Duality},
+ journal = {Proceedings of the National Academy of Sciences},
+ year = 1948,
+ volume = 34,
+ number = 6,
+ pages = {263-267}}
+
+@article{J42,
+ author = {David Fuenmayor and Christoph Benzmüller},
+ title = {{Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL}},
+ journal = {Archive of Formal Proofs},
+ month = oct,
+ year = 2018,
+ note = {\url{http://isa-afp.org/entries/GewirthPGCProof.html},
+ Formal proof development},
+ ISSN = {2150-914x},
+}
+
+@Book{Isabelle,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
+ publisher = {Springer},
+ series = {LNCS},
+ volume = 2283,
+ year = 2002}
+
+@article{J50,
+ Author = {Kirchner, Daniel and Benzm{\"u}ller, Christoph and
+ Zalta, Edward N.},
+ Keywords = {own, Higher Order Logic, Higher Order Modal Logic,
+ Universal Reasoning, Computational Metaphysics},
+ Title = {Mechanizing Principia Logico-Metaphysica in
+ Functional Type Theory},
+ Journal = {Review of Symbolic Logic},
+ Volume = {13},
+ Number = {1},
+ Publisher = {Cambridge University Press},
+ Doi = {10.1017/S1755020319000297},
+ pages = {206-218},
+ Addendum = {Preprint: \url{https://www.researchgate.net/publication/321160582}},
+ Year = 2020,
+}
+
+@article{Thesis,
+ author = {Daniel Kirchner},
+ title = {{Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL}},
+ journal = {Archive of Formal Proofs},
+ month = sep,
+ year = 2017,
+ note = {\url{http://isa-afp.org/entries/PLM.html},
+ Formal proof development},
+ ISSN = {2150-914x},
+}
+@Article{rtt,
+ author = {Oppenheimer, Paul E. and Zalta, Edward N.},
+ title = {{Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations}},
+ journal = {Journal of Logic and Computation},
+ year = 2011,
+ volume = 21,
+ number = 2,
+ pages = {351--374}
+}
+@article{Andrews89,
+ author = {Peter B. Andrews},
+ title = {On Connections and Higher-Order Logic},
+ journal = {Journal of Automated Reasoning},
+ volume = {5},
+ number = {3},
+ pages = {257--291},
+ year = {1989},
+ url = {https://doi.org/10.1007/BF00248320},
+ doi = {10.1007/BF00248320},
+ timestamp = {Sat, 20 May 2017 00:22:32 +0200},
+ biburl = {https://dblp.org/rec/bib/journals/jar/Andrews89},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+
+
+
+@book{BurrisSankappanavar1981,
+ author = {Burris, S. and Sankap\-panavar, H.P.},
+ owner = 23,
+ publisher = {Springer},
+ title = {A Course in Universal Algebra},
+ url = {http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html},
+ year = 1981
+}
+
+@article{Kanckos2017VariantsOG,
+ title={Variants of {G{\"o}del}’s Ontological Proof in a Natural Deduction Calculus},
+ author={Annika Kanckos and Woltzenlogel Paleo, Bruno},
+ journal={Studia Logica},
+ year={2017},
+ volume={105},
+ pages={553-586}
+}
+
+
+@Article{Rushby,
+ author = {John Rushby},
+ title = {A Mechanically Assisted Examination of Begging the Question in {Anselm's} Ontological Argument},
+ journal = {J. Applied Logics},
+ year = 2018,
+ volume = 5,
+ number = 7,
+ pages = {1473--1496}}
+
+
+@Article{Blumson,
+ author = {Ben Blumson},
+ title = {{Anselm's God in Isabelle/HOL}},
+ journal = {Archive of Formal Proofs},
+ year = 2017}
+
+
+@article{KanckosLethen19,
+title = "The Development of {G{\"o}del}'s ontological Proof",
+keywords = "611 Philosophy",
+author = "Annika Kanckos and Tim Lethen",
+year = "2019",
+month = "11",
+day = "15",
+doi = "10.1017/S1755020319000479",
+language = "English",
+OPTpages = "1 -- 19",
+journal = "The Review of Symbolic Logic",
+issn = "1755-0203",
+publisher = "Cambridge University Press",
+}
+
+
+@InProceedings{C78,
+ Keywords = {own, Automated Reasoning, Free Logic, Higher Order
+ Logic, Category Theory, Algebraic Structures, Modeloids},
+ Author = {Lucca Tiemens and Dana S. Scott and Christoph Benzm\"uller and Miroslav Benda},
+ title = {Computer-supported Exploration of a Categorical Axiomatization of Modeloids},
+ booktitle = {Relational and Algebraic Methods in Computer Science -- 18th International Conference, RAMiCS 2020},
+ editors = {Uli Fahrenberg and Peter Jipsen and Michael Winter},
+ year = 2020,
+ series = {LNCS},
+ url = {https://www.springerprofessional.de/computer-supported-exploration-of-a-categorical-axiomatization-o/17853766},
+ publisher = {Springer},
+ volume = 12062,
+ pages = {302--317},
+ doi = {10.1007/978-3-030-43520-2_19},
+ addendum = {Preprint (with proofs): \url{https://www.researchgate.net/publication/336838722}},
+}
+
+
+@article{J40,
+ author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
+ Keywords = {own, Automated Reasoning, Free Logic, Higher Order
+ Logic, Category Theory},
+ title = {Automating Free Logic in {HOL}, with an Experimental
+ Application in Category Theory},
+ volume = 64,
+ number = 1,
+ pages = {53--72},
+ year = 2020,
+ url = {http://doi.org/10.13140/RG.2.2.11432.83202},
+ journal = {Journal of Automated Reasoning},
+ publisher = {Springer Netherlands},
+ doi = {10.1007/s10817-018-09507-7},
+ Addendum = {Preprint:
+ \url{http://doi.org/10.13140/RG.2.2.11432.83202}},
+}
+
+
+@book{sobel2004logic,
+ author = {Sobel, Jordan H.},
+ booktitle = {Logic and Theism: Arguments for and Against Beliefs
+ in {God}},
+ OPTeditor = {Sobel, J.H.},
+ publisher = {Cambridge University Press},
+ title = {Logic and Theism: Arguments for and Against Beliefs
+ in God},
+ year = {2004},
+ isbn = {9781139449984},
+}
\ No newline at end of file