References of "Steen, Alexander 50031912"
     in
Bookmark and Share    
Full Text
See detailExtensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III
Steen, Alexander UL

Book published by AKA-Verlag (2018)

Detailed reference viewed: 72 (4 UL)
See detailGCAI-2018. 4th Global Conference on Artificial Intelligence
Lee, Daniel; Steen, Alexander UL; Walsh, Toby

Book published by EasyChair (2018)

Detailed reference viewed: 33 (4 UL)
Full Text
Peer Reviewed
See detailSystem Demonstration: The Higher-Order Prover Leo-III
Steen, Alexander UL; Benzmüller, Christoph UL

in CEUR Workshop Proceedings (2018), 2095

Detailed reference viewed: 31 (15 UL)
Full Text
Peer Reviewed
See detailThe Higher-Order Prover Leo-III
Steen, Alexander UL; Benzmüller, Christoph UL

in Automated Reasoning 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (2018)

Detailed reference viewed: 68 (3 UL)
Full Text
Peer Reviewed
See detailLeo-III Version 1.1 (System description)
Benzmüller, Christoph UL; Steen, Alexander UL; Wisniewski, Max

in IWIL Workshop and LPAR Short Presentations (2017, June 04)

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based ... [more ▼]

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers. Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use. [less ▲]

Detailed reference viewed: 82 (3 UL)
Full Text
Peer Reviewed
See detailGoing Polymorphic - TH1 Reasoning for Leo-III
Steen, Alexander UL; Wisniewski, Max; Benzmüller, Christoph UL

in IWIL Workshop and LPAR Short Presentations (2017, June 04)

While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and ... [more ▼]

While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL. To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP THF problems. [less ▲]

Detailed reference viewed: 71 (4 UL)
Full Text
Peer Reviewed
See detailCapability Discovery for Automated Reasoning Systems
Steen, Alexander UL; Wisniewski, Max; Schurr, Hans-Jörg et al

in IWIL Workshop and LPAR Short Presentations (2017, June 04)

Automated reasoning systems such as theorem provers often employ interaction or cooperation with further reasoning software. Whereas in most cases the concrete choice of cooperating software is, to some ... [more ▼]

Automated reasoning systems such as theorem provers often employ interaction or cooperation with further reasoning software. Whereas in most cases the concrete choice of cooperating software is, to some extent, irrelevant, these systems are nevertheless often rigid in practice due to compatibility issues. In order to support more flexible cooperation schemes, a machine-readable description format for automated reasoning systems' capabilities is proposed. Additionally, a simple HTTP-based protocol for system and capability discovery is outlined. Both the format and the protocol are designed to be simple, extensible and easy to use with none to minor modifications for existing reasoning systems. [less ▲]

Detailed reference viewed: 85 (2 UL)
Full Text
Peer Reviewed
See detailTheorem Provers for Every Normal Modal Logic
Gleißner, Tobias; Steen, Alexander UL; Benzmüller, Christoph UL

in Eiter, Thomas; Sands, David (Eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2017, May 04)

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used ... [more ▼]

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant the- orem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification for- mat as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined. By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate. [less ▲]

Detailed reference viewed: 93 (2 UL)
Full Text
Peer Reviewed
See detailThe Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument
Fuenmayor, David; Benzmüller, Christoph UL; Steen, Alexander UL et al

in The 2nd World Congress on Logic and Religion -- Book of Abstracts (2017)

Detailed reference viewed: 73 (2 UL)
Full Text
Peer Reviewed
See detailTPTP and Beyond: Representation of Quantified Non-Classical Logics
Wisniewski, Max; Steen, Alexander UL; Benzmüller, Christoph UL

in Benzmüller, Christoph; Otten, Jens (Eds.) ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics (2016, December)

Detailed reference viewed: 22 (0 UL)
Full Text
Peer Reviewed
See detailTutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL
Steen, Alexander UL; Wisniewski, Max; Benzmüller, Christoph UL

in Benzmüller, Christoph; Sutcliffe, Geoff; Rojas, Raul (Eds.) GCAI 2016, 2nd Global Conference on Artificial Intelligence (2016, September 29)

Detailed reference viewed: 36 (0 UL)
Full Text
Peer Reviewed
See detailTowards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers
Libal, Tomer UL; Steen, Alexander UL

in Urban, Josef; Fontaine, Pascal; Schulz, Stephan (Eds.) Practical Aspects of Automated Reasoning (2016, July)

Detailed reference viewed: 16 (1 UL)
Full Text
Peer Reviewed
See detailAgent-Based HOL Reasoning
Steen, Alexander UL; Wisniewski, Max; Benzmüller, Christoph UL

in Greuel, GM; Koch, T; Paule, P (Eds.) et al Mathematical Software -- ICMS 2016, 5th International Congress, Proceedings (2016, July)

Detailed reference viewed: 42 (0 UL)
Full Text
Peer Reviewed
See detailEffective Normalization Techniques for HOL
Wisniewski, Max; Steen, Alexander UL; Kern, Kim et al

in Olivetti, Nicola; Tiwari, Ashish (Eds.) Automated Reasoning --- 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 -- July 2, 2016, Proceedings (2016, June)

Detailed reference viewed: 38 (0 UL)
See detailLeo-III
Steen, Alexander UL; Wisniewski, Max; Benzmüller, Christoph UL

Software (2016)

Detailed reference viewed: 32 (4 UL)
Full Text
Peer Reviewed
See detailSweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
Steen, Alexander UL; Benzmüller, Christoph UL

in Logic and Logical Philosophy (2016), 25(4), 535-554

Detailed reference viewed: 29 (0 UL)
Full Text
Peer Reviewed
See detailEinsatz von Theorembeweisern in der Lehre
Wisniewski, Max; Steen, Alexander UL; Benzmüller, Christoph UL

in Schwill, Andreas; Lucke, Ulrike (Eds.) Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam (2016)

Detailed reference viewed: 17 (0 UL)
Full Text
Peer Reviewed
See detailEmbedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic
Wisniewski, Max; Steen, Alexander UL

in Benzmüller, Christpoh; Otten, Jens (Eds.) ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics (2015, December)

Detailed reference viewed: 17 (0 UL)
Full Text
Peer Reviewed
See detailThere Is No Best Beta-Normalization Strategy for Higher-Order Reasoners
Steen, Alexander UL; Benzmüller, Christoph UL

in Davis, Martin; Fehnker, Ansgar; McIver, Annabelle (Eds.) et al Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (2015, November)

Detailed reference viewed: 30 (0 UL)
Full Text
Peer Reviewed
See detailLeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners
Wisniewski, Max; Steen, Alexander UL; Benzmüller, Christoph UL

in Kerber, Manfred; Carette, Jacques; Kaliszyk, Cezary (Eds.) et al Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings (2015, June)

Detailed reference viewed: 29 (0 UL)