\n \n \n
\n
\n\n \n \n \n \n News — 25th International Conference on Automated Deduction (CADE-25).\n \n \n\n\n \n Benzmüller, C., Steen, A., & Wisniewski, M.\n\n\n \n\n\n\n Technical Report 2015.\n
Künstliche Intelligenz 29(4):451-452; non-reviewed conference report\n\n
\n\n
\n\n
\n\n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@techreport{J34,\n Author =\t {Christoph Benzm{\\"u}ller and Alexander Steen and Max\n Wisniewski},\n Title =\t {News --- 25th International Conference on Automated\n Deduction (CADE-25)},\n doi =\t\t {10.1007/s13218-015-0402-z},\n Year =\t 2015,\n note =\t {K\\"unstliche Intelligenz 29(4):451-452; non-reviewed\n conference report},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners.\n \n \n\n\n \n Steen, A., & Benzmüller, C.\n\n\n \n\n\n\n In Davis, M., Fehnker, A., McIver, A., & Voronkov, A., editor(s),
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 9450, of
LNAI, pages 329-339, Suva, Fiji, 2015. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C51,\n Address =\t {Suva, Fiji},\n Author =\t {Alexander Steen and Christoph Benzm{\\"u}ller},\n Booktitle =\t {Logic for Programming, Artificial Intelligence, and\n Reasoning (LPAR)},\n Doi =\t\t {10.1007/978-3-662-48899-7_23},\n Editor =\t {M. Davis and A. Fehnker and A. McIver and\n A. Voronkov},\n Isbn =\t {978-3-662-48898-0},\n Keywords =\t {own, Higher Order Logic, Automated Reasoning, LEO\n Prover},\n Pages =\t {329-339},\n Publisher =\t {Springer},\n Series =\t {LNAI},\n Title =\t {There Is No Best Beta-Normalization Strategy for\n Higher-Order Reasoners},\n url_preprint = {http://christoph-benzmueller.de/papers/C51.pdf},\n Volume =\t 9450,\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic.\n \n \n\n\n \n Steen, A., & Benzmüller, C.\n\n\n \n\n\n\n In
7th International Conference Non-Classical Logic – Theory and Applications, Torun, Poland, 2015. \n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C49,\n Author =\t {Alexander Steen and Christoph Benzm{\\"u}ller},\n Booktitle =\t {7th International Conference Non-Classical Logic --\n Theory and Applications, Torun, Poland},\n Keywords =\t {own, Higher Order Logic, Semantic Embedding, Multi\n Valued Logics, Automated Reasoning},\n Title =\t {Sweet SIXTEEN: Automation via Embedding into\n Classical Higher-Order Logic},\n url_preprint = {http://christoph-benzmueller.de/papers/C49.pdf},\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n The Higher-Order Prover LEO-II.\n \n \n\n\n \n Benzmüller, C., Sultana, N., Paulson, L. C., & Theiss, F.\n\n\n \n\n\n\n
Journal of Automated Reasoning, 55(4): 389-404. 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{J30,\n Author =\t {Christoph Benzm{\\"u}ller and Nik Sultana and\n Paulson, Lawrence C. and Frank Theiss},\n Doi =\t\t {10.1007/s10817-015-9348-y},\n Journal =\t {Journal of Automated Reasoning},\n publisher =\t {Springer Netherlands},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic,\n DFG-2501-Selected},\n Number =\t 4,\n Pages =\t {389-404},\n Title =\t {The Higher-Order Prover {LEO-II}},\n url_preprint = {https://www.researchgate.net/publication/280986731},\n Volume =\t 55,\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Proofs and reconstructions.\n \n \n\n\n \n Sultana, N., Benzmüller, C., & Paulson, L. C.\n\n\n \n\n\n\n In Lutz, C., & Ranise, S., editor(s),
FroCoS 2015, volume 9322, of
LNAI, pages 256-271, Wroclaw, Poland, 2015. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C48,\n Address =\t {Wroclaw, Poland},\n Author =\t {Nik Sultana and Christoph Benzm{\\"u}ller and\n Paulson, Lawrence C.},\n Booktitle =\t {FroCoS 2015},\n Doi =\t\t {10.1007/978-3-319-24246-0_16},\n Editor =\t {Carsten Lutz and Silvio Ranise},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic},\n Pages =\t {256-271},\n Publisher =\t {Springer},\n Series =\t {LNAI},\n Title =\t {Proofs and reconstructions},\n url_preprint = {http://christoph-benzmueller.de/papers/C48.pdf},\n Volume =\t 9322,\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Systematic Verification of the Modal Logic Cube in Isabelle/HOL.\n \n \n\n\n \n Benzmüller, C., Claus, M., & Sultana, N.\n\n\n \n\n\n\n In Kaliszyk, C., & Paskevich, A., editor(s),
PxTP 2015, volume 186, pages 27-41, Berlin, Germany, 2015. EPTCS\n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C47,\n Address =\t {Berlin, Germany},\n Author =\t {Christoph Benzm{\\"u}ller and Maximilian Claus and\n Nik Sultana},\n Booktitle =\t {PxTP 2015},\n Comment =\t {<a href="http://christoph-benzmueller.de/papers/2015-PxTP.pdf">slides</a>},\n Doi =\t\t {10.4204/EPTCS.186.5},\n Editor =\t {Cezary Kaliszyk and Andrei Paskevich},\n Issn =\t {2075-2180},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic},\n Pages =\t {27-41},\n Publisher =\t {EPTCS},\n Title =\t {Systematic Verification of the Modal Logic Cube in\n {Isabelle/HOL}},\n url_preprint = {http://christoph-benzmueller.de/papers/C47.pdf},\n Volume =\t 186,\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Higher-Order Modal Logics: Automation and Applications.\n \n \n\n\n \n Benzmüller, C., & Woltzenlogel Paleo, B.\n\n\n \n\n\n\n In Paschke, A., & Faber, W., editor(s),
Reasoning Web 2015, of
LNCS, pages 32-74, Berlin, Germany, 2015. Springer\n
(Invited paper)\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C46,\n Address =\t {Berlin, Germany},\n Author =\t {Christoph Benzm{\\"u}ller and Woltzenlogel Paleo,\n Bruno},\n Booktitle =\t {Reasoning Web 2015},\n Doi =\t\t {10.1007/978-3-319-21768-0_2},\n Editor =\t {Adrian Paschke and Wolfgang Faber},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic,\n Computational Metaphysics},\n Note =\t {(Invited paper)},\n Number =\t 9203,\n Pages =\t {32-74},\n Publisher =\t {Springer},\n Series =\t {LNCS},\n Title =\t {Higher-Order Modal Logics: Automation and\n Applications},\n url_preprint = {https://www.researchgate.net/publication/281677232},\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Interacting with Modal Logics in the Coq Proof Assistant.\n \n \n\n\n \n Benzmüller, C., & Woltzenlogel Paleo, B.\n\n\n \n\n\n\n In Beklemishev, L. D., & Musatov, D. V., editor(s),
Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings, volume 9139, of
LNCS, pages 398–411, 2015. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C44,\n Author =\t {Christoph Benzm{\\"{u}}ller and Woltzenlogel Paleo,\n Bruno},\n Booktitle =\t {Computer Science - Theory and Applications - 10th\n International Computer Science Symposium in Russia,\n {CSR} 2015, Listvyanka, Russia, July 13-17, 2015,\n Proceedings},\n Doi =\t\t {10.1007/978-3-319-20297-6_25},\n Editor =\t {Lev D. Beklemishev and Daniil V. Musatov},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic,\n Computational Metaphysics},\n Pages =\t {398--411},\n Publisher =\t {Springer},\n Series =\t {LNCS},\n Title =\t {Interacting with Modal Logics in the {Coq} Proof\n Assistant},\n url_preprint = {https://www.researchgate.net/publication/273201458},\n Volume =\t 9139,\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Gödel's Ontological Argument Revisited – Findings from a Computer-supported Analysis (invited).\n \n \n\n\n \n Benzmüller, C.\n\n\n \n\n\n\n In Silvestre, R. S., & Béziau, J., editor(s),
Handbook of the 1st World Congress on Logic and Religion, João Pessoa, Brazil, pages 13, 2015. \n
(Invited abstract)\n\n
\n\n
\n\n
\n\n \n \n Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C42,\n Author =\t {Christoph Benzm{\\"u}ller},\n Booktitle =\t {Handbook of the 1st World Congress on Logic and\n Religion, Jo\\~ao Pessoa, Brazil},\n Editor =\t {Ricardo Souza Silvestre and Jean-Yves B\\'eziau},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic,\n Computational Metaphysics},\n Note =\t {(Invited abstract)},\n Pages =\t 13,\n Title =\t {{G\\"{o}del's} Ontological Argument Revisited --\n Findings from a Computer-supported Analysis\n (invited)},\n Url =\n {http://christoph-benzmueller.de/papers/2015-handbook-logic-and-religion.pdf},\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy.\n \n \n\n\n \n Benzmüller, C., Weber, L., & Paleo, B. W.\n\n\n \n\n\n\n In Silvestre, R. S., & Béziau, J., editor(s),
Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brazil, pages 53-54, 2015. \n
(superseded by 2016 paper in Logica Universalis)\n\n
\n\n
\n\n
\n\n \n \n Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{C41,\n Author =\t {Christoph Benzm{\\"u}ller and Leon Weber and Bruno\n Woltzenlogel Paleo},\n Booktitle =\t {Handbook of the 1st World Congress on Logic and\n Religion, Joao Pessoa, Brazil},\n Editor =\t {Ricardo Souza Silvestre and Jean-Yves B\\'eziau},\n Keywords =\t {own, Automated Reasoning, Interactive Proof,\n Ontology Reasoning, LEO Prover, Higher Order Logic,\n Computational Metaphysics},\n Note =\t {(superseded by 2016 paper in Logica Universalis)},\n Pages =\t {53-54},\n Title =\t {Computer-Assisted Analysis of the\n {Anderson-H\\'{a}jek} Ontological Controversy},\n Url =\n {http://christoph-benzmueller.de/papers/2015-handbook-logic-and-religion.pdf},\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n On Logic Embeddings and Gödel's God.\n \n \n\n\n \n Benzmüller, C., & Woltzenlogel Paleo, B.\n\n\n \n\n\n\n In Codescu, M., Diaconescu, R., & Tutu, I., editor(s),
Recent Trends in Algebraic Development Techniques: 22nd International Workshop, WADT 2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers, of
LNCS, pages 3-6, Sinaia, Romania, 2015. Springer\n
(Invited paper)\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{W55,\n Address =\t {Sinaia, Romania},\n Author =\t {Christoph Benzm{\\"u}ller and Woltzenlogel Paleo,\n Bruno},\n Booktitle =\t {Recent Trends in Algebraic Development Techniques:\n 22nd International Workshop, WADT 2014, Sinaia,\n Romania, September 4-7, 2014, Revised Selected\n Papers},\n Doi =\t\t {10.1007/978-3-319-28114-8_1},\n Editor =\t {Codescu, Mihai and Diaconescu, Razvan and Tutu,\n Ionut},\n Isbn =\t {978-3-319-28114-8},\n Keywords =\t {own, Higher Order Logic, Semantic Embedding, Modal\n Logics, Automated Reasoning, Computational\n Metaphysics},\n Note =\t {(Invited paper)},\n Number =\t 9563,\n Pages =\t {3-6},\n Publisher =\t {Springer},\n Series =\t {LNCS},\n Title =\t {On Logic Embeddings and {G\\"odel's} {God}},\n url_preprint = {https://www.researchgate.net/publication/300112614},\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics.\n \n \n\n\n \n Benzmüller, C., & Otten, J.,\n editors.\n \n\n\n \n\n\n\n Volume 33, of EPiC Series in Computing.EasyChair. 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@proceedings{E14,\n Comment =\t {<a href="http://www.iltp.de/ARQNL-2014/">event-website</a>},\n Editor =\t {Christoph Benzm{\\"u}ller and Jens Otten},\n issn =\t {2398-7340},\n Pages =\t {1-86},\n Publisher =\t {EasyChair},\n Series =\t {EPiC Series in Computing},\n Title =\t {ARQNL 2014. Automated Reasoning in Quantified\n Non-Classical Logics},\n Url =\n {https://easychair.org/publications/volume/ARQNL_2014/},\n Volume =\t 33,\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n HOL Provers for First-order Modal Logics — Experiments.\n \n \n\n\n \n Benzmüller, C.\n\n\n \n\n\n\n In
Benzmüller, C., & Otten, J., editor(s),
ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics, volume 33, of
EPiC Series in Computing, pages 37-41, 2015. EasyChair\n
\n\n
\n\n
\n\n
\n\n \n \n Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{W54,\n Author =\t {Christoph Benzm{\\"u}ller},\n Booktitle =\t {ARQNL 2014. Automated Reasoning in Quantified\n Non-Classical Logics},\n Editor =\t {Christoph Benzm{\\"u}ller and Jens Otten},\n issn =\t {2398-7340},\n Keywords =\t {own, LEO Prover, Automated Reasoning, Proof\n Transformation, Higher Order Logic},\n Pages =\t {37-41},\n Publisher =\t {EasyChair},\n Series =\t {EPiC Series in Computing},\n Title =\t {{HOL} Provers for First-order Modal Logics ---\n Experiments},\n Url =\t\t {https://easychair.org/publications/paper/sdnL},\n Volume =\t 33,\n Year =\t 2015,\n Doi =\t\t {10.29007/przw},\n}\n\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n Higher-Order Automated Theorem Provers.\n \n \n\n\n \n Benzmüller, C.\n\n\n \n\n\n\n In Delahaye, D., & Woltzenlogel Paleo, B., editor(s),
All about Proofs, Proof for All, of Mathematical Logic and Foundations, pages 171-214. College Publications, London, UK, 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n preprint\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{B14,\n Address =\t {London, UK},\n Author =\t {Christoph Benzm{\\"u}ller},\n Booktitle =\t {All about Proofs, Proof for All},\n Comment =\t {<a href="http://www.collegepublications.co.uk/logic/mlf/?00023">publisher</a>},\n Editor =\t {David Delahaye and Woltzenlogel Paleo, Bruno},\n Isbn =\t {978-1-84890-166-7},\n Keywords =\t {own, Automated Reasoning, Higher Order Logic},\n Pages =\t {171-214},\n Publisher =\t {College Publications},\n Series =\t {Mathematical Logic and Foundations},\n Title =\t {Higher-Order Automated Theorem Provers},\n url_preprint = {http://christoph-benzmueller.de/papers/B14.pdf},\n Year =\t 2015,\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n