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