@String{lncs =   "LNCS"}

@String{jar =    "J. Autom. Reasoning"}

@String{cade99 = "16th Conf.\ on Automated Deduction (CADE)"}

@String{ijcar08 = "Fourth International Joint Conference on Automated
                 Reasoning"}

@String{jlc =    "J. of Logic and Computation"}

@String{lics92 = "7th Symp.\ on Logic in Computer Science"}

@String{lnai =   "Lecture Notes in Artificial Intelligence"}

@String{lmcs =   "Logical Methods in Computer Science"}

@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",
  number =       2283,
  year =         2002,
}

@book{Williamson-MLAM,
	title = {Modal Logic as Metaphysics},
	year = {2013},
	author = {Timothy Williamson},
	publisher = {Oxford University Press}
}

@book{moreland2013,
 author = {Moreland, James},
 title = {Debating Christian theism},
 publisher = {Oxford University Press},
 year = {2013},
 address = {Oxford New York},
 isbn = {9780199981434}
 }

@article{J23,
  keywords =	 {Higher Order Logic, Semantic Embedding, Modal
                  Logics, Henkin Semantics},
  author =	 {C. Benzm{\"u}ller and L.C. Paulson},
  title =	 {Quantified Multimodal Logics in Simple Type Theory},
  journal =	 {Logica Universalis (Special Issue on Multimodal
                  Logics)},
  year =	 2013,
  volume =	 7,
  number =	 1,
  pages =	 {7-20},
  doi =		 {10.1007/s11787-012-0052-y},
  url =		 {http://christoph-benzmueller.de/papers/J23.pdf},
}

@article{J32,
  Author =	 {Benzm{\"u}ller, Christoph and Weber, Leon and
                  Woltzenlogel Paleo, Bruno},
  Journal =	 {Logica Universalis},
  Keywords =	 {own, Automated Reasoning, Interactive Proof, Semantic
                  Embedding, Higher Order Logic, Higher Order Modal
                  Logic, Computational Metaphysics, DFG-2501-Selected},
  Volume =	 11,
  Number =	 1,
  Pages =	 {139-151},
  Doi =		 {10.1007/s11787-017-0160-9},
  url =		 {http://christoph-benzmueller.de/papers/J32.pdf},
  title =	 {Computer-Assisted Analysis of the
                  {Anderson-H\'{a}jek} Controversy},
  Year =	 2017
}

@article{J35,
  Author =	 {David Fuenmayor and Christoph Benzm\"uller},
  Journal =	 {Archive of Formal Proofs},
  Keywords =	 {own, Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, Higher Order Logic, Computational
                  Metaphysics},
  Note =	 {This publication is formally verified with Isabelle/HOL},
  Title =	 {{Types, Tableaus and G{\"o}del's God in
                  Isabelle/HOL}},
  Url =
                  {https://isa-afp.org/entries/Types_Tableaus_and_Goedels_God.shtml},
  Year =	 2017,
}

@inproceedings{C47,
	Address = {Berlin, Germany},
	Author = {Christoph Benzm{\"u}ller and Maximilian Claus and Nik Sultana},
	Booktitle = {PxTP 2015. EPTCS},
	Comment = {<a href="http://christoph-benzmueller.de/papers/2015-PxTP.pdf" target="_blank">slides</a>},
	Doi = {10.4204/EPTCS.186.5},
	Editor = {Cezary Kaliszyk and Andrei Paskevich},
	Issn = {2075-2180},
	Keywords = {Automated Reasoning, Interactive Proof, Ontology Reasoning, LEO Prover, Higher Order Logic},
	Pages = {27-41},
	Title = {Systematic Verification of the Modal Logic Cube in {Isabelle/HOL}},
	Url = {http://christoph-benzmueller.de/papers/C47.pdf},
	Volume = {186},
	Year = 2015,
}

@InProceedings{C55,
  keywords =	 {Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, LEO Prover, Higher Order Logic,  Computational Metaphysics},
  OPTeditor =	 {},
  author =	 {Christoph Benzm{\"u}ller and Woltzenlogel
                  Paleo, Bruno},
  title =	 {The Inconsistency in {G{\"o}del’s} Ontological Argument: A Success Story for {AI} in Metaphysics},
  OPTpages =	 {},
  booktitle =	 {IJCAI 2016},
  OPTdoi =		 {},
  OPTseries =	 {},
  OPTvolume =	 263,
  OPTpublisher =	 {IOS Press},
  year =	 2016,
  OPTcomment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2014-ECAI.pdf
                  " target="_blank">slides</a>},
  url =		 {http://christoph-benzmueller.de/papers/C55.pdf},
}

@inCollection{sep-dependence-ontological,
	author       =	{Lowe, E. Jonathan},
	title        =	{Ontological Dependence},
	booktitle    =	{The Stanford Encyclopedia of Philosophy},
	editor       =	{Edward N. Zalta},
	howpublished =	{\url{https://plato.stanford.edu/archives/spr2010/entries/dependence-ontological/}},
	year         =	{2010},
	edition      =	{Spring 2010},
	publisher    =	{Metaphysics Research Lab, Stanford University}
}

@inproceedings{Nitpick,
  author =	 {J.C. Blanchette and T. Nipkow},
  title =	 {Nitpick: A Counterexample Generator for Higher-Order
                  Logic Based on a Relational Model Finder},
  pages =	 {131-146},
  ee =		 {https://doi.org/10.1007/978-3-642-14052-5_11},
  booktitle =	 {Proc. of ITP 2010},
  publisher =	 {Springer},
  series =	 {LNCS},
  volume =	 6172,
  year =	 2010,
  isbn =	 {978-3-642-14051-8},
  ee =		 {https://doi.org/10.1007/978-3-642-14052-5},
  bibsource =	 {DBLP, http://dblp.uni-trier.de}
}

@article{Sledgehammer,
  year =	 2013,
  issn =	 {0168-7433},
  journal =	 {Journal of Automated Reasoning},
  volume =	 51,
  number =	 1,
  doi =		 {10.1007/s10817-013-9278-5},
  title =	 {Extending {Sledgehammer} with {SMT} Solvers},
  url =		 {https://doi.org/10.1007/s10817-013-9278-5},
  publisher =	 {Springer},
  keywords =	 {SMT solvers; Automatic theorem provers; Interactive
                  theorem provers},
  author =	 {Blanchette, J.C. and B\"ohme, S. and Paulson, L.C.},
  pages =	 {109-128},
  language =	 {English}
}
