@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): <a href="http://dx.doi.org/10.13140/RG.2.2.31921.84323">10.13140/RG.2.2.31921.84323</a>},  
  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 =	 {<a href="http://christoph-benzmueller.de/papers/2015-PxTP.pdf">slides</a>},
  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},
}