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,2177 +1,2171 @@
@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{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{LEO-II,
+ author = {Christoph Benzm{\"{u}}ller and
+ Lawrence C. Paulson and
+ Frank Theiss and
+ Arnaud Fietzke},
+ title = {{LEO-II} -- {A} Cooperative Automatic Theorem Prover for Classical
+ Higher-Order Logic (System Description)},
+ booktitle = {Proc. of {IJCAR} 2008},
+ series = {LNAI},
+ volume = {5195},
+ pages = {162--170},
+ publisher = {Springer},
+ year = {2008},
+ url = {https://doi.org/10.1007/978-3-540-71070-7\_14},
+ doi = {10.1007/978-3-540-71070-7\_14},
}
@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},
+ booktitle = {Proc. of {IJCAR} 2012},
pages = {111--117},
publisher = {Springer},
- series = {Lecture Notes in Computer Science},
+ series = {LNAI},
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},
+ booktitle = {Proc. of {ITP} 2010},
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}}
-
+@inproceedings{rushby,
+ title={The {Ontological Argument in PVS}},
+ author={Rushby, John},
+ booktitle={CAV Workshop ``Fun With Formal Methods'},
+ address = {St. Petersburg, Russia},
+ month = {July},
+ volume={13},
+ year={2013}
+}
@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
+}