@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"}


	 Cambridge, MA: The MIT Press/Bradford Books, 1988.

@article{Hajek2002,
  author    = {P. H{\'{a}}jek},
  title     = {A New Small Emendation of {G\"{o}del's} Ontological Proof},
  journal   = {Studia Logica},
  year      = {2002},
  volume    = {71},
  number    = {2},
  pages     = {149--164},
  OPTurl    = {https://doi.org/10.1023/A:1016583920890},
  doi       = {10.1023/A:1016583920890},
  timestamp = {Fri, 24 Oct 2014 22:19:43 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/sLogica/Hajek02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@InCollection{bjordal99,
  author    = {F. Bj{\o}rdal},
  title     = {Understanding {G\"{o}del's} Ontological Argument},
  booktitle = {The Logica Yearbook 1998},
  publisher = {Filosofia},
  year 	    = 1999,
  editor    = {T. Childers}
}

@article{FitelsonZ07,
  author    = {Branden Fitelson and
               Edward N. Zalta},
  title     = {Steps Toward a Computational Metaphysics},
  journal   = {J. Philosophical Logic},
  volume    = {36},
  number    = {2},
  pages     = {227--247},
  year      = {2007},
  url       = {https://doi.org/10.1007/s10992-006-9038-7},
  doi       = {10.1007/s10992-006-9038-7},
  timestamp = {Thu, 10 May 2012 13:14:10 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jphil/FitelsonZ07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{Zalta15,
  author    = {Jesse Alama and 
               Paul E. Oppenheimer and 
               Edward N. Zalta},
  title     = {Automating Leibniz's Theory of Concepts},
  booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  pages     = {73--97},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6_4},
  doi       = {10.1007/978-3-319-21401-6_4},
  editor    = {Amy P. Felty and
               Aart Middeldorp},
  series    = {LNCS},
  volume    = {9195},
  publisher = {Springer},
}

@Book{Zalta88,
  author = 	 {Zalta, Edward N.},
  title = 	 {Intensional Logic and the Metaphysics of Intentionality},
  publisher = 	 {Cambridge, MA: The MIT Press/Bradford Books},
  year = 	 1988}

@Article{zalta11:_relat_versus_funct_found_logic,
  author = 	 {Paul E.~Oppenheimer and Edward N.~Zalta},
  title = 	 {Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations},
  journal = 	 {Journal of Logic and Computation},
  year = 	 2011,
  number = 	 21,
  pages = 	 {351--374}}


@Unpublished{zalta:_princ_metap,
  author = 	 {Zalta, Edward N.},
  title = 	 {{Principia Metaphysica} (version of July 10, 2016)},
  note = 	 {Available at \texttt{http://mally.stanford.edu/principia.pdf}}}



@Book{zalta83:_abstr_objec,
  author = 	 {Zalta, Edward N.},
  title = 	 {Abstract Objects: An Introduction to Axiomatic Metaphysics},
  publisher = 	 {Dordrecht: D. Reidel},
  year = 	 1983}


@inCollection{B12,
  keywords =	 {Modal Logics, Semantic Embedding, Higher Order
                  Logic, Automated Reasoning, LEO Prover},
  author =	 {C. Benzm\"uller},
  editor =	 {S. Siegler and N. Wasser},
  booktitle =	 {Verification, Induction, Termination Analysis -
                  Festschrift for Christoph Walther on the Occasion of
                  His 60th Birthday},
  title =	 {Verifying the Modal Logic Cube is an Easy Task (for
                  Higher-Order Automated Reasoners)},
  series =	 {LNCS},
  volume =	 6463,
  publisher =	 {Springer},
  year =	 2010,
  pages =	 {117-128},
  doi =		 {10.1007/978-3-642-17172-7\_7},
  url =		 {http://christoph-benzmueller.de/papers/B12.pdf},
}

@article{GoedelGod-AFP,
  author =	 {C. Benzm\"uller and B. Woltzenlogel Paleo},
  title =	 {G\"odel's God in Isabelle/HOL},
  journal =	 {Archive of Formal Proofs},
  month =	 nov,
  year =	 2013,
  note =	 {\url{https://isa-afp.org/entries/GoedelGod.shtml},
                  Formal proof development},
  ISSN =	 {2150-914x},
}

@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{Rabe,
  author =	 {Rabe, F. and Pudlak, P. and Sutcliffe, G. and Shen,
                  W.},
  title =	 {Solving the \$ 100 modal logic challenge},
  journal =	 {Journal of Applied Logic},
  year =	 2009,
  volume =	 7,
  pages =	 {113-130},
  doi =		 {10.1016/j.jal.2007.07.007}
}

@InProceedings{C25,
  keywords =	 {Higher Order Logic, Henkin Semantics, Automated
                  Reasoning},
  author =	 {C. Benzm{\"u}ller and F. Rabe and G.  Sutcliffe},
  title =	 {{THF0} -- The Core of the {TPTP} Language for
                  Classical Higher-Order Logic},
  editor =	 {A. Armando and P. Baumgartner and G.  Dowek},
  booktitle =	 {Automated Reasoning, 4th International Joint
                  Conference, IJCAR 2008, Sydney, Australia, August
                  12-15, 2008, Proceedings},
  url =		 {http://christoph-benzmueller.de/papers/C25.pdf},
  publisher =	 {Springer},
  pages =	 {491-506},
  series =	 {LNCS},
  year =	 2008,
  doi =		 {10.1007/978-3-540-71070-7\_41},
  volume =	 5195
}

@inproceedings{BlanchetteN-ITP10,
  author =	 {J.C. Blanchette and T. Nipkow},
  title =	 {Nitpick: A counterexample generator for higher-order
                  logic based on a relational model finder},
  booktitle =	 {Interactive Theorem Proving (ITP 2010)},
  editor =	 {M. Kaufmann and L. Paulson},
  publisher =	 Springer,
  series =	 LNCS,
  volume =	 6172,
  pages =	 {131-146},
  year =	 2010,
  doi =		 {10.1007/978-3-642-14052-5\_11}
}

@incollection{Satallax,
  year =	 2010,
  isbn =	 {978-3-642-14202-4},
  booktitle =	 {Automated Reasoning},
  volume =	 6173,
  series =	 {Lecture Notes in Computer Science},
  editor =	 {Giesl, J. and H{\"a}hnle, R.},
  doi =		 {10.1007/978-3-642-14203-1\_7},
  title =	 {Analytic Tableaux for Higher-Order Logic with
                  Choice},
  publisher =	 {Springer Berlin Heidelberg},
  author =	 {Backes, J. and Brown, C.E.},
  pages =	 {76-90},
}

@InProceedings{C26,
  keywords =	 {LEO Prover, Higher Order Logic, Automated Reasoning,
                  Henkin Semantics},
  author =	 {C. Benzm{\"u}ller and F. Theiss and L.C. Paulson and
                  A. Fietzke},
  title =	 {{LEO-II} - A Cooperative Automatic Theorem Prover
                  for Higher-Order Logic (System Description)},
  editor =	 {A. Armando and P. Baumgartner and G.  Dowek},
  booktitle =	 {Automated Reasoning, 4th International Joint
                  Conference, IJCAR 2008, Sydney, Australia, August
                  12-15, 2008, Proceedings},
  url =		 {http://christoph-benzmueller.de/papers/C26.pdf},
  publisher =	 {Springer},
  series =	 {LNCS},
  pages =	 {162-170},
  year =	 2008,
  doi =		 {10.1007/978-3-540-71070-7\_14},
  volume =	 5195,
  comment =	 {<a
                  href="http://christoph-benzmueller.de/papers/2008_IJCAR_LEO-II.pdf
                  " target="_blank">slides</a>},
}

@Book{Nipkow-Paulson-Wenzel:2002,
  author =	 {T. Nipkow and L.C. Paulson and M. Wenzel},
  title =	 {Isabelle/HOL --- A Proof Assistant for Higher-Order
                  Logic},
  publisher =	 {Springer},
  series =	 {LNCS},
  volume =	 2283,
  year =	 2002
}

@inproceedings{EasyChair:128,
  author =	 {L.C. Paulson and J.C. Blanchette},
  title =	 {Three years of experience with Sledgehammer, a
                  Practical Link Between Automatic and Interactive
                  Theorem Provers},
  booktitle =	 {IWIL 2010},
  editor =	 {G. Sutcliffe and S. Schulz and E. Ternovska},
  series =	 {EPiC Series},
  volume =	 2,
  pages =	 {1-11},
  year =	 2012,
  publisher =	 {EasyChair},
  bibsource =	 {EasyChair, http://www.easychair.org},
  issn =	 {2040-557X},
}

@inproceedings{hurd2003d,
  author =	 {J. Hurd},
  title =	 {First-Order Proof Tactics in Higher-Order Logic
                  Theorem Provers},
  booktitle =	 {Design and Application of Strategies/Tactics in
                  Higher Order Logics (STRATA 2003)},
  editor =	 {M. Archer and B. Di Vito and C. Mu{\~{n}}oz},
  series =	 {{NASA} Technical Reports},
  year =	 2003,
  pages =	 {56-68},
  url =		 {http://www.gilith.com/research/papers},
}

@PhdThesis{sultana14:_higher,
  author =	 {Sultana, N.},
  title =	 {{Higher-order proof translation}},
  year =	 2015,
  school =	 {Computer Laboratory, University of Cambridge},
  note =	 {Available as Tech Report UCAM-CL-TR-867}
}

@InProceedings{ECAI,
  keywords =	 {Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, LEO Prover, Higher Order Logic},
  editor =	 {T. Schaub and G. Friedrich and B. O'Sullivan},
  author =	 {C. Benzm{\"u}ller and B. Woltzenlogel Paleo},
  title =	 {Automating {G\"{o}del's} Ontological Proof of
                  {God}'s Existence with Higher-order Automated
                  Theorem Provers},
  pages =	 {93 -- 98},
  booktitle =	 {ECAI 2014},
  doi =		 {10.3233/978-1-61499-419-0-93},
  series =	 {Frontiers in Artificial Intelligence and
                  Applications},
  volume =	 263,
  publisher =	 {IOS Press},
  year =	 2014,
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2014-ECAI.pdf
                  " target="_blank">slides</a>},
  url =		 {http://christoph-benzmueller.de/papers/C40.pdf},
}

@inproceedings{SPASS,
  author =	 {C. Weidenbach and D. Dimova and A. Fietzke and
                  R. Kumar and M. Suda and P. Wischnewski},
  title =	 {{SPASS} Version 3.5},
  booktitle =	 {Automated Deduction - CADE-22, 22nd International
                  Conference on Automated Deduction, Montreal, Canada,
                  August 2-7, 2009. Proceedings},
  pages =	 {140--145},
  year =	 2009,
  doi =		 {10.1007/978-3-642-02959-2\_10},
  editor =	 {R.A. Schmidt},
  series =	 {LNCS},
  volume =	 5663,
  publisher =	 {Springer},
}

@inproceedings{E,
  author =	 {S. Schulz},
  title =	 {System Description: {E} 1.8},
  booktitle =	 {Logic for Programming, Artificial Intelligence, and
                  Reasoning - 19th International Conference, LPAR-19,
                  Stellenbosch, South Africa, December 14-19,
                  2013. Proceedings},
  pages =	 {735--743},
  year =	 2013,
  doi =		 {10.1007/978-3-642-45221-5\_49},
  editor =	 {K.L. McMillan and A. Middeldorp and A. Voronkov},
  title =	 {Logic for Programming, Artificial Intelligence, and
                  Reasoning - 19th International Conference, LPAR-19,
                  Stellenbosch, South Africa, December 14-19,
                  2013. Proceedings},
  series =	 {LNCS},
  volume =	 8312,
  publisher =	 {Springer},
}

@inproceedings{Vampire,
  author =	 {L. Kov{\'{a}}cs and A. Voronkov},
  title =	 {First-Order Theorem Proving and Vampire},
  booktitle =	 {Computer Aided Verification - 25th International
                  Conference, {CAV} 2013, Saint Petersburg, Russia,
                  July 13-19, 2013. Proceedings},
  pages =	 {1--35},
  year =	 2013,
  doi =		 {10.1007/978-3-642-39799-8\_1},
  editor =	 {N. Sharygina and H. Veith},
  series =	 {LNCS},
  volume =	 8044,
  publisher =	 {Springer},
}

@inproceedings{Z3,
  author =	 {L.M. de Moura and N. Bj{\o}rner},
  title =	 {{Z3:} An Efficient {SMT} Solver},
  booktitle =	 {Tools and Algorithms for the Construction and
                  Analysis of Systems, 14th International Conference,
                  {TACAS} 2008, Budapest, Hungary, March 29-April 6,
                  2008. Proceedings},
  pages =	 {337--340},
  year =	 2008,
  doi =		 {10.1007/978-3-540-78800-3\_24},
  editor =	 {C.R. Ramakrishnan and J. Rehof},
  series =	 {LNCS},
  volume =	 4963,
  publisher =	 {Springer},
}

@InProceedings{IJCAI,
  keywords =	 {Higher Order Logic, LEO Prover, Semantic Embedding,
                  Conditional Logics, Combinations of Logics},
  author =	 {C. Benzm{\"u}ller},
  title =	 {Automating Quantified Conditional Logics in {HOL}},
  booktitle =	 {23rd International Joint Conference on Artificial
                  Intelligence (IJCAI-13)},
  isbn =	 {978-1-57735-633-2},
  address =	 {Beijing, China},
  pages =	 {746-753},
  editor =	 {F. Rossi},
  year =	 2013,
  url =		 {http://ijcai.org/papers13/Papers/IJCAI13-117.pdf},
  comment =	 {<a
                  href="http://christoph-benzmueller.de/papers/2013-IJCAI-Poster.pdf"
                  target="_blank " target="_blank">poster</a>},
}

@incollection{CVC4,
  year =	 2011,
  isbn =	 {978-3-642-22109-5},
  booktitle =	 {Computer Aided Verification},
  volume =	 6806,
  series =	 {LNCS},
  editor =	 {Gopalakrishnan, Ganesh and Qadeer, Shaz},
  doi =		 {10.1007/978-3-642-22110-1\_14},
  title =	 {CVC4},
  publisher =	 {Springer Berlin Heidelberg},
  author =	 {Barrett, C. and Conway, C.L. and Deters, M. and
                  Hadarean, L. and Jovanovic, D. and King, T. and
                  Reynolds, A. and Tinelli, C.},
  pages =	 {171-177},
  language =	 {English}
}


@InProceedings{C40,
  keywords =	 {Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, LEO Prover, Higher Order Logic},
  editor =	 {Torsten Schaub and Gerhard Friedrich and Barry
                  O'Sullivan},
  author =	 {Christoph Benzm{\"u}ller and Woltzenlogel
                  Paleo, Bruno},
  title =	 {Automating {G\"{o}del's} Ontological Proof of
                  {God}'s Existence with Higher-order Automated
                  Theorem Provers},
  pages =	 {93 -- 98},
  booktitle =	 {ECAI 2014},
  doi =		 {10.3233/978-1-61499-419-0-93},
  series =	 {Frontiers in Artificial Intelligence and
                  Applications},
  volume =	 263,
  publisher =	 {IOS Press},
  year =	 2014,
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2014-ECAI.pdf
                  " target="_blank">slides</a>},
  url =		 {http://christoph-benzmueller.de/papers/C40.pdf},
}



@misc{ModalProvers,
  author = {Renate Schmidt},
  title = {List of Modal Provers (\url{www.cs.man.ac.uk/~schmidt/tools/})},
  url = {http://www.cs.man.ac.uk/~schmidt/tools/},
  lastchecked = {2014-12-12}
}

@ARTICLE{2013arXiv1302.2898H,
  author =	 {{Hales}, T.},
  title =	 "{Mathematics in the Age of the Turing Machine}",
  journal =	 {ArXiv e-prints},
  archivePrefix ="arXiv",
  eprint =	 {1302.2898},
  primaryClass = "math.HO",
  keywords =	 {Mathematics - History and Overview},
  year =	 2013,
  month =	 feb,
  adsurl =	 {http://adsabs.harvard.edu/abs/2013arXiv1302.2898H},
  adsnote =	 {Provided by the SAO/NASA Astrophysics Data System}
}

@article{ACL2_1997,
  author    = {Matt Kaufmann and
               J. Strother Moore},
  title     = {An Industrial Strength Theorem Prover for a Logic Based
               on {Common Lisp}},
  journal   = {IEEE Trans. Software Eng.},
  volume    = {23},
  number    = {4},
  year      = {1997},
  pages     = {203-213},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/32.588534},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Proceedings{ACM72,
  booktitle =    "Proceedings of the ACM Annual Conference",
  title =        "Proceedings of the {ACM} Annual Conference 1972",
  year =         1972,
}

@InProceedings{Agda99,
  author = 	 {C. Coquand and T. Coquand},
  title = 	 {Structured type theory},
  booktitle = {Proc.~of LMF’99: Workshop on Logical Frameworks and Meta-languages},
  editor = 	 {A. Felty},
  year = {1999},
  url = {http://www.site.uottawa.ca/~afelty/LFM99/}
}

@Article{AnCo:ahol84,
  old-key =      "AnCo84",
  author =       "Peter B. Andrews and Eve Longini-Cohen and Dale
                  Miller and Frank Pfenning",
  journal =      "Contemp. Math",
  pages =        "169--192",
  title =        "Automating Higher Order Logics",
  volume =       29,
  year =         1984,
}

@Book{Andrews02,
  author =       "Peter B. Andrews",
  title =        "An Introduction to Mathematical Logic and Type
                  Theory: To Truth Through Proof",
  publisher =    "Kluwer Academic Publishers",
  year =         2002,
  edition =      "Second",
}

@book{andrews2002introduction,
  title =        {An Introduction to Mathematical Logic and Type
                  Theory: To Truth Through Proof},
  author =       {Peter B Andrews},
  series =       {Applied Logic Series},
  volume =       27,
  year =         2002,
  publisher =    {Springer}
}

@article{daCosta,
  title = {Semantical Analysis of the Calculi Cn},
  author = {da Costa, N.C.A. and Alves, E.H.},
  journal = {Notre Dame Journal of Formal Logic},
  year = {1977},
  volume = {18},
  number = {4},
  pages = {621--630}
}

@article{Tanaka,
  title = {Three Schools of Paraconsistency},
  author = {Tanaka, K.},
  journal = {The Australasian Journal of Logic},
  year = {2003}
}

@book{Paraconsistency,
  title = {Handbook of Paraconsistency},
  editor = {Beziau, J.Y. and Carnielli, W. and Gabbay, D.},
  year = {2007},
  publisher = {College Publications}
}

@article{JoaoMarcos,
  title = {Modality and Paraconsistency},
  author = {Jo\~ao Marcos},
  year = {2005},
  journal = {The Logica Yearbook},
  pages = {213--222} 
}

@article{RelevantLogics1,
  title = {Simplified Semantics for Basic Relevant Logics},
  author = {Priest, G. and Sylvan, R.},
  journal = {Journal of Philosophical Logic},
  year = {1992}
}

@misc{HoareLogicInIsabelle,
  title = {Hoare Logic in Isabelle},
  author = {Makarius Wenzel},
  note = {\url{http://isabelle.in.tum.de/dist/library/HOL/HOL-Isar_Examples/Hoare.html}}
}


@article{Nameless,
  author    = {Arthur Chargu{\'{e}}raud},
  title     = {The Locally Nameless Representation},
  journal   = {J. Autom. Reasoning},
  volume    = {49},
  number    = {3},
  pages     = {363--408},
  year      = {2012},
  url       = {https://doi.org/10.1007/s10817-011-9225-2},
  doi       = {10.1007/s10817-011-9225-2},
  timestamp = {Thu, 25 Oct 2012 21:20:16 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jar/Chargueraud12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{RelevantLogics2,
  title = {Relevance Logic},
  author = {Dunn, J.M. and Restall, G.},
  journal = {Handbook of Philosophical Logic},
  volume = {6},
  pages = {1--136},
  year = {2002}
}

@article{Jaskowski69,
  title = {Propositional Calculus for Contradictory Deductive Systems},
  year = {1969},
  author = {Ja\'{s}kowski, S.},
  journal = {Studia Logica},
  volume = {24},
  pages = {143--157}
}

@article{Jaskowski48,
  title = {Rachunek zda\'n dla system\'ow dedukcyjnych sprzecznych},
  year = {1948},
  author = {Ja\'{s}kowski, S.},
  journal = {Studia Societatis Scientiarun Torunesis},
  volume = {1},
  number = {5},
  pages = {55--77}
}

@article{BeliefRevision1,
  title = {Paraconsistent Belief Revision},
  author = {Priest, G.},
  year = {2001},
  journal = {Theoria},
  volume = {67},
  pages = {214 -- 228}
}

@inproceedings{BeliefRevision2,
  title = {Realistic Belief Revision},
  author = {Restall, G. and Slaney, J.},
  year = {1995},
  booktitle = {Proceedings of the Second World Conference in the Fundamentals of Artificial Intelligence},
  pages = {367--378}
}

@Misc{Andrews73,
  author =       "Peter B. Andrews",
  year =         1973,
  note =         "letter to Roger Hindley dated January 22, 1973",
}

@Article{Andrews74b,
  author =       "Peter B. Andrews",
  title =        "Provability in Elementary Type Theory",
  journal =      "Zeitschrift fur Mathematische Logic und Grundlagen
                  der Mathematik",
  year =         1974,
  volume =       20,
  pages =        "411--418",
}

@Book{Andrews86,
  author =       "Peter B. Andrews",
  publisher =    "Academic Press",
  title =        "{An Introduction to Mathematical Logic and Type
                  Theory: To Truth Through Proof}",
  year =         1986,
}

@Article{Andrews:gmae72,
  author =       "P.B.~Andrews",
  journal =      "Journal of Symbolic Logic",
  number =       2,
  pages =        "395--397",
  title =        "General Models and Extensionality",
  volume =       37,
  year =         1972,
}

@Article{Andrews:gmdacitt72,
  author =       "Peter B. Andrews",
  journal =      "Journal of Symbolic Logic",
  number =       2,
  pages =        "385--394",
  title =        "General Models, Descriptions, and Choice in Type
                  Theory",
  volume =       37,
  year =         1972,
}

@Article{Andrews:ocahol89,
  author =       "Peter B. Andrews",
  journal =      "J. of Autom. Reasoning",
  pages =        "257--291",
  title =        "On connections and Higher Order Logic",
  volume =       5,
  number =       3,
  year =         "1989",
  ee =           "https://doi.org/10.1007/BF00248320",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@Article{Andrews:ratcoa74,
  author =       "Peter B. Andrews",
  journal =      "Notre Dame Journal of Formal Logic",
  pages =        "73--84",
  title =        "Resolution and the Consistency of Analysis",
  volume =       15,
  number =       1,
  year =         1974,
}

@Article{Andrews:ritt71,
  author =       "Peter B. Andrews",
  journal =      "Journal of Symbolic Logic",
  number =       3,
  title =        "Resolution in Type Theory",
  volume =       36,
  pages =        "414--432",
  year =         1971,
  location =     "miko",
}

@Book{Automath94,
  editor = 	 {R. P. Nederpelt and J. H. Geuvers and R. C. De Vrijer},
  title = 	 {Selected Papers on Automath},
  publisher = 	 {North Holland},
  year = 	 {1994},
  volume = 	 {133},
  series = 	 {Studies in Logic and The Foundations of Mathematics},
}

@InProceedings{B10,
  keywords =	 {Proof Assistants, OMEGA, Interactive Proof,
                  Automated Reasoning, Proof Planning, System
                  Integration, Agents},
  author =	 {Serge Autexier and Christoph Benzm\"uller and
                  Dominik Dietrich and J\"org Siekmann},
  editor =	 {Matthew W. Crocker and J\"org Siekmann},
  booktitle =	 {Resource-Adaptive Cognitive Processes},
  title =	 {{OMEGA}: Resource-Adaptive Processes in an Automated
                  Reasoning System},
  series =	 {Cognitive Technologies},
  publisher =	 {Springer, Cognitive Technologies},
  pages =	 {389-423},
  year =	 2010,
}

@article{BBP13,
  author    = {Jasmin Christian Blanchette and
               Sascha B{\"o}hme and
               Lawrence C. Paulson},
  title     = {Extending {Sledgehammer} with {SMT} Solvers},
  journal   = {J. Autom. Reasoning},
  volume    = {51},
  number    = {1},
  year      = {2013},
  pages     = {109-128},
  ee        = {https://doi.org/10.1007/s10817-013-9278-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{BC04,
    Author       = "Bertot, Y. and Casteran, P.",
    Year         = "2004",
    Title        = "{Interactive Theorem Proving and Program Development -
                    Coq'Art: The Calculus of Inductive Constructions}",
    Series       = "Texts in Theoretical Computer Science",
    Publisher    = "Springer",
    Comment      = ""
}

@inproceedings{BN10,
  author    = {Jasmin Christian Blanchette and
               Tobias Nipkow},
  title     = {Nitpick: A Counterexample Generator for Higher-Order Logic
               Based on a Relational Model Finder},
  booktitle = {Proc. of ITP 2010},
  pages     = {131-146},
  editor    = {Matt Kaufmann and
               Lawrence C. Paulson},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6172},
  year      = {2010},
}

@InProceedings{BackesBrown2010,
  title =        "Analytic Tableaux for Higher-Order Logic with
                  Choice",
  author =       "Julian Backes and Chad E. Brown",
  year =         2010,
  address =      "{Saarbr{\"u}cken, Germany}",
  booktitle =    "Fifth International Joint Conference on Automated
                  Reasoning (IJCAR 2010)",
  publisher =    "Springer",
  note =         "to appear",
}

@Book{Barendregt84,
  author =       "Henk P. Barendregt",
  publisher =    "North Holland",
  title =        "The Lambda Calculus",
  year =         1984,
}

@inproceedings{Beluga2010,
  author    = {Brigitte Pientka and
               Joshua Dunfield},
  title     = {Beluga: A Framework for Programming and Reasoning with Deductive
               Systems (System Description)},
  pages     = {15-21},
  editor    = {J{\"u}rgen Giesl and
               Reiner H{\"a}hnle},
  booktitle     = {Automated Reasoning, 5th International Joint Conference,
               IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6173},
  year      = {2010},
  isbn      = {978-3-642-14202-4},
  ee        = {https://doi.org/10.1007/978-3-642-14203-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@PhdThesis{Ben99,
  author =       "C. Benzm{\"u}ller",
  title =        "Equality and Extensionality in Automated
                  Higher-Order Theorem Proving",
  school =       "Saarland University",
  year =         1999,
  URL =          "http://www.ags.uni-sb.de/\textasciitilde
                  chris/papers/diss.ps.gz",
}

@TechReport{Ben:acaasafehor97,
  author =       "Christoph Benzm{\"u}ller",
  title =        "A Calculus and a System Architecture for Extensional
                  Higher-Order Resolution",
  institution =  "Department of Mathematical Sciences, Carnegie Mellon
                  University, Pittsburgh,USA",
  year =         1997,
  month =        jun,
  type =         "Research Report",
  number =       "97-198",
}

@InProceedings{Ben:ehoparr99,
  author =       "Christoph Benzm{\"u}ller",
  title =        "Extensional Higher-Order Paramodulation and
                  {RUE}-Resolution",
  year =         1999,
  booktitle =    "Proceedings of the 16th International {C}onference
                  on {A}utomated {D}eduction",
  editor =       "Harald Ganzinger",
  publisher =    "Springer",
  address =      "Trento, Italy",
  series =       "LNAI",
  number =       1632,
  chrisnote =    10,
  keywords =     "!OMEGA!,ARTICLE",
  URL =          "http://www.ags.uni-sb.de/\textasciitilde
                  chris/papers/cade99.ps.gz",
  pages =        "399--413",
  abstract =     "This paper presents two approaches to primitive
                  equality treatment in higher-order (HO) automated
                  theorem proving: a calculus $\EXTPARA$ adapting
                  traditional first-order (FO)
                  paramodulation~\cite{RoWo69} , and a calculus
                  $\EXTRUE$ adapting FO
                  RUE-Resolution~\cite{Digricoli79} to HO logic (based
                  on Church's simply typed
                  $\lambda$-calculus). $\EXTPARA$ and $\EXTRUE$ extend
                  the extensional HO resolution approach
                  $\EXTRES$~\cite{BenKoh:ehor98}. In order to reach
                  Henkin completeness without the need for additional
                  extensionality axioms both calculi employ new,
                  positive extensionality rules analogously to the
                  respective negative ones provided by $\EXTRES$ that
                  operate on unification constraints. As the
                  extensionality rules have an intrinsic and
                  unavoidable difference-reducing character the HO
                  paramodulation approach looses its pure
                  term-rewriting character. On the other hand examples
                  demonstrate that the extensionality rules harmonise
                  rather well with the difference-reducing HO
                  RUE-resolution idea.",
}

@TechReport{BenBroKoh:_seman_techn_higher_order_cut_elimin,
  author =       "Christoph Benzm{\"u}ller and Chad E. Brown and
                  Michael Kohlhase",
  title =        "Semantic Techniques for Higher-Order
                  Cut-Elimination",
  institution =  "Saarland University, Saarbr{\"u}cken, Germany",
  year =         2004,
  type =         "SEKI Technical Report",
  number =       "SR-2004-07",
  note =         "Available at:
                  \url{http://www.ags.uni-sb.de/~chris/papers/R37.pdf}",
}

@Unpublished{BenBroKoh:mecfhol02,
  author =       "Christoph Benzm{\"u}ller and Chad E. Brown and
                  Michael Kohlhase",
  title =        "Semantic Techniques for Higher-Order
                  Cut-Elimination",
  note =         "manuscript,
                  http://www.ags.uni-sb.de/\verb+~+chris/papers/R23.pdf",
  year =         2002,
}

@Article{BenBroKoh:mehol02,
  author =       "Christoph Benzm{\"u}ller and Chad Brown and Michael
                  Kohlhase",
  title =        "Higher-Order Semantics and Extensionality",
  journal =      "Journal of Symbolic Logic",
  year =         2004,
  volume =       69,
  number =       4,
  pages =        "1027--1088",
}


@InCollection{B8,
  keywords =	 {Higher Order Logic},
  author =	 {Christoph Benzm{\"u}ller and Chad Brown and Michael
                  Kohlhase},
  editor =	 {Christoph Benzm{\"u}ller and Chad Brown and J{\"o}rg
                  Siekmann and Richard Statman},
  booktitle =	 {Reasoning in Simple Type Theory: Festschrift in
                  Honor of Peter B.~Andrews on His 70th Birthday},
  title =	 {Cut Elimination with Xi-Functionality},
  publisher =	 {College Publications},
  year =	 2008,
  series =	 {Studies in Logic, Mathematical Logic and
                  Foundations},
  isbn =	 {978-1-904987-70-3},
  url =		 {http://christoph-benzmueller.de/papers/B8.pdf},
  pages =	 {84-100},
}

@TechReport{BenBroKoh:mehol03,
  author =       "Christoph Benzm{\"u}ller and and Chad E. Brown and
                  Michael Kohlhase",
  title =        "Higher-Order Semantics and Extensionality",
  year =         2003,
  institution =  "Department of Mathematical Sciences, Carnegie Mellon
                  University",
  type =         "Research Report",
  number =       "03-001",
}

@InProceedings{BenKoh:ehor98,
  author =       "Christoph Benzm{\"u}ller and Michael Kohlhase",
  title =        "Extensional Higher Order Resolution",
  pages =        "56--72",
  crossref =     "CADE98",
  year =         1998,
}

@InProceedings{BenKoh:lahotp98,
  author =       "Christoph Benzm{\"u}ller and Michael Kohlhase",
  title =        "{LEO} -- a Higher Order Theorem Prover",
  pages =        "139--144",
  crossref =     "CADE98",
  year =         1998,
}

@TechReport{BenKoh:mefhol97,
  author =       "Christoph Benzm{\"u}ller and Michael Kohlhase",
  title =        "Model Existence for Higher-Order Logic",
  institution =  "Saarland University",
  year =         1997,
  type =         "SEKI-Report",
  number =       "SR-97-09",
}

@TechReport{BenKoh:rfhm97,
  author =       "Christoph Benzm{\"u}ller and Michael Kohlhase",
  title =        "Resolution for {Henkin} Models",
  institution =  "Universit{\"a}t des Saarlandes",
  year =         1997,
  type =         "SEKI-Report",
  number =       "SR-97-10",
}

@Book{BibSch:adabfa98,
  key =          "Bibel",
  title =        "Automated Deduction -- {A} Basis for Applications",
  booktitle =    "Automated Deduction -- A Basis for Applications",
  publisher =    "Kluwer",
  year =         1998,
  editor =       "Wolfgang Bibel and Peter Schmitt",
}

@inproceedings{BlanchetteBPS13,
  author    = {Jasmin Christian Blanchette and
               Sascha B{\"o}hme and
               Andrei Popescu and
               Nicholas Smallbone},
  title     = {Encoding Monomorphic and Polymorphic Types},
  booktitle = {Proc. of TACAS-19},
  year      = {2013},
  pages     = {493-507},
  editor    = {Nir Piterman and
               Scott A. Smolka},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7795},
}

@inproceedings{Brown02,
  author    = {Chad E. Brown},
  title     = {Solving for Set Variables in Higher-Order Theorem Proving},
  booktitle = {Proc. of CADE-18},
  year      = {2002},
  pages     = {408-422},
  editor    = {Andrei Voronkov},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2392},
}

@inproceedings{Brown05,
  author    = {Chad E. Brown},
  title     = {Reasoning in Extensional Type Theory with Equality},
  booktitle = {Proc. of CADE-20},
  year      = {2005},
  pages     = {23-37},
  editor    = {Robert Nieuwenhuis},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3632},
}

@Book{Brown07,
  author = 	 {Chad E. Brown},
  title = 	 {Automated Reasoning in Higher-Order Logic},
  publisher = 	 {College Publications},
  year = 	 2007,
  note = {This is book is a revised version of the authors thesis
                  \emph{Set Comprehension in Church's Type Theory},
                  Dep. of Mathematical Sciences, Carnegie Mellon
                  University, 2004.}
} 

@PhdThesis{BrownPhD,
  author =       "Chad E. Brown",
  title =        "Set Comprehension in Church's Type Theory",
  school =       "Department of Mathematical Sciences, Carnegie Mellon
                  University",
  year =         2004,
  note = {See also Chad E. Brown, \emph{Automated Reasoning in Higher-Order Logic}, College Publications, 2007}
}

@article{BrownSmolka2010,
  author    = {Chad E. Brown and
               Gert Smolka},
  title     = {Analytic Tableaux for Simple Type Theory and its First-Order
               Fragment},
  journal   = {Logical Methods in Computer Science},
  volume    = {6},
  number    = {2},
  year      = {2010},
  ee        = {http://arxiv.org/abs/1004.1947},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jar/Brown13,
  author    = {Chad E. Brown},
  title     = {Reducing Higher-Order Theorem Proving to a Sequence of SAT
               Problems},
  journal   = {J. Autom. Reasoning},
  volume    = {51},
  number    = {1},
  year      = {2013},
  pages     = {57-77},
  ee        = {https://doi.org/10.1007/s10817-013-9283-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Article{Bruijn72,
  title =        "Lambda Calculus Notation with Nameless Dummies, a
                  Tool for Automatic Formula Manipulation, with an
                  Application to the {Church-Rosser} Theorem",
  author =       "Nicolaas Govert de Bruijn",
  journal =      "Indagationes Mathematicae",
  pages =        "381--392",
  volume =       34,
  number =       5,
  year =         1972,
}

@InProceedings{Busch94,
  author =       "Holger Busch",
  title =        "First-Order Automation for Higher-Order-Logic
                  Theorem Proving",
  booktitle =    "Proceedings of the 7th International Workshop on
                  Higher Order Logic Theorem Proving and Its
                  Applications",
  year =         1994,
  ISBN =         "3-540-58450-1",
  pages =        "97--112",
  publisher =    "Springer-Verlag",
  address =      "London, UK",
}

@InProceedings{C1,
  keywords =     {Proof Assistants, OMEGA, Interactive Proof,
                  Automated Reasoning, Proof Planning, System
                  Integration},
  author =       {Christoph Benzm{\"u}ller and Lassaad Cheikhrouhou
                  and Detlef Fehrer and Armin Fiedler and Xiaorong
                  Huang and Manfred Kerber and Michael Kohlhase and
                  Karsten Konrad and Erica Melis and Andreas Meier and
                  Wolf Schaarschmidt and J{\"o}rg Siekmann and Volker
                  Sorge},
  title =        {{OMEGA}: Towards a mathematical assistant},
  editor =       {William McCune},
  booktitle =    {Proceedings of CADE-14},
  publisher =    {Springer},
  series =       {LNCS},
  number =       1249,
  pages =        {252-255},
  year =         1997,
  doi =          {10.1007/3-540-63104-6_23},
  URL =          {http://christoph-benzmueller.de/papers/C1.pdf},
  abstract =     {{Omega} is a mixed-initiative system with the
                  ultimate purpose of supporting theorem proving in
                  main-stream mathematics and mathematics
                  education. The current system consists of a proof
                  planner and an integrated collection of tools for
                  formulating problems, proving subproblems, and proof
                  presentation.}
}

@InProceedings{C2,
  keywords =	 {LEO Prover, Higher Order Logic, Automated Reasoning,
                  Henkin Semantics},
  author =	 {Christoph Benzm\"uller and Michael Kohlhase},
  title =	 {Extensional Higher-Order Resolution},
  year =	 1998,
  editor =	 {Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
  booktitle =	 {Proc. of CADE-15},
  series =	 {LNAI},
  number =	 1421,
  pages =	 {56-71},
  doi =		 {10.1007/BFb0054248},
  publisher =	 {Springer},
  URL =		 {http://christoph-benzmueller.de/papers/C2.pdf},
  abstract =	 {In this paper we present an extensional higher-order
                  resolution calculus that is complete relative to
                  Henkin model semantics. The treatment of the
                  extensionality principles -- necessary for the
                  completeness result -- by specialized
                  (goal-directed) inference rules is of practical
                  applicability, as an implentation of the calculus in
                  the LEO-System shows. Furthermore, we prove the
                  long-standing conjecture, that it is sufficient to
                  restrict the order of primitive substitutions to the
                  order of input formulae.}
}

@InProceedings{C25,
  keywords =     {Higher Order Logic, Henkin Semantics, Automated
                  Reasoning},
  author =       {Christoph Benzm{\"u}ller and Florian Rabe and Geoff
                  Sutcliffe},
  title =        {{THF0} -- The Core of the {TPTP} Language for
                  Classical Higher-Order Logic},
  editor =       {Alessandro Armando and Peter Baumgartner and Gilles
                  Dowek},
  booktitle =    {Proceeding of IJCAR 2008},
  URL =          {http://christoph-benzmueller.de/papers/C25.pdf},
  publisher =    {Springer},
  pages =        {491-506},
  series =       {LNCS},
  year =         2008,
  doi =          {10.1007/978-3-540-71070-7_41},
  volume =       5195
}

@InProceedings{C26,
  keywords =     {LEO Prover, Higher Order Logic, Automated Reasoning,
                  Henkin Semantics},
  author =       {Christoph Benzm{\"u}ller and Frank Theiss and
                  Lawrence Paulson and Arnaud Fietzke},
  title =        {{LEO-II} - A Cooperative Automatic Theorem Prover
                  for Higher-Order Logic (System Description)},
  OPTeditor =       {Alessandro Armando and Peter Baumgartner and Gilles
                  Dowek},
  booktitle =    {Proc.~of IJCAR 2008},
  URL =          {http://christoph-benzmueller.de/papers/C26.pdf},
  publisher =    {Springer},
  series =       {LNCS},
  pages =        {162-170},
  year =         2008,
  doi =          {10.1007/978-3-540-71070-7_14},
  number =       5195,
  comment =      {<a
                  href="http://christoph-benzmueller.de/papers/2008_IJCAR_LEO-II.pdf
                  " target="_blank">slides</a>},
}

@InProceedings{C27,
  keywords =	 {LEO Prover, Higher Order Logic, Automated Reasoning,
                  Henkin Semantics, Security Logics},
  author =	 {Christoph Benzm{\"u}ller},
  title =	 {Automating Access Control Logic in Simple Type
                  Theory with {LEO-II}},
  editor =	 {Dimitris Gritzalis and Javier L{\'o}pez},
  booktitle =	 {Emerging Challenges for Security, Privacy and Trust,
                  24th IFIP TC 11 International Information Security
                  Conference, SEC 2009, Pafos, Cyprus, May 18-20,
                  2009. Proceedings},
  publisher =	 {Springer},
  series =	 {IFIP},
  volume =	 297,
  year =	 2009,
  doi =		 {10.1007/978-3-642-01244-0_34},
  isbn =	 {978-3-642-01243-3},
  pages =	 {387-398},
  URL =		 {http://christoph-benzmueller.de/papers/C27.pdf},
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2009-SEC.pdf
                  " target="_blank">slides</a>},
}

@InProceedings{C3,
  keywords =     {LEO Prover, Higher Order Logic, Automated Reasoning,
                  Henkin Semantics},
  author =       {Christoph Benzm\"uller and Michael Kohlhase},
  title =        {{LEO} -- A Higher-Order Theorem Prover},
  year =         1998,
  editor =       {Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
  booktitle =    {Proc. of CADE-15},
  series =       {LNCS},
  number =       1421,
  pages =        {139-143},
  doi =          {10.1007/BFb0054256},
  publisher =    {Springer},
  URL =          {http://christoph-benzmueller.de/papers/C3.pdf},
  abstract =     {In this paper we discuss the Higher-Order Theorem
                  Prover LEO, which is based on the Extensional
                  Higher-Order Resolution Calculus EXTRES.},
  comment =      {<a href="~/chris/trunk/www/papers/1998-leo-talk.pdf
                  " target="_blank">slides</a>},
}

InProceedings{C34,
  keywords =	 {Higher Order Logic, Semantic Embedding, Modal
                  Logics, Automated Reasoning},
  author =	 {C. Benzm{\"u}ller and J. Otten and Th.
                  Raths},
  title =	 {Implementing and Evaluating Provers for First-order
                  Modal Logics},
  booktitle =	 {Proc. of the 20th European Conference on Artificial
                  Intelligence (ECAI)},
  OPTaddress =	 {Montpellier, France},
  pages =	 {163-168},
  year =	 2012,
  doi =		 {10.3233/978-1-61499-098-7-163},
  URL =		 {http://christoph-benzmueller.de/papers/C34.pdf},
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2012_ECAI.pdf
                  " target="_blank">slides</a>},
}

@InProceedings{C35,
  keywords =	 {Higher Order Logic, Semantic Embedding, Modal
                  Logics, Combinations of Logics},
  author =	 {Christoph Benzm{\"u}ller},
  title =	 {A Top-down Approach to Combining Logics},
  booktitle =	 {Proc. of ICAART-5},
  address =	 {Barcelona, Spain},
  year =	 2013,
  url =		 {http://christoph-benzmueller.de/papers/C35.pdf},
  doi =		 {10.5220/0004324803460351},
  publisher =	 {SciTePress Digital Library},
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2013-ICAART.pdf " target="_blank">slides</a>},
}


InProceedings{C38,
  keywords =	 {Higher Order Logic, Semantic Embedding, Modal
                  Logics, Automated Reasoning},
  author =	 {Christoph Benzm{\"u}ller and Thomas Raths},
  title =	 {{HOL} based First-order Modal Logic Provers},
  booktitle =	 {Proceedings of LPAR-19},
  address =	 {Stellenbosch, South Africa},
  editor =	 {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
  year =	 2013,
  URL =		 {http://christoph-benzmueller.de/papers/C38.pdf},
}

@INPROCEEDINGS{C5,
  AUTHOR =       {Christoph Benzm{\"u}ller},
  TITLE =        {Extensional Higher-Order Paramodulation and
                  {RUE}-Resolution},
  YEAR =         1999,
  BOOKTITLE =    {Proc. of CADE-16},
  EDITOR =       {Harald Ganzinger},
  PUBLISHER =    {Springer},
  SERIES =       {LNCS},
  number =       1632,
  URL =          {http://christoph-benzmueller.de/papers/C5.pdf},
  PAGES =        {399-413},
  doi =          {10.1007/3-540-48660-7_39},
  ABSTRACT =     {This paper presents two approaches to primitive
                  equality treatment in higher-order (HO) automated
                  theorem proving: a calculus $\EXTPARA$ adapting
                  traditional first-order (FO)
                  paramodulation~\cite{RoWo69} , and a calculus
                  $\EXTRUE$ adapting FO
                  RUE-Resolution~\cite{Digricoli79} to HO logic (based
                  on Church's simply typed
                  $\lambda$-calculus). $\EXTPARA$ and $\EXTRUE$ extend
                  the extensional HO resolution approach
                  $\EXTRES$~\cite{BenKoh:ehor98}. In order to reach
                  Henkin completeness without the need for additional
                  extensionality axioms both calculi employ new,
                  positive extensionality rules analogously to the
                  respective negative ones provided by $\EXTRES$ that
                  operate on unification constraints. As the
                  extensionality rules have an intrinsic and
                  unavoidable difference-reducing character the HO
                  paramodulation approach looses its pure
                  term-rewriting character. On the other hand examples
                  demonstrate that the extensionality rules harmonise
                  rather well with the difference-reducing HO
                  RUE-resolution idea.},
  comment =      {<a
                  href="http://christoph-benzmueller.de//papers/1999-CADE-para-and-rue.pdf
                  " target="_blank">slides</a>},
}

@Book{CA+86,
    Author       = "Constable, R. and Allen, S. and Bromly, H. and Cleaveland,
                    W. and Cremer, J. and Harper, R. and Howe, D. and
                    Knoblock, T. and Mendler, N. and Panangaden, P. and
                    Sasaki, J. and Smith, S.",
    Year         = "1986",
    Title        = "{Implementing Mathematics with the Nuprl Proof Development
                    System}",
    Publisher    = "Prentice-Hall",
    Comment      = "higher order"
}

@Proceedings{CADE98,
  key =          "CADE98",
  booktitle =    "Proceedings of the 15th {C}onference on {A}utomated
                  {D}eduction",
  title =        "Proceedings of the 15th {C}onference on {A}utomated
                  {D}eduction",
  publisher =    "Springer",
  address =      "Lindau, Germany",
  series =       "LNAI",
  editor =       "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  number =       1421,
  year =         1998,
}

@Article{ChiTur:man88,
  author =       "Gennaro Chierchia and Raymond Turner",
  title =        "Semantics and Property Theory",
  journal =      "Linguistics and Philosophy",
  year =         1988,
  volume =       11,
  pages =        "261--302",
}

@Article{Church40,
  author =       "Alonzo Church",
  title =        "A Formulation of the Simple Theory of Types",
  journal =      "Journal of Symbolic Logic",
  year =         1940,
  volume =       5,
  pages =        "56--68",
}

@Book{Church85,
  author =       "Alonzo Church",
  title =        "The Calculi of Lambda Conversion. ({AM}-6) (Annals
                  of Mathematics Studies)",
  year =         1985,
  ISBN =         "0-691-08394-0",
  publisher =    "Princeton University Press",
  address =      "Princeton, NJ, USA",
}

@Book{Chwistek48,
  author =       "L. Chwistek",
  title =        "The Limits of Science: Outline of Logic and of the
                  Methodology of the Exact Sciences",
  publisher =    "London: Routledge and Kegan Paul",
  year =         1948,
}

@Proceedings{DBLP:conf/cade/1998,
  editor =       "Claude Kirchner and H{\'e}l{\`e}ne Kirchner",
  title =        "Automated Deduction - {CADE}-15, 15th International
                  Conference on Automated Deduction, Lindau, Germany,
                  July 5-10, 1998, Proceedings",
  booktitle =    "CADE",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       1421,
  year =         1998,
  ISBN =         "3-540-64675-2",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@Proceedings{DBLP:conf/cade/2000,
  editor =       "David A. McAllester",
  title =        "Automated Deduction - {CADE}-17, 17th International
                  Conference on Automated Deduction, Pittsburgh, {PA},
                  {USA}, June 17-20, 2000, Proceedings",
  booktitle =    "CADE",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       1831,
  year =         2000,
  ISBN =         "3-540-67664-3",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}


@inproceedings{DBLP:conf/cade/Burel11,
  author    = {Guillaume Burel},
  title     = {Experimenting with Deduction Modulo},
  booktitle = {Proc. of CADE-23},
  pages     = {162-176},
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie-Stokkermans},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6803},
  year      = {2011},
}

@inproceedings{DBLP:conf/icfem/GuttmannSW11,
  author    = {Walter Guttmann and
               Georg Struth and
               Tjark Weber},
  title     = {Automating Algebraic Methods in Isabelle},
  booktitle = {Proc. of ICFEM 2011},
  year      = {2011},
  pages     = {617-632},
  editor    = {Shengchao Qin and
               Zongyan Qiu},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6991},
}

@Proceedings{DBLP:conf/iclp/1986,
  editor =       "Ehud Y. Shapiro",
  title =        "Third International Conference on Logic Programming,
                  Imperial College of Science and Technology, London,
                  United Kingdom, July 14-18, 1986, Proceedings",
  booktitle =    "ICLP",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       225,
  year =         1986,
  ISBN =         "3-540-16492-8",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@InProceedings{DBLP:conf/iclp/MillerN86,
  author =       "Dale Miller and Gopalan Nadathur",
  title =        "Higher-Order Logic Programming",
  booktitle =    "ICLP",
  year =         1986,
  pages =        "448--462",
  ee =           "https://doi.org/10.1007/3-540-16492-8_94",
  crossref =     "DBLP:conf/iclp/1986",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@inproceedings{DBLP:conf/tacas/MossakowskiML07,
  author    = {Till Mossakowski and
               Christian Maeder and
               Klaus L{\"u}ttich},
  title     = {The Heterogeneous Tool Set, {Hets}},
  pages     = {519-522},
  booktitle     = {Proceedings of TACAS 2007},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4424},
  year      = {2007},
}

@Proceedings{DBLP:conf/tphol/1998,
  editor =       "Jim Grundy and Malcolm C. Newey",
  title =        "Theorem Proving in Higher Order Logics, 11th
                  International Conference, {TPHOL}s'98, Canberra,
                  Australia, September 27 - October 1, 1998,
                  Proceedings",
  booktitle =    "TPHOLs",
  publisher =    "Springer",
  series =       "LNCS",
  volume =       1479,
  year =         1998,
  ISBN =         "3-540-64987-5",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@inproceedings{DBLP:conf/tphol/Harrison09a,
  author =       {John Harrison},
  title =        {{HOL Light}: An Overview},
  pages =        {60-66},
  booktitle =    {Proceedings of TPHOLs 2009},
  publisher =    {Springer},
  series =       {LNCS},
  volume =       5674,
  year =         2009,
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  booktitle     = {Theorem Proving in Higher Order Logics, 22nd International
               Conference, TPHOLs 2009, Munich, Germany, August 17-20,
               2009. Proceedings},
}

@article{DBLP:journals/ai/MelisMS08,
  author    = {Erica Melis and
               Andreas Meier and
               J{\"o}rg H. Siekmann},
  title     = {Proof planning with multiple strategies},
  journal   = {Artif. Intell.},
  volume    = {172},
  number    = {6-7},
  year      = {2008},
  pages     = {656-684},
  ee        = {https://doi.org/10.1016/j.artint.2007.11.004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/corr/abs-1211-7012,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Learning-assisted Automated Reasoning with Flyspeck},
  journal   = {CoRR},
  volume    = {abs/1211.7012},
  year      = {2012},
  ee        = {http://arxiv.org/abs/1211.7012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{DBLP:journals/jacm/Andrews81,
  author =       "Peter B. Andrews",
  title =        "Theorem Proving via General Matings",
  journal =      "J. ACM",
  volume =       28,
  number =       2,
  year =         1981,
  pages =        "193--214",
  ee =           "http://doi.acm.org/10.1145/322248.322249",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@article{DBLP:journals/jar/Beeson06,
  author =       {Michael Beeson},
  title =        {Mathematical Induction in {Otter}-Lambda},
  journal =      {J. Autom. Reasoning},
  volume =       36,
  number =       4,
  year =         2006,
  pages =        {311-344},
  ee =           {https://doi.org/10.1007/s10817-006-9036-z},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jar/HolmesA01,
  author =       {M. Randall Holmes and Jim Alves-Foss},
  title =        {The {Watson} Theorem Prover},
  journal =      {J. Autom. Reasoning},
  volume =       26,
  number =       4,
  year =         2001,
  pages =        {357-408},
  ee =           {https://doi.org/10.1023/A:1010652212067},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jar/KerberKS98,
  author    = {Manfred Kerber and
               Michael Kohlhase and
               Volker Sorge},
  title     = {Integrating Computer Algebra into Proof Planning},
  journal   = {J. Autom. Reasoning},
  volume    = {21},
  number    = {3},
  year      = {1998},
  pages     = {327-355},
  ee        = {https://doi.org/10.1023/A:1006059810729},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DBLP:journals/jar/Paulson89,
  author =       {Lawrence C. Paulson},
  title =        {The Foundation of a Generic Theorem Prover},
  journal =      {J. Autom. Reasoning},
  volume =       5,
  number =       3,
  year =         1989,
  pages =        {363-397},
  ee =           {https://doi.org/10.1007/BF00248324},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@Article{DBLP:journals/tc/Andrews76,
  author =       "Peter B. Andrews",
  title =        "Refutations by Matings",
  journal =      "IEEE Trans. Computers",
  volume =       25,
  number =       8,
  year =         1976,
  pages =        "801--807",
  ee =
                  "http://doi.ieeecomputersociety.org/10.1109/TC.1976.1674698",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@Article{DHK-HOL-ls-MSCS-2001,
  author =       "Gilles Dowek and Th{\'e}r{\`e}se Hardin and Claude
                  Kirchner",
  title =        "{HOL-$\lambda \sigma$} an intentional first-order
                  expression of higher-order logic",
  journal =      "Mathematical Structures in Computer Science",
  year =         2001,
  volume =       11,
  number =       1,
  pages =        "1--25",
}

@PhdThesis{DeMarco99,
  author =       "Mary DeMarco",
  school =       "Wesleyan University",
  title =        "Intuitionistic Semantics for Heriditarily Harrop
                  Logic Programming",
  year =         1999,
}

@Article{ELAN-1,
  author =       "Quang Huy Nguyen and Claude Kirchner and
                  H\&\#233;l\&\#232;ne Kirchner",
  title =        "External Rewriting for Skeptical Proof Assistants",
  journal =      "J. Autom. Reason.",
  volume =       29,
  number =       "3-4",
  year =         2002,
  ISSN =         "0168-7433",
  pages =        "309--336",
  publisher =    "Kluwer Academic Publishers",
  address =      "Hingham, MA, USA",
}

@inproceedings{EasyChair:101,
  author    = {Christoph Benzm\"uller and Nik Sultana},
  title     = {{LEO-II} Version 1.5},
  booktitle = {PxTP 2013},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series},
  volume    = 14,
  pages     = {2-10},
  year      = 2013,
  publisher = {EasyChair EPiC Series 14, 2-12},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2040-557X},
}

@inproceedings{Elf1994,
  author    = {Frank Pfenning},
  title     = {Elf: A Meta-Language for Deductive Systems (System Descrition)},
  pages     = {811-815},
  editor    = {Alan Bundy},
  booktitle     = {Automated Deduction - CADE-12, 12th International Conference
               on Automated Deduction, Nancy, France, June 26 - July 1,
               1994, Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {814},
  year      = {1994},
  isbn      = {3-540-58156-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Farmer08,
  author    = {William M. Farmer},
  title     = {The seven virtues of simple type theory},
  journal   = {J. Applied Logic},
  volume    = {6},
  number    = {3},
  year      = {2008},
  pages     = {267-286},
  ee        = {https://doi.org/10.1016/j.jal.2007.11.001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Farmer90,
  author    = {William M. Farmer},
  title     = {A Partial Functions Version of Church's Simple Theory of
               Types},
  journal   = {J. Symb. Log.},
  volume    = {55},
  number    = {3},
  year      = {1990},
  pages     = {1269-1291},
  ee        = {http://projecteuclid.org/euclid.jsl/1183743419},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{Fitting90,
  title =        "First-Order Logic and Automated Theorem Proving",
  author =       "Melvin Fitting",
  publisher =    "Springer",
  year =         1990,
}

@Book{Fitting96,
  author =       "Melvin Fitting",
  title =        "First-Order Logic and Automated Theorem Proving,
                  second edition",
  publisher =    "Springer",
  year =         1996,
  series =       "Graduate Texts in Computer Science",
  location =     "Fachbereichsbibliothek Informatik",
  idnumber =     "M 13130",
  signature =    "FIT m 96:1 2.Ex",
  ISBN =         "0-387-94593-8",
  status =       "available",
  bibtype =      "BOOK",
}

@Book{Frege1879,
  author =       "Gottlob Frege",
  title =        "Begriffsschrift, eine der arithmetischen
                  nachgebildete Formelsprache des reinen Denkens",
  publisher =    "Halle",
  note =         "Translated in \cite{vanHeijenoort67}",
  year =         1879,
}

@Book{Frege1893,
  author =       "Gottlob Frege",
  title =        "Grundgesetze der Arithmetik (Band {I})",
  year =         1893,
}

@InCollection{Frege86,
  author =       "G. Frege",
  title =        "Begriffsschrift, eine der arithmetischen
                  nachgebildete Formelsprache des reinen Denkens
                  (gekuerzter Nachdruck)",
  year =         1986,
  booktitle =    "Logik-Texte: Kommentierte Auswahl zur Geschichte der
                  Modernen Logik (vierte Auflage)",
  editor =       "K. Berka and L. Kreiser",
  publisher =    "Akademie-Verlag",
  address =      "Berlin",
  pages =        "82--107",
}

@Book{GoMe93,
  author =       "M. J. C. Gordon and T. F. Melham",
  title =        "Introduction to {HOL} -- {A} theorem proving
                  environment for higher order logic",
  publisher =    "Cambridge University Press",
  year =         1993,
}

@PhdThesis{Goedel29,
  author =       "Kurt G{\"o}del",
  title =        "{\"U}ber die Vollst{\"a}ndigkeit des
                  Logikkalk{\"u}ls",
  school =       "Universit{\"a}t Wien",
  year =         1929,
}

@Article{Goedel30,
  author =       "Kurt G{\"o}del",
  title =        "{Die Vollst{\"a}ndigkeit der Axiome des logischen
                  Funktionenkalk{\"u}ls}",
  journal =      "Monatshefte f{\"u}r Mathematik und Physik",
  year =         1930,
  volume =       37,
  number =       1,
  pages =        "349--360",
}

@Article{Goedel31,
  author =       "Kurt G{\"o}del",
  title =        "{\"U}ber formal unentscheidbare {S\"a}tze der
                  {Principia Mathematica} und verwandter {S}ysteme
                  {I}",
  journal =      "Monatshefte der Mathematischen Physik",
  year =         1931,
  volume =       38,
  pages =        "173--198",
  note =         "English Version in~\cite{vanHeijenoort67}",
}


@Book(GordonMelham93,
  Author =       "M.J. Gordon and T.F. Melham",
  Title =        "Introduction to {HOL}: A Theorem-Proving Environment
                  for Higher-Order Logic",
  Publisher =    "Cambridge University Press",
  Year =         1993
)

@InProceedings{HOL-CLAM-1,
  author =       "Konrad Slind and Michael J. C. Gordon and Richard J.
                  Boulton and Alan Bundy",
  title =        "System Description: An Interface Between
                  {CL}$^{\mbox{A}}${M} and {HOL}.",
  booktitle =    "CADE",
  year =         1998,
  pages =        "134--138",
  ee =
                  "http://link.springer.de/link/service/series/0558/bibs/1421/14210134.htm",
  crossref =     "DBLP:conf/cade/1998",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@InProceedings{HOL-CLAM-2,
  author =       "Richard J. Boulton and Konrad Slind and Alan Bundy
                  and Michael J. C. Gordon",
  title =        "An Interface between Clam and {HOL}.",
  booktitle =    "TPHOLs",
  year =         1998,
  pages =        "87--104",
  crossref =     "DBLP:conf/tphol/1998",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@article{HalesEtal2010,
  author    = {Thomas C. Hales and
               John Harrison and
               Sean McLaughlin and
               Tobias Nipkow and
               Steven Obua and
               Roland Zumkeller},
  title     = {A Revision of the Proof of the Kepler Conjecture},
  journal   = {Discrete {\&} Computational Geometry},
  volume    = {44},
  number    = {1},
  year      = {2010},
  pages     = {1-34},
  ee        = {https://doi.org/10.1007/s00454-009-9148-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Heck93,
  author =       "Jr. Richard G. Heck",
  journal =      "Journal of Symbolic Logic",
  title =        "The Development of Arithmetic in Frege's {\it
                  Grundgesetze der Arithmetik}",
  volume =       58,
  issue =        2,
  year =         1993,
  pages =        "579--601",
  note =         "This paper does not seem to exist?!",
}

@Book{Heijenoort67,
  author =       "Jean van Heijenoort",
  title =        "From {F}rege to {G\"{o}}del. {A} Source Book in
                  Mathematical Logic 1879--1931",
  publisher =    "Harvard University Press",
  year =         1967,
  address =      "Cambridge, Massachusetts",
}

@Article{Henkin50,
  author =       "L.~Henkin",
  journal =      "Journal of Symbolic Logic",
  number =       2,
  pages =        "81--91",
  title =        "Completeness in the Theory of Types",
  volume =       15,
  year =         1950,
}

@Article{Henkin96,
  author =       "Leon Henkin",
  journal =      "The Bulletin of Symbolic Logic",
  number =       2,
  pages =        "127--157",
  title =        "The discovery of my completeness proofs",
  volume =       2,
  year =         1996,
}

@Article{Henkin:dcp96,
  author =       "Leon Henkin",
  journal =      "The Bulletin of Symbolic Logic",
  volume =       2,
  number =       2,
  pages =        "127--158",
  title =        "The discovery of my completeness proofs",
  year =         1996,
}

@inproceedings{Henschen72,
 author = {Henschen, Lawrence J.},
 title = {N-sorted Logic for Automatic Theorem-proving in Higher-order Logic},
 booktitle = {Proceedings of the ACM Annual Conference - Volume 1},
 series = {ACM '72},
 year = 1972,
 location = {Boston, Massachusetts, USA},
 pages = {71--81},
 numpages = 11,
 url = {http://doi.acm.org/10.1145/800193.805823},
 doi = {10.1145/800193.805823},
 acmid = 805823,
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Artificial intelligence, Higher-order logic, Theorem proving},
}

@Book{HiSe86,
  author =       "J. R. Hindley and J. P. Seldin",
  publisher =    "Cambridge University Press",
  title =        "Introduction to Combinators and Lambda Calculus",
  year =         1986,
}

@Book{HindleySeldin86,
  author =       "Roger J. Hindley and Jonathan P. Seldin",
  title =        "Introduction to Combinators and Lambda-Calculs",
  publisher =    "Cambridge University Press",
  address =      "Cambridge",
  year =         1986,
  location =     "Fachbereichsbibliothek Informatik",
  idnumber =     "M 6417",
  signature =    "HIN r 86:1",
  ISBN =         "0-521-31839-4",
  status =       "available",
  bibtype =      "BOOK",
}

@Article{Hintikka55,
  title =        "Form and Content in Quantification Theory",
  author =       "K. J. J. Hintikka",
  journal =      "Acta Philosophica Fennica",
  volume =       8,
  pages =        "7--55",
  year =         1955,
}

@Article{HonsellLenisa99,
  author =       "Furio Honsell and Marina Lenisa",
  title =        "Coinductive Characterizations of Applicative
                  Structures",
  journal =      "Mathematical Structures in Computer Science",
  year =         1999,
  volume =       9,
  pages =        "403--435",
}

@InProceedings{HonsellSannella99,
  author =       "Furio Honsell and Donald Sannella",
  title =        "Pre-logical relations",
  booktitle =    "Proceedings of Computer Science Logic (CSL'99)",
  pages =        "546--561",
  year =         1999,
  volume =       1683,
  series =       "LNCS",
  publisher =    "Springer",
}

@InProceedings{Huet:amott73,
  author =       "G\'{e}rard P. Huet",
  booktitle =    "Proceedings of the 3rd International Joint
                  Conference on Artificial Intelligence",
  year =         1973,
  pages =        "139--146",
  title =        "A Mechanization of Type Theory",
}

@PhdThesis{Huet:cracmfhol72,
  author =       "G\'{e}rard P. Huet",
  school =       "Case Western Reserve University",
  title =        "Constrained Resolution: {A} Complete Method for
                  Higher Order Logic",
  year =         1972,
}

@inproceedings{Hurd02,
  author    = {Joe Hurd},
  title     = {An LCF-Style Interface between HOL and First-Order Logic},
  booktitle = {Proc. of CADE-18},
  year      = {2002},
  pages     = {134-138},
  editor    = {Andrei Voronkov},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2392},
  year      = {2002},
  isbn      = {3-540-43931-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@Proceedings{IJCAI73,
  key =          "IJCAI73",
  booktitle =    "Proceedings of the 3rd International Joint
                  Conference on Artificial Intelligence",
  title =        "Proceedings of the 3rd International Joint
                  Conference on Artificial Intelligence",
  year =         1973,
  editor =       "Donald E. Walker and Lewis Norton",
}

@inproceedings{IsaPlanner2003,
  author    = {Lucas Dixon and
               Jacques D. Fleuriot},
  title     = {{IsaPlanner}: A Prototype Proof Planner in Isabelle},
  pages     = {279-283},
  editor    = {Franz Baader},
  booktitle     = {Automated Deduction - CADE-19, 19th International Conference
               on Automated Deduction Miami Beach, FL, USA, July 28 - August
               2, 2003, Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2741},
  year      = {2003},
  isbn      = {3-540-40559-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Isabelle-Automation-1,
  author =       "Lawrence C. Paulson",
  title =        "Generic automatic proof tools",
  book =         "Automated reasoning and its applications: essays in
                  honor of Larry Wos",
  year =         1997,
  ISBN =         "0-262-22055-5",
  pages =        "23--47",
  publisher =    "MIT Press",
  address =      "Cambridge, MA, USA",
}

@Article{Isabelle-Automation-2,
  author =       "Lawrence C. Paulson",
  title =        "A Generic Tableau Prover and its Integration with
                  Isabelle.",
  journal =      "J. UCS",
  volume =       5,
  number =       3,
  year =         1999,
  pages =        "73--87",
  ee =
                  "http://www.jucs.org/jucs_5_3/a_generic_tableau_prover",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@Article{Isabelle-FOATP-1,
  author =       "Jia Meng and Claire Quigley and Lawrence C. Paulson",
  title =        "Automation for interactive proof: first prototype",
  journal =      "Inf. Comput.",
  volume =       204,
  number =       10,
  year =         2006,
  ISSN =         "0890-5401",
  pages =        "1575--1596",
  doi =          "https://doi.org/10.1016/j.ic.2005.05.010",
  publisher =    "Academic Press, Inc.",
  address =      "Duluth, MN, USA",
}

@Article{J1,
  keywords =	 {Proof Assistants, OMEGA, Proof Transformation,
                  System Integration, Higher Order Logic},
  author =	 {Christoph Benzm{\"u}ller and Matt Bishop and Volker
                  Sorge},
  title =	 {Integrating {TPS} and {OMEGA}},
  journal =	 {Journal of Universal Computer Science},
  year =	 1999,
  volume =	 5,
  number =	 3,
  pages =	 {188-207},
  URL =		 {http://christoph-benzmueller.de/papers/J1.pdf},
  abstract =	 {This paper reports on the integration of the
                  higher-order theorem proving environment TPS
                  [Andrews96] into the mathematical assistant OMEGA
                  [Omega97]. TPS can be called from OMEGA either as a
                  black box or as an interactive system. In black box
                  mode, the user has control over the parameters which
                  control proof search in TPS; in interactive mode,
                  all features of the TPS-system are available to the
                  user. If the subproblem which is passed to TPS
                  contains concepts defined in OMEGA's database of
                  mathematical theories, these definitions are not
                  instantiated but are also passed to TPS. Using a
                  special theory which contains proof tactics that
                  model the ND-calculus variant of TPS within OMEGA,
                  any complete or partial proof generated in TPS can
                  be translated one to one into an OMEGA proof
                  plan. Proof transformation is realised by proof plan
                  expansion in OMEGA's 3-dimensional proof data
                  structure, and remains transparent to the user.},
  doi =		 {10.3217/jucs-005-03-0188},
}

@Article{J18,
  keywords =	 {Higher Order Logic, Henkin Semantics, Cut
                  Elimination},
  author =	 {Christoph Benzm{\"u}ller and Chad Brown and Michael
                  Kohlhase},
  title =	 {Cut-Simulation and Impredicativity},
  journal =	 {Logical Methods in Computer Science},
  year =	 2009,
  volume =	 5,
  number =	 {1:6},
  pages =	 {1-21},
  doi =		 {10.2168/LMCS-5(1:6 for )2009},
  url =		 {http://christoph-benzmueller.de/papers/J18.pdf},
}

@Article{J21,
  keywords =	 {Higher Order Logic, LEO Prover, Semantic Embedding,
                  Modal Logics, Combinations of Logics, Henkin Semantics},
  author =	 {Christoph Benzm{\"u}ller and Lawrence Paulson},
  title =	 {Multimodal and Intuitionistic Logics in Simple Type
                  Theory},
  journal =	 {The Logic Journal of the IGPL},
  publisher =	 {Oxford University Press},
  year =	 2010,
  volume =	 18,
  number =	 6,
  pages =	 {881-892},
  doi =		 {10.1093/jigpal/jzp080},
  URL =		 {http://christoph-benzmueller.de/papers/J21.pdf},
}




@Article{J24,
  keywords =	 {Ontology Reasoning, System Integration, Automated
                  Reasoning},
  author =	 {Adam Pease and Christoph Benzm{\"u}ller},
  title =	 {Sigma: An Integrated Development Environment for
                  Formal Ontology},
  journal =	 {AI Communications},
  year =	 2013,
  volume =	 26,
  pages =	 {79-97},
  number =	 1,
  doi =		 {10.3233/AIC-120549},
  URL =		 {http://christoph-benzmueller.de/papers/J24.pdf},
}

Article{J25,
  keywords =	 {Higher Order Logic, Semantic Embedding,
                  Modal Logics, Henkin Semantics, Automated Reasoning},
  author =	 {Christoph Benzm{\"u}ller},
  title =	 {Combining and Automating Classical and Non-Classical
                  Logics in Classical Higher-Order Logic},
  journal =	 {Annals of Mathematics and Artificial Intelligence},
  year =	 2011,
  volume =	 62,
  number =	 {1-2},
  pages =	 {103-128},
  OPTdoi =		 {10.1007/s10472-011-9249-7},
  URL =		 {http://christoph-benzmueller.de/papers/J25.pdf},
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2010-ECAI-ARCOE-16-8.pdf " target="_blank">slides</a>},
}

@Article{J26,
  keywords =	 {Higher Order Logic, Semantic Embedding, Conditional
                  Logics, Automated Reasoning},
  author =	 {Christoph Benzm{\"u}ller and Dov Gabbay and Valerio
                  Genovese and Daniele Rispoli},
  title =	 {Embedding and Automating Conditional Logics in
                  Classical Higher-Order Logic},
  journal =      {Ann. Math. Artif. Intell.},
  ournal =	 {Annals of Mathematics and Artificial Intelligence},
  year =	 2012,
  volume =	 66,
  number =	 {1-4},
  pages =	 {257-271},
  OPTdoi =		 {10.1007/s10472-012-9320-z},
  URL =		 {http://christoph-benzmueller.de/papers/J26.pdf},
}

Article{J27,
 keywords =     {Ontology Reasoning, Automated Reasoning, Higher
                  Order Logic, Modal Logics},
  author =	 {Christoph Benzm{\"u}ller and Adam Pease},
  title =	 {Higher-order Aspects and Context in {SUMO}},
  journal =	 {Journal of Web Semantics},
  year =	 2012,
  volume =	 {12-13},
  pages =	 {104-117},
  doi =		 {10.1016/j.websem.2011.11.008},
  url =		 {http://christoph-benzmueller.de/papers/J27.pdf},
}

@Article{J5,
  keywords =	 {LEO Prover, Automated Reasoning, Higher Order Logic,
                  Henkin Semantics, History of Logic},
  author =	 {Christoph Benzm{\"u}ller},
  title =	 {Comparing Approaches to Resolution based
                  Higher-Order Theorem Proving},
  journal =	 {Synthese},
  publisher =	 {Springer},
  volume =	 133,
  number =	 {1-2},
  issn =	 {0039-7857},
  pages =	 {203-235},
  year =	 2002,
  url =		 {http://christoph-benzmueller.de/papers/J5.pdf},
  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},
}

@Book{KeY2007,
   editor =        {Bernhard Beckert and Reiner H\"ahnle and Peter H. Schmitt},
   title =         {Verification of Object-Oriented Software: The {KeY} Approach},
   series        = {LNCS 4334},
   publisher     = {Springer-Verlag},
   year          = {2007}
}

@inproceedings{Kerber91,
  author    = {Manfred Kerber},
  title     = {How to Prove Higher Order Theorems in First Order Logic},
  booktitle = {Proc. of IJCAI-12},
  year      = {1991},
  pages     = {137-142},
  editor    = {John Mylopoulos and
               Raymond Reiter},
  publisher = {Morgan Kaufmann},
  isbn      = {1-55860-160-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Kerber94,
  author    = {Manfred Kerber},
  title     = {On the Translation of Higher-Order Problems into First-Order
               Logic},
  booktitle = {Proc. of ECAI},
  year      = {1994},
  pages     = {145-149},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Key2007CADE,
  author    = {Bernhard Beckert and
               Martin Giese and
               Reiner H{\"a}hnle and
               Vladimir Klebanov and
               Philipp R{\"u}mmer and
               Steffen Schlager and
               Peter H. Schmitt},
  title     = {The KeY system 1.0 (Deduction Component)},
  pages     = {379-384},
  editor    = {Frank Pfenning},
  booktitle     = {Automated Deduction - CADE-21, 21st International Conference
               on Automated Deduction, Bremen, Germany, July 17-20, 2007,
               Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4603},
  year      = {2007},
  isbn      = {978-3-540-73594-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{KohSch99:homvr,
  author =       "Michael Kohlhase and Ortwin Scheja",
  title =        "Higher-Order Multi-Valued Resolution",
  journal =      "Journal of Applied Non-Classical Logics",
  year =         1999,
  volume =       9,
  number =       4,
}

@PhdThesis{Kohlhase94,
  author =       "Michael Kohlhase",
  school =       "Saarland University",
  title =        "A Mechanization of Sorted Higher-Order Logic Based
                  on the Resolution Principle",
  year =         1994,
}

@TechReport{Kohlhase94a,
  author =       "Michael Kohlhase",
  title =        "Higher-Order Order-Sorted Resolution",
  institution =  "Fachbereich Informatik, Universit{\"a}t des
                  Saarlandes",
  year =         1994,
  type =         "Seki Report",
  number =       "SR-94-1",
}

@InCollection{Kohlhase:hoatp98,
  author =       "Michael Kohlhase",
  title =        "Higher-Order Automated Theorem Proving",
  crossref =     "BibSch:adabfa98",
  volume =       1,
  pages =        "431--462",
}

@InProceedings{Kohlhase:hot95,
  author =       "Michael Kohlhase",
  title =        "Higher-Order Tableaux",
  pages =        "294--309",
  crossref =     "TABLEAU95",
}

@book{LCF,
  author    = {Michael J. C. Gordon and
               Robin Milner and
               Christopher P. Wadsworth},
  title     = {Edinburgh LCF},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {78},
  year      = {1979},
  isbn      = {3-540-09724-4},
  ee        = {https://doi.org/10.1007/3-540-09724-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{LDMcK06,
  author =       "{St\'ephane} Lengrand and Roy Dyckhoff and James
                  McKinna",
  title =        "A sequent calculus for {Pure Type Systems}",
  booktitle =    "Proceedings of the 15th Annual Conference of the
                  European Association for Computer Science Logic
                  (CSL'06)",
  editor =       "Zoltan Esik",
  publisher =    "Springer-Verlag",
  series =       "LNCS",
  volume =       4207,
  month =        sep,
  year =         2006,
  place =        "Szeged, Hungary",
  pages =        "441--455",
}

@book{Landau1930, 
   author = {Landau, Edmund}, 
   title = {{Grundlagen der Analysis}}, 
   publisher = {Akademische Verlagsgesellschaft}, 
   year = 1930, 
   address = {Leipzig}, 
   URL = {http://www.fernuni-hagen.de/imperia/md/content/ausstellung/juedischemathematiker/landau.pdf, http://books.google.de/books?id=SM3CS-VguyQC, http://de.scribd.com/doc/2452802/Landau-Edmund-Grundlagen-der-Analysis}, 
   quality = 5}

@book{Landau30,
  author =	 "Landau, E.",
  title =	 "Grundlagen der Analysis",
  publisher =	 "Leizig",
  year =	 1930
}

@Misc{LapPol:hofglis02,
  author =       "Shalom Lappin and Carl Pollard",
  title =        "A Higher-Order Fine-Grained Logic for Intensional
                  Semantics",
  howpublished = "Manuscript",
  year =         2002,
}

@Misc{LapPol:shs00,
  author =       "Shalom Lappin and Carl Pollard",
  title =        "Strategies for Hyperintensional Semantics",
  howpublished = "Manuscript, King's College, London and Ohio State
                  University",
  year =         2000,
}

@Book{LarSeg:kom95,
  author =       "Richard Larson and Gabriel Segal",
  title =        "Knowledge of Meaning",
  publisher =    "MIT Press",
  year =         1995,
  address =      "Cambridge Ma",
}

@PhdThesis{Lego94,
  author = 	 {R. Pollack},
  title = 	 {The Theory of LEGO},
  school = 	 {University of Ediburgh},
  year = 	 1994}

@article{McDowellM02,
  author    = {Raymond McDowell and
               Dale Miller},
  title     = {Reasoning with higher-order abstract syntax in a logical
               framework},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {3},
  number    = {1},
  year      = {2002},
  pages     = {80-136},
  ee        = {http://doi.acm.org/10.1145/504077.504080},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{MengP08,
  author    = {Jia Meng and
               Lawrence C. Paulson},
  title     = {Translating Higher-Order Clauses to First-Order Clauses},
  journal   = {J. Autom. Reasoning},
  volume    = {40},
  number    = {1},
  year      = {2008},
  pages     = {35-60},
  ee        = {https://doi.org/10.1007/s10817-007-9085-y},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Miller:alplwl91,
  author =       "Dale Miller",
  title =        "A Logic Programming Language with
                  Lambda-Abstraction, Function Variables, and Simple
                  Unification",
  journal =      "Journal of Logic and Computation",
  year =         1991,
  number =       1,
  volume =       4,
  pages =        "497--536",
}

@PhdThesis{Miller:pihol83,
  author =       "Dale Miller",
  school =       "Carnegie-Mellon University",
  title =        "Proofs in Higher-Order Logic",
  year =         1983,
}

@article{Mints99,
  author    = {Grigori Mints},
  title     = {Cut-Elimination for Simple Type Theory with An Axiom of
               Choice},
  journal   = {J. Symb. Log.},
  volume    = {64},
  number    = {2},
  year      = {1999},
  pages     = {479-485},
  ee        = {http://projecteuclid.org/euclid.jsl/1183745789},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{Mitchell96,
  author =       "John C. Mitchell",
  title =        "Foundations for Programming Languages",
  publisher =    "MIT Press",
  year =         1996,
  series =       "Foundations of Computing",
  location =     "Fachbereichsbibliothek Informatik",
  idnumber =     "M 12322",
  signature =    "MIT j 96:1 1.Ex",
  ISBN =         "0-262-13321-0",
  status =       "available",
  bibtype =      "BOOK",
}

@article{Muskens07,
  author    = {R.~Muskens},
  title     = {Intensional models for the theory of types},
  journal   = {J. Symb. Log.},
  volume    = {72},
  number    = {1},
  year      = {2007},
  pages     = {98-118},
  ee        = {http://projecteuclid.org/euclid.jsl/1174668386},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{NPW02,
  Author =       "Nipkow,T. and Paulson, L. and Wenzel, M.",
  Year =         2002,
  Title =        "{Isabelle/HOL: A Proof Assistant for Higher-Order
                  Logic}",
  Series =       "LNCS",
  Number =       2283,
  Publisher =    "Springer"
}

@TechReport{NadMil:holp94,
  author =       "Gopalan Nadathur and Dale Miller",
  title =        "Higher-Order Logic Programming",
  institution =  "Department of Computer Science, Duke University",
  year =         1994,
  type =         "Technical Report",
  number =       "CS-1994-38",
}

@InCollection{NadMil:holp98,
  author =       "Gopalan Nadathur and Dale Miller",
  title =        "Higher-Order Logic Programming",
  editor =       "Dov M. Gabbay and C. J. Hogger and J. A. Robinson",
  booktitle =    "Handbook of Logics for Artificial Intelligence and
                  Logic Programming",
  publisher =    "Clarendon Press, Oxford",
  volume =       5,
  pages =        "499--590",
  year =         1998,
}

@article{Nip89,
  author    = {Tobias Nipkow},
  title     = {Equational Reasoning in {Isabelle}},
  journal   = {Sci. Comput. Program.},
  volume    = {12},
  number    = {2},
  year      = {1989},
  pages     = {123-149},
  ee        = {https://doi.org/10.1016/0167-6423(89)90038-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{NipPauWen:iaphol02,
  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,
}

@InProceedings{OANTS,
  keywords =	 {Proof Assistants, OMEGA, Interactive Proof,
                  Automated Reasoning, System Integration, Agents, LEO
                  Prover},
  author =	 {Christoph Benzm{\"u}ller and Volker Sorge},
  title =	 {{OANTS} -- An open approach at combining Interactive
                  and Automated Theorem Proving},
  booktitle =	 {Symbolic Computation and Automated Reasoning},
  editor =	 {Manfred Kerber and Michael Kohlhase},
  year =	 2000,
  pages =	 {81-97},
  publisher =	 {A.K.Peters},
  URL =		 {http://christoph-benzmueller.de/papers/C8.pdf},
  abstract =	 {We present the O-ANTS theorem prover that is built
                  on top of an agent-based command suggestion
                  mechanism. The theorem prover inherits beneficial
                  properties from the underlying suggestion mechanism
                  such as run-time extendibility and resource
                  adaptability. Moreover, it supports the distributed
                  integration of external reasoning systems. We also
                  discuss how the implementation and modeling of a
                  calculus in our agent-based approach can be
                  investigated wrt. the inheritance of properties such
                  as completeness and soundness.},
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2000-calculemus-oants.pdf
                  " target="_blank">slides</a>},
}

@InProceedings{ORS92,
    Author       = "Owre, S. and Rushby, J.M. and Shankar, N",
    Year         = "1992",
    Title        = "{PVS: A Prototype Verification System}",
    Editor       = "Kapur D.",
    BookTitle    = "{Proceedings of the 11th International Conference on
                    Automated Deduction}",
    Place        = "Saratoga Springs, USA",
    Series       = "LNAI",
    Number       = "607",
    Pages        = "748-752",
    Publisher    = "Springer"
}

@Article{Orevkov79,
  author =       "V. P. Orevkov",
  title =        "Lower bounds for lengthening of proofs after
                  cut-elimination",
  journal =      "Zapiski Nauchnykh Seminarov LOMI",
  year =         1979,
  volume =       88,
  pages =        "137--162",
  note =         "English translation in: \cite{Orevkov79e}",
}

@Article{Orevkov79e,
  author =       "V. P. Orevkov",
  title =        "Lower bounds for lengthening of proofs after
                  cut-elimination",
  journal =      "J. Soviet Mathematics",
  year =         1982,
  volume =       20,
  pages =        "2337--2350",
}

@inproceedings{OysterClam1990,
  author    = {Alan Bundy and
               Frank van Harmelen and
               Christian Horn and
               Alan Smaill},
  title     = {The {Oyster-Clam} System},
  pages     = {647-648},
  editor    = {Mark E. Stickel},
  booktitle     = {10th International Conference on Automated Deduction, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {449},
  year      = {1990},
  isbn      = {3-540-52885-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{PN94,
  author    = {Lawrence C. Paulson},
  title     = {Isabelle - A Generic Theorem Prover (with a contribution
               by T. Nipkow)},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {828},
  year      = {1994},
  isbn      = {3-540-58244-4},
  ee        = {https://doi.org/10.1007/BFb0030541},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{Pau99,
    author = {Lawrence C. Paulson},
    title = {A generic tableau prover and its integration with Isabelle},
    journal = {Journal of Universal Computer Science},
    year = {1999},
    volume = {5},
    pages = {51--60}
}

@Book{Paulson:iagtp94,
  author =       "Lawrence C. Paulson",
  title =        "Isabelle: {A} Generic Theorem Prover",
  publisher =    "Springer Verlag",
  series =       "LNCS",
  nuber =        828,
  year =         1994,
}

@Article{Prawitz68,
  author =       "Dag Prawitz",
  title =        "Hauptsatz for Higher Order Logic",
  journal =      "Journal of Symbolic Logic",
  volume =       33,
  year =         1968,
  pages =        "452--457",
}

@Book{Principia,
  author =       "Alfred North Whitehead and Bertrand Russell",
  title =        "Principia Mathematica, 3 vols",
  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.",
  year =         "1910, 1912, 1913",
}

@Book{Quine1940,
  author =       "W. V. O. Quine",
  title =        "Mathematical Logic",
  publisher =    "Harvard University Press",
  year =         1940,
  address =      "Boston, MA",
}

@ARTICLE{R54,
   author = {{Benzm{\"u}ller}, C. and {Woltzenlogel Paleo}, B.},
    title = "{Formalization, Mechanization and Automation of G{\"o}del's Proof of {God's} Existence}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1308.4526},
     year = 2013,
   adsurl = {http://adsabs.harvard.edu/abs/2013arXiv1308.4526B},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@InProceedings{Ramsey26,
  author =       "F. P. Ramsey",
  title =        "The foundations of mathematics",
  booktitle =    "Proceedings of the London Mathematical Society",
  pages =        "338--384",
  year =         1926,
  volume =       25,
  series =       2,
}

@InCollection{Robinson69,
  author =       "J. A. Robinson",
  title =        "Mechanizing Higher-Order Logic",
  booktitle =    "Machine Intelligence 4",
  publisher =    "Edinburgh University Press",
  year =         1969,
  pages =        "151--170",
}

@InCollection{Robinson70,
  author =       "J. A. Robinson",
  title =        "A Note on Mechanizing Higher Order Logic",
  booktitle =    "Machine Intelligence 5",
  publisher =    "Edinburgh University Press",
  year =         1970,
  pages =        "121--135",
}

@Book{RobinsonVoronkov2001,
  author =       "J. Alan Robinson and Andrei Voronkov",
  title =        "Handbook of Automated Reasoning",
  publisher =    "MIT Press",
  year =         2001,
  location =     "Fachbereichsbibliothek Informatik",
  idnumber =     "M 15558",
  signature =    "ROB a 01:1 1.Ex",
  ISBN =         "0-262-18221-1",
  status =       "borrowed",
  bibtype =      "BOOK",
}

@Book{Russell03,
  author =       "Bertrand Russell",
  title =        "The principles of mathematics",
  publisher =    "Cambridge University Press, Cambridge, England",
  year =         1903,
}

@Article{Russell08,
  author =       "Bertrand Russell",
  title =        "Mathematical Logic as Based on the Theory of Types",
  journal =      "American Journal of Mathematics",
  volume =       30,
  year =         1908,
  pages =        "222--262",
}

@Misc{Russell1902,
  author =       "Bertrand Russell",
  title =        "Letter to {Frege}",
  note =         "Translated in \cite{vanHeijenoort67}",
  year =         1902,
}

@InProceedings{SchMos:hisdfp02,
  author =       "L. Schr{\"o}der and T. Mossakowski",
  title =        "Has{CASL}: towards integrated specification and
                  development of functional programs",
  booktitle =    "Algebraic Methodology And Software Technology",
  series =       "LNCS",
  year =         2002,
  publisher =    "Springer",
  pubaddr =      "Berlin",
  volume =       2422,
  pages =        "99--116",
}

@Unpublished{Schroeder:hmpl02,
  author =       "Lutz Schr{\"o}der",
  title =        "Henkin Models for the Partial $\lambda$-Calculus",
  note =         "Manuscript,
                  cf.~\url{http://www.informatik.uni-bremen.de/~lschrode/hascasl/henkin.ps}",
  year =         2002,
}

@Article{Schuette60,
  author =       "Kurt Sch{\"u}tte",
  journal =      "Journal of Symbolic Logic",
  title =        "Semantical and Syntactical Properties of Simple Type
                  Theory",
  volume =       25,
  number =       4,
  year =         1960,
  pages =        "305--326",
}


@article{Schulz:AICOM-2002,
  title =	 {E -- A brainiac theorem prover},
  author =	 {S.~Schulz},
  journal =	 {{AI Communications}},
  volume =	 15,
  number =	 2,
  pages =	 {111--126},
  year =	 2002,
  publisher =	 {IOS Press}
}

@Article{Shapiro85,
  jstor_articletype ="research-article",
  title =        "Second-Order Languages and Mathematical Practice",
  author =       "Stewart Shapiro",
  journal =      "Journal of Symbolic Logic",
  volume =       50,
  number =       3,
  jstor_formatteddate ="Sep., 1985",
  pages =        "714--742",
  URL =          "http://www.jstor.org/stable/2274326",
  ISSN =         00224812,
  language =     "English",
  year =         1985,
  publisher =    "Association for Symbolic Logic",
  copyright =    "Copyright © 1985 Association for Symbolic Logic",
}


@Article{Smullyan63,
  title =        "A Unifying Principle for Quantification Theory",
  author =       "Raymond M. Smullyan",
  journal =      "Proc. Nat. Acad Sciences",
  volume =       49,
  pages =        "828--832",
  year =         1963,
}


@Book{Smullyan68,
  title =        "First-Order Logic",
  author =       "Raymond M. Smullyan",
  publisher =    "Springer",
  year =         1968,
}

@Article{StatmanBoundsForProof,
  author =       "R Statman",
  title =        "Bounds for proof-search and speed-up in the
                  predicate calculus",
  journal =      "Annals of Mathematical Logic",
  year =         1978,
  volume =       15,
  pages =        "225--287",
}

@Proceedings{TABLEAU95,
  title =        "Proceedings of Theorem Proving with Analytic
                  Tableaux and Related Methods",
  key =          "TABLEAU95",
  editor =       "Peter Baumgartner and Reiner H{\"a}hnle and Joachim
                  Posegga",
  number =       918,
  series =       "LNAI",
  booktitle =    "Theorem Proving with Analytic Tableaux and Related
                  Methods",
  year =         1995,
}


@InProceedings{TRAMP-1,
  author =       "Andreas Meier",
  title =        "System Description: {TRAMP}: Transformation of
                  Machine-Found Proofs into {ND}-Proofs at the
                  Assertion Level.",
  booktitle =    "CADE",
  year =         2000,
  pages =        "460--464",
  crossref =     "DBLP:conf/cade/2000",
  bibsource =    "DBLP, http://dblp.uni-trier.de",
}

@Article{Takahashi67,
  author =       "{Moto-o} Takahashi",
  title =        "A Proof of Cut-Elimination Theorem in Simple Type
                  Theory",
  journal =      "Journal of the Mathematical Society of Japan",
  volume =       19,
  year =         1967,
  pages =        "399--410",
}


@Article{Takahashi68,
  author =       "Moto-o Takahashi",
  journal =      "Journal of the Mathematical Society of Japan",
  title =        "Cut-Elimination in Simple Type Theory with
                  Extensionality",
  volume =       19,
  year =         1968,
}


@Article{Takeuti53,
  author =       "Gaisi Takeuti",
  title =        "On a Generalized Logic Calculus",
  journal =      "Japanese Journal of Mathematics",
  volume =       23,
  year =         1953,
  pages =        "39--96",
  note =         "Errata: ibid, vol.\ 24 (1954), 149--156",
}

@Article{Takeuti58,
  author =       "Gaisi Takeuti",
  title =        "Remark on the fundamental conjecture of {GLC}",
  journal =      "Journal of the Mathematical Society of Japan",
  volume =       10,
  year =         1958,
  pages =        "44--45",
}

@Article{Takeuti60,
  author =       "Gaisi Takeuti",
  title =        "An example on the fundamental conjecture of {GLC}",
  journal =      "Journal of the Mathematical Society of Japan",
  volume =       12,
  year =         1960,
  pages =        "238--242",
}

@Book{Takeuti75,
author = "Gaisi Takeuti",
title = "Proof Theory",
publisher = "Elsevier",
year = 1975,
volume = 81,
pages = "iii - ",
series = "Studies in Logic and the Foundations of Mathematics ",
issn = "0049-237X",
doi = "https://doi.org/10.1016/S0049-237X(08)70603-7",
url = "http://www.sciencedirect.com/science/article/pii/S0049237X08706037",
key = "tagkey1975iii"
}

@Book{Takeuti87,
  author =       "Gaisi Takeuti",
  publisher =    "North Holland",
  title =        "Proof Theory",
  year =         1987,
}

@article{TheoremProvingModulo2003,
  author    = {Gilles Dowek and
               Th{\'e}r{\`e}se Hardin and
               Claude Kirchner},
  title     = {Theorem Proving Modulo},
  journal   = {J. Autom. Reasoning},
  volume    = {31},
  number    = {1},
  year      = {2003},
  pages     = {33-72},
  ee        = {https://doi.org/10.1023/A:1027357912519},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Thomason:amtfpa80,
  author =       "R. Tomason",
  title =        "A Model Theory for Proposistional Attitudes",
  journal =      "Linguistics and Philosophy",
  year =         1980,
  volume =       4,
  pages =        "47--70",
}

@Book{TroelstraSchw00b,
  author =       "A. S. Troelstra and H. Schwichtenberg",
  title =        "Basic Proof Theory",
  edition =      2,
  publisher =    "Cambridge University Press",
  year =         2000,
}

@inproceedings{Twelf1999,
  author    = {Frank Pfenning and
               Carsten Sch{\"u}rmann},
  title     = {System Description: Twelf - A Meta-Logical Framework for
               Deductive Systems},
  pages     = {202-206},
  editor    = {Harald Ganzinger},
  booktitle     = {Automated Deduction - CADE-16, 16th International Conference
               on Automated Deduction, Trento, Italy, July 7-10, 1999,
               Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1632},
  year      = {1999},
  isbn      = {3-540-66222-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{W49,
  keywords =	 {Automated Reasoning, Ontology Reasoning, LEO Prover,
                  Higher Order Logic},
  author =	 {Christoph Benzm{\"u}ller and Marco Ziener},
  title =	 {Automated Consistency Checking of Expressive
                  Ontologies --- Beware of the Wrong Interpretation of
                  Success!},
  editor =	 {Michael Fink and Martin Homola and Alessandra Mileo
                  and Ivan Jose Varzinczak},
  booktitle =	 {Proceedings of ARCOE-LogIC 2013},
  address =	 {Corunna, Spain},
  year =	 2013,
  url =		 {http://christoph-benzmueller.de/papers/W49.pdf},
}
                  
@article{Wirth04,
  author    = {Claus-Peter Wirth},
  title     = {Descente Infinie + Deduction},
  journal   = {Logic Journal of the IGPL},
  volume    = {12},
  number    = {1},
  year      = {2004},
  pages     = {1-96},
  ee        = {https://doi.org/10.1093/jigpal/12.1.1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Wolfram:asflp94,
  author =       "David A. Wolfram",
  title =        "A semantics for $\lambda$-{PROLOG}",
  journal =      "Theoretical Computer Science",
  year =         1994,
  volume =       136,
  number =       1,
}

@Misc{agsyHOL,
  author = 	 {Fredrik Lindblad},
  title = 	 {{agsyHOL} website},
  howpublished = {\url{https://github.com/frelindb/agsyHOL}}}


@Article{andreoli92jlc,
  author =       "Jean-Marc Andreoli",
  title =        "Logic Programming with Focusing Proofs in Linear
                 Logic",
  journal =      jlc,
  volume =       "2",
  number =       "3",
  pages =        "297--347",
  year =         "1992",
}

@InCollection{andrewsSEP,
	author       =	{Andrews, P.B.},
	title        =	{Church's Type Theory},
	booktitle    =	{The Stanford Encyclopedia of Philosophy},
	editor       =	{E.N.~Zalta},
	howpublished =	{\url{http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/}},
	year         =	{2014},
	edition      =	{Spring 2014},
}


@InCollection{andrews09sep,
  author =       "P.B.~Andrews",
  title =        "Church's Type Theory",
  booktitle =    "The Stanford Encyclopedia of Philosophy",
  editor =       "Edward N. Zalta",
  publisher =    "Stanford University",
  howpublished =
                  "\url{http://plato.stanford.edu/archives/spr2009/entries/type-theory-church/}",
  year =         2009,
  edition =      "Spring 2009",
}


@Book{andrews65book,
  author =	 {P. B. Andrews},
  publisher =	 "North-Holland Publishing Company",
  title =	 "{A} {T}ransfinite {T}ype {T}heory with {T}ype
                  {V}ariables",
  year =	 1965,
  series =	 "Studies in Logic and the Foundations of Mathematics",
}


@Article{andrews:tatpsfctt96,
  author =       "Peter B. Andrews and Matthew Bishop and Sunil Issar
                  and Dan Nesmith and Frank Pfenning and Hongwei Xi",
  title =        "{TPS}: {A} Theorem Proving System for Classical Type
                  Theory",
  journal =      "J. Autom. Reasoning",
  year =         1996,
  volume =       16,
  number =       3,
  pages =        "321--353",
}


@Misc{arthan11:_proof_websit,
  author = 	 {Rob Arthan},
  title = 	 {ProofPower Website},
  howpublished = {\url{http://www.lemma-one.com/ProofPower/index/}},
  year = 	 2011}


@article{backes2011analytic,
  title =	 {Analytic tableaux for higher-order logic with
                  choice},
  author =	 {Backes, Julian and Brown, Chad Edward},
  journal =	 {J. Autom. Reasoning},
  volume =	 {47},
  number =	 {4},
  pages =	 {451--479},
  year =	 {2011},
  publisher =	 {Springer}
}


@Book{barendregt13book,
  author =       "Henk Barendregt and Wil Dekkers and Richard Statman",
  title =        "Lambda Calculus with Types",
  publisher =    "Cambridge University Press",
  year =         2013,
  series =       "Perspectives in Logic",
}





@InCollection{benl98ad,
  author =	 {H. Benl and U. Berger and H. Schwichtenberg and
                  M. Seisenberger and W. Zuber},
  title =	 {Proof theory at work: Program development in the
                  Minlog system},
  booktitle =	 {Automated Deduction},
  publisher =	 {Kluwer},
  year =	 1998,
  editor =	 {W. Bibel and P.H. Schmitt},
  volume =	 {II}
}



@inproceedings{blanchette11nitpicking,
  author    = {Jasmin Christian Blanchette and Tjark Weber and Mark Batty and Scott Owens and Susmit Sarkar},
  title     = {Nitpicking {C++} Concurrency},
  editor    = {Peter Schneider-Kamp and Michael Hanus},
  booktitle = {Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July~20-22, 2011, Odense, Denmark},
  pages     = {113--124},
  publisher = {ACM},
  OPTurl       = {http://doi.acm.org/10.1145/2003476.2003493},
  year      = 2011
}

<<<<<<< .mine



@InCollection{bledsoe79,
  author =       "W. W. Bledsoe",
  title =        "A Maximal Method for Set Variables in Automatic
                  Theorem-proving",
  booktitle =    "Machine Intelligence 9",
  editors =      "J. E. Hayes, Donald Michie, and L. I. Mikulich",
  publisher =    "John Wiley \&\ Sons",
  year =         1979,
  pages =        "53--100",
}


=======

>>>>>>> .r7843
@Article{boolos87jpl,
  author =       "George Boolos",
  title =        "A curious inference",
  journal =      "Journal of Philosophical Logic",
  year =         1987,
  volume =       16,
  pages =        "1--12",
}


@Book{boolos98:_logic_logic_logic,
  author =       "George Boolos",
  title =        "Logic, Logic, Logic",
  publisher =    "Harvard University Press",
  year =         1998,
}



@article{brown2012satallax,
  title =	 {Satallax: an automatic higher-order prover},
  author =	 {Brown, C.E.},
  journal =	 {J. Autom. Reasoning},
  pages =	 {111--117},
  year =	 2012,
  publisher =	 {Springer}
}

@Article{burel11lmcs,
  title =        "Efficiently Simulating Higher-Order Arithmetic by a
                  First-Order Theory Modulo",
  author =       "Guillaume Burel",
  journal =      "Logical Methods in Computer Science",
  year =         2011,
  pages =        "1--31",
  number =       1,
  volume =       7,
}


@Article{church32am,
  author =       "Alonzo Church",
  title =        "A Set of Postulates for the Foundation of Logic",
  journal =      "Annals of Mathematics",
  volume =       33,
  number =       2,
  pages =        "346--366",
  year =         1932,
}



@Article{church33am,
  author =       "Alonzo Church",
  title =        "A Set of Postulates for the Foundation of Logic
                  (Second Paper)",
  journal =      "Annals of Mathematics",
  volume =       34,
  number =       4,
  pages =        "839--864",
  year =         1933,
}


@Article{church36ajm,
  author =       "Alonzo Church",
  title =        "An unsolvable problem of elementary number theory",
  journal =      "American Journal of Mathematics",
  year =         1936,
  volume =       58,
  pages =        "354--363",
}


@InCollection{comon01handbook,
  title =	"Inductionless Induction",
  author =	"Hubert Comon",
  chapter =	"14",
  booktitle =	"Handbook of Automated Reasoning",
  publisher =	"Elsevier Science",
  editor =	"A. Robinson and A. Voronkov",
  year = 	"2001",
  volume =	"I",
  pages =	"913--962",
}


@InProceedings{cousineau07tlca,
  title =        "Embedding Pure Type Systems in the
                  Lambda-Pi-Calculus Modulo",
  author =       "Denis Cousineau and Gilles Dowek",
  booktitle =    "Typed Lambda Calculi and Applications, 8th
                  International Conference, {TLCA} 2007, Paris,
                  France, June 26-28, 2007, Proceedings",
  publisher =    "Springer",
  year =         2007,
  volume =       4583,
  editor =       "Simona Ronchi Della Rocca",
  pages =        "102--117",
  series =       lncs,
}

@Article{curry42jsl,
  author =       "Haskell Curry",
  title =        "The inconsistency of certain formal logics",
  journal =      "Journal of Symbolic Logic",
  year =         1942,
  volume =       7,
  pages =        "115--117",
}


@InCollection{dowek01handbook,
  title =        "Higher-order unification and matching",
  author =       "Gilles Dowek",
  chapter =      16,
  booktitle =    "Handbook of Automated Reasoning",
  publisher =    "Elsevier Science",
  address =      "New York",
  editor =       "A. Robinson and A. Voronkov",
  year =         2001,
  volume =       "II",
  pages =        "1009--1062",
}



@InCollection{dowek08andrews,
  author =       "Gilles Dowek",
  title =        "Skolemization in Simple Type Theory: the Logical and
                  the Theoretical Points of View",
  booktitle =    "Reasoning in Simple Type Theory: Festschrift in
                  Honor of Peter B. Andrews on His 70th Birthday",
  publisher =    "College Publications",
  editors =      "Christoph Benzm{\"u}ller and Chad E. Brown and
                  J{\"o}rg Siekmann and Richard Statman",
  year =         2008,
  series =       "Studies in Logic",
  number =       17,
  pages =        "244--255",
}


@InProceedings{dowek92lics,
  author =       "Gilles Dowek",
  title =        "Third Order Matching is Decidable",
  booktitle =    lics92,
  address =      "Santa Cruz, California",
  publisher =    "IEEE Computer Society Press",
  pages =        "2--10",
  month =        jun,
  year =         "1992",
}

@Article{dowek93jlc,
  author =       "Gilles Dowek",
  title =        "A complete proof synthesis method for the cube of
                  type systems",
  journal =      "Journal of Logic and Computation",
  year =         1993,
  volume =       3,
  number =       3,
  pages =        "287--315",
}

@InCollection{enderton12sep,
  author =       "Herbert B. Enderton",
  title =        "Second-order and Higher-order Logic",
  booktitle =    "The Stanford Encyclopedia of Philosophy",
  editor =       "Edward N. Zalta",
  howpublished =
                  "\url{http://plato.stanford.edu/archives/fall2012/entries/logic-higher-order/}",
  publisher =    "Stanford University",
  year =         2012,
  edition =      "Fall 2012",
}


@Book{enderton72,
  author = 	 {Hebert B. Enderton},
  title = 	 {A Mathematical Introduction to Logic},
  publisher = 	 {Academic Press},
  year = 	 1972}

@Article{farmer93:_imps,
  author = 	 {William M. Farmer},
  title = 	 {{IMPS}: An Interactive Mathematical Proof System},
  journal = 	 {J. 
Autom. Reasoning},
  year = 	 1993,
  volume = 	 11,
  pages = 	 {213-248}}
                  
@Article{felty00tcs,
  author =       "Amy Felty",
  title =        "The Calculus of Constructions as a Framework for
                  Proof Search with Set Variable Instantiation",
  journal =      "Theoretical Computer Science",
  year =         2000,
  volume =       232,
  number =       "1-2",
  pages =        "187--229",
  month =        feb,
}
                  
@Book{fitting02:_types_tableaus_god,
  author =       "Melvin Fitting",
  title =        "Types, Tableaus, and {G}{\"o}del's God",
  publisher =    "Kluwer",
  year =         2002,
}

@INPROCEEDINGS{gacek08ijcar,
  author = {Andrew Gacek},
  title = {The {A}bella Interactive Theorem Prover (System
                  Description)},
  year = 2008,
  month = {August},
  booktitle = {Proceedings of IJCAR 2008},
  pages = {154--161},
  publisher = {Springer},
  series = {LNCS},
  volume = 5195,
  editor = {A. Armando and P. Baumgartner and G. Dowek},
 URL =          "http://arxiv.org/abs/0803.2305",
  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek08ijcar-slides.pdf}
}

@Article{gacek12jar,
  author =       "Andrew Gacek and Dale Miller and Gopalan Nadathur",
  title =        "A two-level logic approach to reasoning about
                 computations",
  year =         "2012",
  URL =          "http://arxiv.org/abs/0911.2993",
  doi =          "10.1007/s10817-011-9218-1",
  journal =      jar,
  volume =       "49",
  number =       "2",
  pages =        "241--273",
  lixcategorie = "RI",
  lixequipe =    "Parsifal",
  x-pays =       "US",
}

@InCollection{gentzen35,
  author =       "Gerhard Gentzen",
  title =        "Investigations into Logical Deduction",
  booktitle =    "{The Collected Papers of Gerhard Gentzen}",
  editor =       "M. E. Szabo",
  publisher =    "North-Holland",
  address =      "Amsterdam",
  year =         "1969",
  pages =        "68--131",
  note =         "Translation of articles that appeared in 1934-35",
}


@InCollection{girard71sls,
  author =       "Jean-Yves Girard",
  title =        "Une extension de l'interpretation de {G{\"o}del}
                  {\`a} l'analyse, et son application {\`a}
                  l'{\'e}limination des coupures dans l'analyse et la
                  th{\'e}orie des types",
  publisher =    "North-Holland",
  address =      "Amsterdam",
  editor =       "J. E. Fenstad",
  booktitle =    "2nd Scandinavian Logic Symposium",
  year =         1971,
  pages =        "63--92",
}


@Article{girard86tcs,
  author =       "Jean-Yves Girard",
  title =        "The System {F} of Variable Types: Fifteen Years
                  Later",
  journal =      "Theoretical Computer Science",
  volume =       45,
  pages =        "159--192",
  year =         1986,
}

 @InProceedings{goedel36:_ueber_doe_laeng_von_beweis,
  author = 	 {Kurt G{\"o}del},
  title = 	 {{\"Uber die L\"ange von Beweisen}},
  booktitle = {{Ergebnisse eines Mathematischen Kolloquiums}},
  pages = 	 {23-24},
  year = 	 1936,
  note = 	 {English translation ``On the length of proofs'' in Kurt G\"odel: Collected Works, Volume 1, pages 396-399, Oxford University Press, 1986.}}

@InCollection{goedel36vol1,
  author =       "Kurt G{\"o}del",
  title =        "On the length of proofs",
  booktitle =    "Kurt G{\"o}del: Collected Works. Volume 1",
  pages =        "396--399",
  publisher =    "Oxford University Press",
  year =         1986,
  editor =       "S. Feferman and et al.",
}


@Article{goldfarb81tcs,
  author =       "Warren Goldfarb",
  title =        "The Undecidability of the Second-Order Unification
                  Problem",
  journal =      "Theoretical Computer Science",
  volume =       13,
  year =         1981,
  pages =        "225--230",
}


@TechReport{gould66tr,
  author =       "W. E. Gould",
  title =        "A Matching Procedure for $\omega$-Order Logic",
  institution =  "A F C R L",
  number =       "Scientific Report No. 4",
  year =         1966,
}


@InCollection{guard64tr,
  author =       "J. R. Guard",
  title =        "Automated logic for semi-automated mathematics",
  booktitle =    "Scientific Report No 1",
  year =         1964,
  pages =        "64--411",
  publisher =    "A F C R L",
}

@Article{huet73ic,
  author =       "G\'erard Huet",
  title =        "The Undecidability of Unification in Third Order
                  Logic",
  journal =      "Information and Control",
  volume =       22,
  pages =        "257--267",
  year =         1973,
}
                  
@Article{huet75tcs,
  author =       "G\'erard Huet",
  title =        "A Unification Algorithm for Typed
                  $\lambda$-Calculus",
  journal =      "Theoretical Computer Science",
  volume =       1,
  year =         1975,
  pages =        "27--57",
}


@Article{huet78,
  author =       "G\'erard Huet and Bernard Lang",
  title =        "Proving and Applying Program Transformations Expressed
                 with Second-Order Patterns",
  journal =      "Acta Informatica",
  volume =       "11",
  year =         "1978",
  pages =        "31--55",
}


@article{jensen76tcs,
  author =       {D. C. Jensen and Tomasz Pietrzykowski},
  title =        {Mechanizing {\it omega}-Order Type Theory Through
                  Unification},
  journal =      {Theor. Comput. Sci.},
  volume =       3,
  number =       2,
  year =         1976,
  pages =        {123-171},
  doi =          {https://doi.org/10.1016/0304-3975(76)90021-9},
}


@inproceedings{lambdaCLAM1998,
  author    = {Julian Richardson and
               Alan Smaill and
               Ian Green},
  title     = {System Description: Proof Planning in Higher-Order Logic
               with Lambda-{Clam}},
  pages     = {129-133},
  editor    = {Claude Kirchner and
               H{\'e}l{\`e}ne Kirchner},
  booktitle     = {Automated Deduction - CADE-15, 15th International Conference
               on Automated Deduction, Lindau, Germany, July 5-10, 1998,
               Proceedings},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1421},
  year      = {1998},
  isbn      = {3-540-64675-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InCollection{leivant94lailp,
  author =       "Daniel Leivant",
  booktitle =    "Handbook of Logic in Artificial Intelligence and
                  Logic Programming",
  title =        "Higher-order logic",
  publisher =    "Oxford University Press",
  year =         1994,
  editor =       "Dov M. Gabbay and C. J. Hogger and J. A. Robinson",
  pages =        "229--321",
  volume =       2,
}

@Article{liang05jar,
  author =       "Chuck Liang and Gopalan Nadathur and Xiaochu Qi",
  title =        "Choices in Representing and Reduction Strategies for
                 Lambda Terms in Intensional Contexts",
  journal =      "Journal of Automated Reasoning",
  year =         "2005",
  volume =       "33",
  pages =        "89--132",
}


@Article{liang09tcs,
  author =       "Chuck Liang and Dale Miller",
  title =        "Focusing and Polarization in Linear, Intuitionistic,
                 and Classical Logics",
  year =         "2009",
  journal =      "Theoretical Computer Science",
  publisher =    "Elsevier",
  volume =       "410",
  number =       "46",
  pages =        "4747--4768",
  lixcategorie = "RI",
  lixequipe =    "Parsifal",
  x-pays =       "US",
  aeres =        "Dummy Field",
  x-equipes =    "parsifal",
  x-type =       "article",
  x-support =    "revue",
  x-cle-support = "TCS",
  x-international-audience = "yes",
  x-editorial-board = "yes",
  doi =          "10.1016/j.tcs.2009.07.041",
}


@InProceedings{lncs711*84,
  author =       "F. Honsell and M. Lenisa",
  title =        "Some results on the full abstraction problem for
                  restricted lambda calculi",
  booktitle =    "Proceedings of Mathematical Foundations of Computer
                  Science (MFCS '93)",
  caddress =     "Gdansk, POL",
  editor =       "Andrzej M. Borzyszkowski and Stefan Sokolowski",
  publisher =    "Springer",
  pyear =        1993,
  cmonth =       "September",
  cyear =        1993,
  series =       "LNCS",
  volume =       711,
  pages =        "84--104",
  location =     "Fachbereichsbibliothek Informatik",
  signature =    "C 19 :18",
  crossref =     "lncs711",
  status =       "available",
  bibtype =      "INPROCEEDINGS",
}


@TechReport{lucchesi72tr,
  author =       "C. L. Lucchesi",
  title =        "The Undecidability of Unification for Third Order
                  Languages",
  institution =  "Dept of Applied Analysis and Computer Science,
                  University of Waterloo",
  number =       "Report CSRR 2059",
  year =         1972,
}

@InProceedings{martinlof82,
  author =       "Per Martin-L{\"{o}}f",
  title =        "Constructive Mathematics and Computer Programming",
  booktitle =    "Sixth International Congress for Logic, Methodology,
                 and Philosophy of Science",
  pages =        "153--175",
  publisher =    "North-Holland",
  address =      "Amsterdam",
  year =         "1982",
}


@InProceedings{miller11cpp,
  author =       "Dale Miller",
  title =        "A proposal for broad spectrum proof certificates",
  booktitle =    "CPP: First International Conference on Certified
                  Programs and Proofs",
  year =         2011,
  editor =       "J.-P. Jouannaud and Z. Shao",
  series =       lncs,
  volume =       7086,
  pages =        "54--69",
}


@Book{miller12proghol,
  author =       "Dale Miller and Gopalan Nadathur",
  title =        "Programming with Higher-Order Logic",
  publisher =    "Cambridge University Press",
  year =         2012,
  month =        jun,
  doi =          "10.1017/CBO9781139021326",
  lixcategorie = "OUV",
  lixequipe =    "Parsifal",
  aeres =        "Dummy Field",
  x-equipes =    "parsifal EXT",
  x-type =       "livre",
  x-editorial-board ="no",
  x-proceedings ="no",
  x-international-audience ="yes",
  x-invited-conference ="no",
  x-scientific-popularization ="yes",
}


@InProceedings{miller82,
  author =       "Dale A. Miller and Eve Longini Cohen and Peter B.
                  Andrews",
  title =        "A Look at {TPS}",
  booktitle =    "Sixth Conference on Automated Deduction",
  address =      "New York",
  publisher =    "Springer",
  year =         1982,
  editor =       "Donald W. Loveland",
  series =       lncs,
  volume =       138,
  pages =        "50--69",
}

@Article{miller87sl,
  author =       "Dale Miller",
  title =        "A Compact Representation of Proofs",
  journal =      "Studia Logica",
  volume =       "46",
  number =       "4",
  pages =        "347--370",
  year =         "1987",
}


@InCollection{miller92encyclopedia,
  author =       "Dale Miller",
  title =        "Logic, Higher-order",
  booktitle =    "Second Edition of the Encyclopedia of Artificial
                  Intelligence",
  publisher =    "Wiley",
  year =         1992,
  editor =       "S. Shapiro",
}


@Article{miller92jsc,
  author =       "Dale Miller",
  title =        "Unification under a mixed prefix",
  year =         1992,
  journal =      "Journal of Symbolic Computation",
  pages =        "321--358",
  volume =       14,
  number =       4,
  pdf =
                  "http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jsc92.pdf",
}

@InCollection{moore.history,
  author =	 {J. Strother Moore and Claus-Peter Wirth},
  editor =	 {J\"org Seikmann and Dov Gabbay and John Woods},
  title =	 "Automation of Mathematical Induction",
  booktitle =	 {History of Logic and Computation in the 20th
                  Century},
  publisher =	 {Elsevier},
  year =	 {this volume},
  volume =	 9
}


@InProceedings{nadathur05iclp,
  author =       "Gopalan Nadathur and Natalie Linnell",
  title =        "Practical Higher-Order Pattern Unification With
                 On-the-Fly Raising",
  editors =      "Maurizio Gabbrielli and Gopal Gupta",
  booktitle =    "{ICLP 2005: 21st International Logic Programming
                 Conference}",
  address =      "Sitges, Spain",
  publisher =    "Springer",
  series =       lncs,
  volume =       "3668",
  pages =        "371--386",
  month =        oct,
  year =         "2005",
  lixequipe =    "Slimmer",
}


@InProceedings{nadathur88iclp,
  author =       "Gopalan Nadathur and Dale Miller",
  title =        "An {Overview} of {$\lambda$Prolog}",
  editors =      "Kenneth A. Bowen and Robert A. Kowalski",
  booktitle =    "{Fifth International Logic Programming Conference}",
  address =      "Seattle",
  publisher =    "MIT Press",
  pages =        "810--827",
  month =        aug,
  year =         1988,
  URL =
                  "http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp88.pdf",
}


@Article{padovani00mscs,
  title =	"Decidability of fourth-order matching",
  author =	"Vincent Padovani",
  journal =	"Mathematical Structures in Computer Science",
  year = 	2000,
  number =	3,
  volume =	10,
  bibdate =	"2011-06-10",
  pages =	"361--372",
}

@Article{parikh73tacm,
  author =       "R. J. Parikh",
  title =        "Some results on the length of proofs",
  journal =      "Transactions of the ACM",
  year =         1973,
  volume =       177,
  pages =        "29--36",
}


@Article{paulson89jar,
  author =       "Lawrence C. Paulson",
  title =        "The Foundation of a Generic Theorem Prover",
  journal =      "Journal of Automated Reasoning",
  month =        sep,
  year =         1989,
  volume =       5,
  pages =        "363--397",
}

@PhdThesis{pfenning87:_proof_trans_in_higher_order_logic,
  author =       "Frank Pfenning",
  title =        "Proof Transformations in Higher-Order Logic",
  school =       "Carnegie Mellon University",
  year =         1987,
}

@InProceedings{pfenning99cade,
  author =       "Frank Pfenning and Carsten Sch{\"u}rmann",
  title =        "System Description: Twelf --- {A} Meta-Logical
                  Framework for Deductive Systems",
  editor =       "H. Ganzinger",
  pages =        "202--206",
  booktitle =    cade99,
  year =         1999,
  publisher =    "Springer",
  series =       lnai,
  number =       1632,
  address =      "Trento",
}



@InProceedings{pietrzykowski72acmconf,
  author =       "T. Pietrzykowski and D. C. Jensen",
  title =        "A complete mechanization of $\omega$-order type
                  theory",
  booktitle =    "ACM '72: Proceedings of the ACM annual conference",
  year =         1972,
  pages =        "82--92",
  publisher =    "ACM Press",
  address =      "New York, NY, USA",
  doi =          "http://doi.acm.org/10.1145/800193.805824",
}


@Article{pietrzykowski73jacm,
  author =       "Tomasz Pietrzykowski",
  title =        "A Complete Mechanization of Second-Order Type
                  Theory",
  journal =      "J. ACM",
  volume =       20,
  number =       2,
  year =         1973,
  ISSN =         "0004-5411",
  pages =        "333--364",
  doi =          "http://doi.acm.org/10.1145/321752.321764",
  publisher =    "ACM Press",
  address =      "New York, NY, USA",
}



@InProceedings{reynolds74cp,
  author =       "John C. Reynolds",
  title =        "Towards a Theory of Type Structure",
  booktitle =    "Colloque sur la Programmation, Paris, France",
  publisher =    "Springer",
  address =      "New York",
  series =       lncs,
  volume =       19,
  year =         1974,
  pages =        "408--425",
}



@InCollection{sep-generalized-quantifiers,
  author =       "Dag Westerst\r{a}hl",
  title =        "Generalized Quantifiers",
  booktitle =    "The Stanford Encyclopedia of Philosophy",
  editor =       "Edward N. Zalta",
  howpublished =
                  "\url{http://plato.stanford.edu/archives/sum2011/entries/generalized-quantifiers/}",
  year =         2011,
  edition =      "Summer 2011",
}


@InProceedings{siekmann02:_proof_devel_omega,
  author =       "J{\"o}rg Siekmann and Christoph Benzm{\"u}ller et
                  al.",
  title =        "Proof Development with {OMEGA}",
  editor =       "Andrei Voronkov",
  booktitle =    "Proceedings of the 18th International Conference on
                  Automated Deduction",
  year =         2002,
  pages =        "144--149",
  publisher =    "Springer",
  series =       "LNAI",
  number =       2392,
  address =      "Copenhagen, Denmark",
}


@Article{snyder89jsc,
  author =       "Wayne Snyder and Jean H. Gallier",
  title =        "Higher Order Unification Revisited: Complete Sets of
                  Transformations",
  journal =      "Journal of Symbolic Computation",
  volume =       8,
  number =       "1-2",
  pages =        "101--140",
  year =         1989,
}


@InProceedings{sprenger03fossacs,
  author =       "C. Spenger and M. Dams",
  title =        "On the Structure of Inductive Reasoning: Circular and
                 Tree-shaped Proofs in the $\mu$-Calculus",
  booktitle =    "FOSSACS'03",
  year =         "2003",
  editor =       "A.~Gordon",
  volume =       "2620",
  pages =        "425--440",
  series =       lncs,
  publisher =    "Springer",
}


@Article{stirling09lmcs,
  author =       "Colin Stirling",
  title =        "Decidability of Higher-Order Matching",
  journal =      lmcs,
  year =         "2009",
  volume =       "5",
  number =       "3",
  pages =        "1--52",
}


@article{sutcliffe2009tptp,
  title =	 {The {TPTP} problem library and associated
                  infrastructure},
  author =	 {Sutcliffe, G.},
  journal =	 {Journal of Automated Reasoning},
  volume =	 {43},
  number =	 {4},
  pages =	 {337--362},
  year =	 {2009},
  publisher =	 {Springer}
}


@Article{tait66bams,
  author =	 {William W. Tait},
  title =	 {A nonconstructive proof of {Gentzen's} {Hauptsatz} for
                  second order predicate logic},
  journal =	 {Bulletin of the American Mathematical Society},
  year =	 1966,
  volume =	 72,
  pages =	 {980--983}
}

@InProceedings{tps-cade-neu,
  author =       "Peter B. Andrews and Matthew Bishop and Chad E.
                  Brown",
  title =        "{TPS}: {A} Theorem Proving System for Type Theory",
  booktitle =    "Proceedings of the 17th International Conference on
                  Automated Deduction",
  editor =       "David McAllester",
  number =       1831,
  series =       "LNAI",
  year =         2000,
  publisher =    "Springer",
  address =      "Pittsburgh, USA",
  pages =        "164--169",
}

@Book{vanHeijenoort67,
  author =       "Jean van Heijenoort",
  title =        "From {F}rege to {G}{\"o}del: {A} Source Book in
                  Mathematics, 1879-1931",
  edition =      "3rd printing, 1997",
  publisher =    "Harvard Univ. Press",
  address =      "Cambridge, MA",
  year =         1967,
  series =       "Source books in the history of the sciences series",
  ISBN =         "0-674-32450-1",
}


@InProceedings{C37,
  keywords =	 {Higher Order Logic, LEO Prover, Semantic Embedding,
                  Conditional Logics, Combinations of Logics},
  author =	 {Christoph Benzm{\"u}ller},
  title =	 {Automating Quantified Conditional Logics in {HOL}},
  booktitle =	 {Proc. of IJCAI-23},
  address =	 {Beijing, China},
  editor =	 {Francesca Rossi},
  year =	 2013,
  url =		 {http://christoph-benzmueller.de/papers/C37.pdf},
  comment =	 {<a
                  href="http://christoph-benzmueller.de/papers/2013-IJCAI-Poster.pdf"
                  target="_blank " target="_blank">poster</a>},
}

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},
  year =	 2013,
  volume =	 7,
  number =	 1,
  pages =	 {7-20},
  doi =       {10.1007/s11787-012-0052-y},
  url =       {http://christoph-benzmueller.de/papers/J23.pdf},
}

@InCollection{Andrews00c,
	Author="Peter B. Andrews",
	Title="Classical Type Theory",
	Editor="Alan Robinson and Andrei Voronkov",
	BookTitle="Handbook of Automated Reasoning",
	Publisher="Elsevier Science",
        Address="Amsterdam",
        Chapter="15",
        Volume="2",
        Pages="965--1007",
	Year="2001"}


@Article{KleeneRosser34,
  author = 	 {S.C. Kleene and J.B. Rosser},
  title = 	 {The Inconsistency of Certain Formal Logics},
  journal = 	 {Annals of Mathematics},
  year = 	 1935,
  volume = 	 36,
  number = 	 3,
  pages = 	 {630-636}}



@article{AndrewsB06,
  author    = {P.B. Andrews and
               C.E. Brown},
  title     = {TPS: A hybrid automatic-interactive system for developing
               proofs},
  journal   = {J. Applied Logic},
  volume    = {4},
  number    = {4},
  year      = {2006},
  pages     = {367-395},
  ee        = {https://doi.org/10.1016/j.jal.2005.10.002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/sat/EenS03,
  author    = {Niklas E{\'e}n and
               Niklas S{\"o}rensson},
  title     = {An Extensible SAT-solver},
  year      = {2003},
  pages     = {502-518},
  editor    = {Enrico Giunchiglia and
               Armando Tacchella},
  booktitle     = {Theory and Applications of Satisfiability Testing, 6th International
               Conference, SAT 2003. Santa Margherita Ligure, Italy, May
               5-8, 2003 Selected Revised Papers},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {2919},
  year      = {2004},
  isbn      = {3-540-20851-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@PhdThesis(Bishop99a,
 Author="Matthew Bishop",
 Title="Mating Search Without Path Enumeration",
 School="Carnegie Mellon University",
 Year=1999,
 Month=apr,
)



@PhdThesis(Pfenning86,
 Author="Frank Pfenning",
 Title="Proof Transformations in Higher-Order Logic",
 School="Carnegie Mellon University",
 Year=1987,
 Note="156 pp.")
@InProceedings{andrews77:_theor_provin_in_type_theor,
  author = 	 {P.B. Andrews and E.L. Cohen},
  title = 	 {Theorem Proving in Type Theory},
  booktitle = {Proc. of IJCAI-77, 5th International Joint Conference on Artificial Intelligence},
  year = 	 1977}



@inproceedings{Nipkow93,
  author    = {Tobias Nipkow},
  title     = {Functional Unification of Higher-Order Patterns},
  year      = {1993},
  pages     = {64-74},
  booktitle     = {Proceedings of the Eighth Annual Symposium on Logic in Computer
               Science (LICS '93), Montreal, Canada, June 19-23, 1993},
  publisher = {IEEE Computer Society},
}


@Article{henkin63:_theor_of_propos_types,
  author = 	 {Leon Henkin},
  title = 	 {A theory of propositional types},
  journal = 	 {Fundamatae Mathematicae},
  year = 	 1963,
  number = 	 52,
  pages = 	 {323-344}}

@inproceedings{DBLP:conf/cade/FarmerGT92,
  author    = {William M. Farmer and
               Joshua D. Guttman and
               F. Javier Thayer},
  title     = {Little Theories},
  year      = {1992},
  pages     = {567-581},
  editor    = {Deepak Kapur},
  booktitle     = {Automated Deduction - CADE-11, 11th International Conference
               on Automated Deduction, Saratoga Springs, NY, USA, June
               15-18, 1992, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {607},
}


@InProceedings{Dedukti,
  author = 	 {Mathieu Boespflug and Quentin Carbonneaux and Olivier Hermant},
  title = 	 {The lambda-Pi-calculus Modulo as a Universal Proof Language},
  booktitle = {PxTP 2012},
  pages = 	 {28-43},
  year = 	 2012,
  editor = 	 {David Pichardie and Tjark Weber},
  volume = 	 878,
  publisher = {CEUR Workshop Proceedings}}

@Book{Gallin75,
  author = 	 {D. Gallin},
  title = 	 {Intensinonal and Higher-Order Modal Logic},
  publisher = 	 {N.-Holland},
  year = 	 {1975},
}

@incollection{homl,
  author = {Muskens, R.},
  title = {{Higher Order Modal Logic}},
  booktitle = {Handbook of Modal Logic},
  pages = {621--653},
  publisher = {Elsevier},
  year = {2006},
  editor = {Blackburn et al., P},
  OPTseries = {Studies in Logic and Practical Reasoning},
  address = {Dordrecht},
  pdf = {homl.pdf}
}

@book{HML,
 author = {Blackburn, Patrick and Benthem, Johan F. A. K. van and Wolter, Frank},
 title = {Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning)},
 year = {2006},
 isbn = {0444516905},
 publisher = {Elsevier Science Inc.},
 address = {New York, NY, USA},
} 


Article{J22,
  key =		 {J22},
  author =	 {G. Sutcliffe and C. Benzm{\"u}ller},
  title =	 {Automated Reasoning in Higher-Order Logic using the
                  {TPTP THF} Infrastructure.},
  journal =	 {Journal of Formalized Reasoning},
  volume =	 3,
  number =	 1,
  pages =	 {1-27},
  year =	 2010
}

@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},
  number =	 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}
}

@InProceedings{LEO-II,
  key =		 {C26},
  author =	 {C. Benzm{\"u}ller and F. Theiss and L.
                  Paulson and A. Fietzke},
  title =	 {{LEO-II} - A Cooperative Automatic Theorem Prover
                  for Higher-Order Logic},
  booktitle =	 {Proc.~of IJCAR 2008},
  url =		 {www.ags.uni-sb.de/~chris/papers/C26.pdf},
  publisher =	 {Springer},
  series =	 {LNAI},
  pages =	 {162-170},
  year =	 2008,
  number =	 5195
}

@CONFERENCE{Satallax,
  title = {Satallax: An Automated Higher-Order Prover},
  author = {C.E. Brown},
  year = {2012},
  publisher = {Springer},
  number = {7364}, 
  series = {LNAI},
  booktitle = {Proc. of IJCAR 2012},
  pages = {111 -- 117}
}

@Book{Isabelle,
  Author =	 "Nipkow, T. and Paulson, L.C. and Wenzel, M.",
  Year =	 2002,
  Title =	 "{Isabelle/HOL: A Proof Assistant for Higher-Order
                  Logic}",
  Series =	 "LNCS",
  Number =	 2283,
  Publisher =	 "Springer"
}




@INPROCEEDINGS{Hurd03first-orderproof,
    author = {Joe Hurd},
    title = {First-order proof tactics in higher-order logic theorem provers},
    booktitle = {Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports},
    year = {2003},
    pages = {56--68}
}

@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}
}

InCollection{B9,
  key =		 {B09},
  author =	 {C. Benzm{\"u}ller and L.C. Paulson},
  editor =       {Benzm{\"u}ller et al., C.},
  booktitle =	 {{Festschrift in Honor of {Peter B. Andrews} on His
                  70th Birthday}},
  title =	 {Exploring Properties of Normal Multimodal Logics in
                  Simple Type Theory with {LEO-II}},
  publisher =	 {College Publications},
  pages =	 {386-406},
  year =	 2008,
}

@book{Coq,
  author =	 {Bertot, Y. and Casteran, P.},
  publisher =	 {Springer},
  title =	 {{Interactive Theorem Proving and Program
                  Development}},
  year =	 2004
}


@url{FormalTheologyRepository,
  Author = {B. Woltzenlogel Paleo and C. Benzm\"uller},
  url = {https://github.com/FormalTheology/GoedelGod},
  Date-Added = {2013-08-17 06:52:50 +0200},
  Date-Modified = {2013-08-17 06:54:37 +0200},
  Lastchecked = {2013-08-17},
  Title = {Formal Theology Repository (\url{https://github.com/FormalTheology/GoedelGod})},
  Urldate = {2013-08-17}
}

@url{ContemporaryBibliography,
  Author = {R.~Corazzon},
  url = {http://www.ontology.co/biblio/ontological-proof-contemporary-biblio.htm},
  Date-Added = {2013-08-17 06:52:50 +0200},
  Date-Modified = {2013-08-17 06:54:37 +0200},
  Lastchecked = {2013-08-17},
  Title = {Contemporary~Bibliography~on~Ontological~Arguments:~\url{http://www.ontology.co/biblio/ontological-proof-contemporary-biblio.htm}},
  Urldate = {2013-08-17}
}

@InCollection{Goedel1970,
  author =	 {K. G\"odel},
  booktitle =	 {{Kurt G\"odel: Collected Works Vol. 3: Unpublished
                  Essays and Letters}},
  title =	 {Ontological Proof},
  publisher =	 {Oxford University Press},
  year =	 1970,
  comment =	 {first draft written in 1941, revised in 1970,
                  published in the collected works in 1995.}
}


@InCollection{Adams,
  author =	 {Adams, R.M.},
  booktitle =	 {{Kurt G\"odel: Collected Works Vol. 3: Unpubl.
                  Essays and Letters}},
  title =	 {Introductory Note to *1970},
  publisher =	 {Oxford Univ. Press},
  year =	 1995
}

@InCollection{Sobel,
  author =	 {Sobel, J.H.},
  booktitle =	 {{On Being and Saying. Essays for Richard
                  Cartwright}},
  title =	 {G\"odel's Ontological Proof},
  publisher =	 {{MIT Press}},
  pages =	 {241-261},
  year =	 1987,
}

@book{sobel2004logic,
  title =	 {Logic and Theism: Arguments for and Against Beliefs
                  in God},
  booktitle =	 {Logic and Theism: Arguments for and Against Beliefs
                  in God},
  author =	 {Sobel, J.H.},
  isbn =	 9781139449984,
  lccn =	 2002034954,
  url =		 {http://books.google.de/books?id=ZQh8QJOQdOQC},
  year =	 2004,
  publisher =	 {Cambridge U. Press}
}


@inBook{GoedelNotes,
  crossref =	 {sobel2004logic},
  author =	 {K.~G\"odel},
  title =	 {Appx.A: Notes in Kurt G\"odel's Hand},
  pages =	 {144-145},
}

@inBook{ScottNotes,
  crossref =	 {sobel2004logic},
  author =	 {D. Scott},
  title =	 {Appx.B: Notes in Dana Scott's Hand},
  pages =	 {145-146},
}

@InCollection{Scott,
  author =	 {D. Scott},
  booktitle =	 {{On Being and Saying. Essays for Richard
                  Cartwright}},
  title =	 {G\"odel's Ontological Proof},
  publisher =	 {{MIT Press}},
  pages =	 {257-258},
  year =	 1987,
}

@InCollection{AndersonGettings,
  author =	 {Anderson, A.C. and Gettings, M.},
  booktitle =	 {{G\"odel'96: Logical Foundations of Mathematics,
                  Computer Science, and Physics: Lecture Notes in
                  Logic 6}},
  title =	 {G\"odel Ontological Proof Revisited},
  publisher =	 {{Springer}},
  pages =	 {167-172},
  year =	 1996,
}

@Article{Hazen,
  author =	 {Hazen, A.P.},
  title =	 {On G\"odel's Ontological Proof},
  journal =	 {Australasian Journal of Philosophy},
  volume =	 76,
  pages =	 {361-377},
  year =	 1998
}

@book{Fitting,
  author =	 {M. Fitting},
  publisher =	 {Kluwer},
  title =	 {Types, Tableaus and G\"odel's God},
  year =	 2002
}

@InProceedings{C36,
  keywords =	 {Higher Order Logic, LEO Prover, Semantic Embedding,
                  Modal Logics, Combinations of Logics},
  author =	 {C.~Benzm{\"u}ller},
  title =	 {{HOL} based Universal Reasoning},
  booktitle =	 {Handbook of the 4th World Congress and School on
                  Universal Logic},
  address =	 {Rio de Janeiro, Brazil},
  editor =	 {Beziau et al., J.Y.},
  isbn =	 {978-85-400-0682-9},
  pages =	 {232-233},
  year =	 2013,
  url =		 {http://christoph-benzmueller.de/papers/C36.pdf},
  comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/2013-RIO.pdf
                  " target="_blank">slides</a>},
}




@Article{oppenheimera11,
  author = 	 {P.E.~Oppenheimera and E.N.~Zalta},
  title = 	 {A Computationally-Discovered Simplification of the Ontological Argument},
  journal = 	 {Australasian Journal of Philosophy},
  year = 	 2011,
  volume = 	 89,
  number = 	 2,
  pages = 	 {333-349}}



@InProceedings{rushby13,
  author = 	 {J.~Rushby},
  title = 	 {The Ontological Argument in {PVS}},
  booktitle = {Proc.~of CAV Workshop ``Fun With Formal Methods''},
  year = 	 2013,
  address = 	 {St. Petersburg, Russia,}}



@InCollection{B5,
  keywords =	 {Automated Reasoning, Higher Order Logic, History of Logic},
  author =	 {C.~Benzm{\"u}ller and D.~Miller},
  booktitle =	 {Handbook of the History of Logic, Volume 9 --- Logic and Computation},
  title =	 {Automation of Higher-Order Logic},
  OPTeditor =	 {J. Siekmann and D. Gabbay and J. Woods},
  publisher =	 {Elsevier},
  year = 2014,
  note = {Forthcoming; preliminary version available at {http://christoph-benzmueller.de/papers/B5.pdf}},
}


@InProceedings{W50,
    Author       = {C. Benzm\"uller and B. Woltzenlogel-Paleo},
    Year         = {2013},
    Title        = {G\"odel's {God} on the Computer},
    OPTEditor       = {Schulz, S. and Sutcliffe, G. and Konev, B.},
    BookTitle    = {Proceedings of the 10th International Workshop on the
                    Implementation of Logics},
    Place        = {Stellenbosch, South Africa},
    Series       = {EPiC Series},
    publisher    = {EasyChair},
    Note         = {Invited abstract},
    url = {http://christoph-benzmueller.de/papers/W50.pdf},
    comment =	 {<a
                  href="http://www.eprover.org/EVENTS/IWIL-2013.html"
                  target="_blank " target="_blank">event-website</a>},
}


@Article{J30,
  keywords =	 {Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, LEO Prover, Higher Order Logic},
  year =	 2013,
  author =	 {C. Benzm{\"u}ller and B. Woltzenlogel-Paleo},
  title =	 {Formalization, Mechanization and Automation of
                  {G{\"o}del's} Proof of {God's} Existence},
  journal =	 {arXiv:1308.4526},
  OPTcomment =	 {<a
                  href="https://github.com/FormalTheology/GoedelGod"
                  target="_blank">complete-formalisation</a>},
  OPTnote =	 {Preprint available as arXiv:1308.4526},
  url =		 {http://arxiv.org/abs/1308.4526},
}

@Article{J29,
 keywords =     {Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, LEO Prover, Higher Order Logic},
  author =	 {B. Woltzenlogel-Paleo and C. Benzm{\"u}ller},
  title =	 {Automated Verification and Reconstruction of {G\"odel's} Proof of {God's} Existence},
  journal =	 {OCG J.},
  year =	 2013,
}
 
@Article{J28,
  author    = {C. Benzm\"uller and B. Woltzenlogel-Paleo},
  title     = {{G{\"o}del's God in Isabelle/HOL}},
  journal   = {Archive of Formal Proofs},
  volume    = {2013},
  year      = {2013},
  url       = {https://isa-afp.org/entries/GoedelGod.shtml},
  ee        = {https://isa-afp.org/entries/GoedelGod.shtml},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Article{anderson90:_some_emend_of_goedel_ontol_proof,
  author = 	 {C.A.~Anderson},
  title = 	 {Some emendations of {G{\"o}del's} ontological proof},
  journal = 	 {Faith and Philosophy},
  year = 	 1990,
  volume = 	 7,
  number = 	 3}


@Article{garbacz12:_prover_simpl_expal_away,
  author = 	 {P.~Garbacz},
  title = 	 {{PROVER9's} simplifications explained away},
  journal = 	 {Australasian Journal of Philosophy},
  year = 	 2012,
  volume = 	 90,
  number = 	 3,
  pages = 	 {585-592}}



@InProceedings{ITP,
  author = 	 {C.~Benzm{\"u}ller and B.~Woltzenlogel Paleo},
  title = 	 {Modal Logic in {Coq} and {Scott’s} Version of {G{\"o}del’s} Proof of {God’s} Existence (Rough Diamond Proof Pearl)},
  note = 	 {Submitted to ITP'2014},
  year = 2014}


@Book{fitting98,
  author = 	 {M.~Fitting and R.L.~Mendelsohn},
  title = 	 {First-Order Modal Logic},
  series = {Synthese Library},
  volume = 277,
  publisher = 	 {Kluwer},
  year = 	 1998}


@book{DescriptionLogicHandbook,
 editor = {Baader, Franz and Calvanese, Diego and McGuinness, Deborah L. and Nardi, Daniele and Patel-Schneider, Peter F.},
 title = {The Description Logic Handbook: Theory, Implementation, and Applications},
 year = {2003},
 isbn = {0-521-78176-0},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
}


@inproceedings{MleanCoP,
  author    = {Jens Otten},
  title     = {MleanCoP: {A} Connection Prover for First-Order Modal Logic},
  booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 19-22, 2014. Proceedings},
  pages     = {269--276},
  year      = {2014},
  editor    = {St{\'{e}}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  series    = {Lecture Notes in Computer Science},
  volume    = {8562},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08587-6},
  doi       = {10.1007/978-3-319-08587-6},
  isbn      = {978-3-319-08586-9},
  timestamp = {Wed, 02 Jul 2014 14:02:31 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cade/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@Book{Labels,
  author = 	 {Dov M. Gabbay},
  title = 	 {Labelled Deductive Systems},
  publisher = 	 {Clarendon Press},
  year = 	 1996}

@article{HOLyHammer,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {HOL(y)Hammer: Online {ATP} Service for {HOL} Light},
  journal   = {Mathematics in Computer Science},
  volume    = {9},
  number    = {1},
  pages     = {5--22},
  year      = {2015},
  url       = {https://doi.org/10.1007/s11786-014-0182-0},
  doi       = {10.1007/s11786-014-0182-0},
  timestamp = {Mon, 09 Feb 2015 13:20:22 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/mics/KaliszykU15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@inproceedings{RathsOtten12,
  author    = {T. Raths and
               J. Otten},
  title     = {The {QMLTP} Problem Library for First-Order Modal Logics},
  pages     = {454-461},
  ee        = {https://doi.org/10.1007/978-3-642-31365-3_35},
  booktitle     = {Proc. of IJCAR 2012},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7364},
  year      = {2012},
  isbn      = {978-3-642-31364-6},
}


@incollection{Paulin, 
  author =  {C. Paulin-Mohring}, 
  title = {Introduction to the Calculus of Inductive Constructions}, 
  year = {2015},
  booktitle = {All about Proofs, Proofs for All}, 
  editor = {Delahaye, D. and Woltzenlogel Paleo, B.}, 
  publisher = {College Publications}, 
  address = {London}, 
  series = {Mathematical Logic and Foundations}, 
}


@article{HOLND,
  author    = {Christoph Benzm{\"{u}}ller and
               Chad E. Brown and
               Michael Kohlhase},
  title     = {Higher-order semantics and extensionality},
  journal   = {J. Symb. Log.},
  volume    = {69},
  number    = {4},
  pages     = {1027--1088},
  year      = {2004},
  url       = {https://doi.org/10.2178/jsl/1102022211},
  doi       = {10.2178/jsl/1102022211},
  timestamp = {Tue, 05 Aug 2014 16:36:16 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jsyml/BenzmullerBK04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@misc{ModalND,
  author = {Siders, A. and Woltzenlogel Paleo, B.},
  title = {A Variant of {G\"odel's} Ontological Proof in a Natural Deduction Calculus},
  note = {(\url{github.com/FormalTheology/GoedelGod/blob/master/Papers/InProgress/NaturalDeduction/GodProof-ND.pdf?raw=true}) },
  url = {https://github.com/FormalTheology/GoedelGod/blob/master/Papers/InProgress/NaturalDeduction/GodProof-ND.pdf?raw=true}
}


@inproceedings{DBLP:conf/ijcai/McCarthy93,
  author    = {John McCarthy},
  title     = {Notes on Formalizing Context},
  booktitle = {Proceedings of IJCAI'93},
  year      = 1993,
  pages     = {555-562},
  ee        = {http://www-formal.stanford.edu/jmc/context3/context3.html},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Article{bucav95:_metam_of_contex,
  author = 	 {S. Bucav and V. Buvac and I.A. Mason},
  title = 	 {Metamathematics
of Contexts},
  journal = 	 {Fundamenta Informaticae},
  year = 	 1995,
  volume = 	 23,
  number = 	 3,
  pages = 	 {263-301}}




@PhdThesis{guha91:_contex,
  author = 	 {R. V. Guha},
  title = 	 {Context: A Formalization and Some Applications},
  school = 	 {Stanford University},
  year = 	 1991}






@Article{giunchiglia94:_multil_hierar_logic_or,
  author = 	 {F. Giunchiglia and L. Serafini},
  title = 	 {Multilanguage
Hierarchical Logics or: How We Can Do without Modal Logics.},
  journal = 	 {Artificial Intelligence},
  year = 	 1994,
  volume = 	 65,
  number = 	 1,
  pages = 	 {29--70}}



@article{PeaseEtAl09,
 author = {Pease, Adam and Sutcliffe, Geoff and Siegel, Nick and Trac, Steven},
 title = {Large theory reasoning with {SUMO} at {CASC}},
 journal = {AI Communications},
 volume = 23,
 number = {2-3},
 year = 2010,
 issn = {0921-7126},
 pages = {137--144},
 publisher = {IOS Press},
 address = {Amsterdam, The Netherlands, The Netherlands},
 }


@inproceedings{DBLP:conf/cade/HoderV11,
  author    = {Krystof Hoder and
               Andrei Voronkov},
  title     = {Sine Qua Non for Large Theory Reasoning},
  year      = {2011},
  pages     = {299-314},
  ee        = {https://doi.org/10.1007/978-3-642-22438-6_23},
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie-Stokkermans},
  booktitle     = {Automated Deduction - CADE-23 - 23rd International Conference
               on Automated Deduction, Wroclaw, Poland, July 31 - August
               5, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6803},
  year      = {2011}
}


@article{PremiseSelection,
year={2014},
issn={0168-7433},
journal={Journal of Automated Reasoning},
volume={52},
number={2},
doi={10.1007/s10817-013-9286-5},
title={Premise Selection for Mathematics by Corpus Analysis and Kernel Methods},
url={https://doi.org/10.1007/s10817-013-9286-5},
publisher={Springer Netherlands},
keywords={Automated reasoning in large theories; Machine learning; Premise selection; Automated theorem proving},
author={Alama, Jesse and Heskes, Tom and Kühlwein, Daniel and Tsivtsivadze, Evgeni and Urban, Josef},
pages={191-213},
language={English}
}


@article{LearningPremiseSelection,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Learning-assisted theorem proving with millions of lemmas},
  journal   = {J. Symb. Comput.},
  volume    = {69},
  pages     = {109--128},
  year      = {2015},
  url       = {https://doi.org/10.1016/j.jsc.2014.09.032},
  doi       = {10.1016/j.jsc.2014.09.032},
  timestamp = {Mon, 19 Jan 2015 10:22:37 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jsc/KaliszykU15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@Article{mccarthy87:_gener_in_artif_intel,
  author = 	 {John McCarthy},
  title = 	 {Generality in Artificial Intelligence},
  journal = 	 {Communications of the ACM},
  year = 	 1987,
  volume = 	 30,
  number = 	 12,
  pages = 	 {1030-1035}}


@Article{giunchiglia93:_contex_reason,
  author = 	 {F. Giunchiglia},
  title = 	 {Contextual Reasoning},
  journal = 	 {Epistemologia (Special Issue on Languages and Machines)},
  year = 	 1993,
  volume = 	 16,
  pages = 	 {345--364}}



@Article{akman96:_steps_towar_formal_contex,
  author = 	 {V. Akman and M. Surav},
  title = 	 {Steps toward Formalizing Context},
  journal = 	 {AI Magazine},
  year = 	 1996,
  volume = 	 17,
  number = 	 3}




@article{Serafini:2004:CFT:992861.992863,
 author = {Serafini, Luciano and Bouquet, Paolo},
 title = {Comparing formal theories of context in {AI}},
 journal = {Artificial Intelligence},
 volume = {155},
 issue = {1-2},
 month = {May},
 year = {2004},
 issn = {0004-3702},
 pages = {41--67},
 numpages = {27},
 acmid = {992863},
 publisher = {Elsevier Science Publishers Ltd.},
 address = {Essex, UK},
 keywords = {context, contextual reasoning, local models semantics, logic of context, multicontext systems, propositional logic of context},
}





@Book{SumoBook11,
  editor = 	 {Adam Pease},
  title = 	 {Ontology: A Practical Guide},
  publisher = 	 {Articulate Software Press, Angwin, CA 94508},
  year = 	 2011}



@InProceedings{ramachandran05:_first_order_resear,
  author = 	 {Ramachandran, Deepak and Reagan, Pace and Goolsbey, Keith},
  editor =       {Shvaiko P.},
  title = 	 {First-Orderized {ResearchCyc}: Expressivity and Efficiency in a Common-Sense Ontology},
  booktitle = {Papers from the AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications, Pittsburgh, Pennsylvania, USA, 2005},
  publisher = {Technical Report WS-05-01 published by The AAAI Press, Menlo Park, California},
  year = 	 {2005},
  month = {July},
}



@inproceedings{PeaseSutcliffe07,
  author    = {Adam Pease and
               Geoff Sutcliffe},
  title     = {First Order Reasoning on a Large Ontology},
  booktitle = {Proceedings of the CADE-21 Workshop on Empirically Successful
               Automated Reasoning in Large Theories (ESARLT)},
  year      = 2007,
  editor    = {G. Sutcliffe and
               J. Urban and
               S. Schulz},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = 257,
  ee        = {\url{http://ceur-ws.org/Vol-257/07_Pease.pdf}},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@InProceedings{C42,
  keywords =	 {Automated Reasoning, Interactive Proof, Ontology
                  Reasoning, LEO Prover, Higher Order Logic},
  author =	 {Christoph Benzm{\"u}ller},
  editor =	 {Jean-Yves Beziau et al.},
  title =	 {Gödel's Ontological Argument Revisited -- Findings from a Computer-supported Analysis (invited)},
  booktitle =	 {Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil},
  OPTpages =	 {},
  year =	 2015,
  OPTurl =		 {http://christoph-benzmueller.de/papers/C42.pdf},
  note =	 {To appear},
}






@Misc{SpecialIssueContext,
  OPTkey = 	 {},
  editor = 	 {Jos Lehmann and Ivan José Varzinczak and Alan Bundy},
  title = 	 {Web Semantics: Science, Services and Agents on the World Wide Web, Special issue on Reasoning with context in the Semantic Web, Volumes 12--13, Pages 1-160},
  OPThowpublished = {},
  OPTmonth = 	 {},
  year = 	 {2012},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@Article{boolos87,
  author = 	 {George Boolos},
  title = 	 {A curious inference.},
  journal = 	 {Journal of Philosophical Logic},
  year = 	 1987,
  volume = 	 16,
  pages = 	 {1--12}}



@Book{boolos98:_logic,
  author = 	 {George Boolos},
  title = 	 {Logic, logic, and logic.},
  publisher = 	 {Harvard University Press},
  year = 	 1998
}


@incollection{Checkerboard, 
year=1996,
OPTisbn={978-3-540-61208-7},
booktitle={Theorem Proving with Analytic Tableaux and Related Methods},
volume=1071,
series={Lecture Notes in Computer Science},
editor={Miglioli, P. and Moscato, U. and Mundici, D. and Ornaghi, M.},
doi={10.1007/3-540-61208-4_1},
title={On sets, types, fixed points, and checkerboards},
url={https://doi.org/10.1007/3-540-61208-4_1},
publisher={Springer Berlin Heidelberg},
author={Andrews, PeterB. and Bishop, Matthew},
pages={1-15},
language={English}
}




@Book{pease11:_ontol,
  author = 	 {Adam Pease},
  title = 	 {Ontology: A Practical Guide},
  publisher = 	 {Articulate Software Press},
  year = 	 2011,
  url = {http://www.adampease.org/OP/Book.html},
  isbn = {1-889455-10-5}}

@article{DBLP:journals/jar/AndrewsBINPX96,
  author    = {Peter B. Andrews and
               Matthew Bishop and
               Sunil Issar and
               Dan Nesmith and
               Frank Pfenning and
               Hongwei Xi},
  title     = {{TPS:} {A} Theorem-Proving System for Classical Type Theory},
  journal   = {J. Autom. Reasoning},
  volume    = {16},
  number    = {3},
  pages     = {321--353},
  year      = {1996},
  url       = {https://doi.org/10.1007/BF00252180},
  doi       = {10.1007/BF00252180},
  timestamp = {Thu, 19 May 2011 15:52:32 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jar/AndrewsBINPX96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}




@InCollection{andrews84:_autom_higher_order_logic,
 author = 	 {Peter B. Andrews and Dale A. Miller and Eve Longini Cohen and Frank Pfenning},
  title = 	 {Automating Higher-Order Logic},
  booktitle = 	 {Automated Theorem Proving: After 25 Years},
  pages = 	 {169-192},
  year = 	 1984,
  editor = 	 {W. W. Bledsoe and D. W. Loveland},
  volume = 	 29,
  series = 	 {Contemporary Mathematics series},
  publisher =    {American Mathematical Society},
}

@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},
}

@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},
	OPTIsbn = {978-3-319-42431-6},
	Keywords = {Automated Reasoning, Interactive Proof, Semantic Embedding, Higher Order Logic, Higher Order Modal Logic, Computational Metaphysics},
	OPTdoi = {10.1007/978-3-319-42432-3_6},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {An Object-Logic Explanation for the Inconsistency in {G\"odel's}
  Ontological Theory (Extended Abstract)},
	Url = {http://christoph-benzmueller.de/papers/C60.pdf},
	OPTVolume = {9725},
	Year = 2016,
        OPTPages = {43-50}}

@inproceedings{C65,
Author = {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 },
Keywords = {Automated Reasoning, Interactive Proof, Ontology
Reasoning, LEO Prover, Higher Order Logic, Computational Metaphysics},
Pages = 2,
Title = {The Computational Metaphysics Lecture Course at {Freie
Universit{\"a}t Berlin}},
Url = {http://christoph-benzmueller.de/papers/C65.pdf},
Year = 2017,
}

@article{R59,
	Author = {Christoph Benzm{\"u}ller},
	Keywords = {Higher Order Logic, Universal Reasoning, Rational Argumentation, Human-Machine Interaction},
	Title = {Universal Reasoning, Rational Argumentation and Human-Machine Interaction},
	Journal = {arXiv, \url{http://arxiv.org/abs/1703.09620}},
	Url = {http://arxiv.org/abs/1703.09620},
	Year = 2017}

@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" 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},
	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,
}