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

in KI – Künstliche Intelligenz (in press)

Detailed reference viewed: 26 (0 UL)
Full Text
Peer Reviewed
See detailProceedings of the Deduktionstreffen 2019
Schon, Claudia; Steen, Alexander UL

Scientific Conference (2019, September 23)

The annual meeting Deduktionstreffen is the prime activity of the Special Interest Group on Deduction Systems (FG DedSys) of the AI Section of the German Society for Informatics (GI-FBKI). It is a meeting ... [more ▼]

The annual meeting Deduktionstreffen is the prime activity of the Special Interest Group on Deduction Systems (FG DedSys) of the AI Section of the German Society for Informatics (GI-FBKI). It is a meeting with a familiar, friendly atmosphere, where everyone interested in deduction can report on their work in an informal setting. [less ▲]

Detailed reference viewed: 33 (1 UL)
See detailRuleML+RR 2019 Doctoral Consortium and Rule Challenge
Soylu, Ahmet; Moschoyiannis, Sotiris; Governatori, Guido et al

Book published by CEUR-WS.org (2019)

Detailed reference viewed: 10 (1 UL)
Full Text
Peer Reviewed
See detailHigher-Order Theorem Proving and its Applications
Steen, Alexander UL

in IT-Information Technology (2019), 61(4), 187-191

Detailed reference viewed: 57 (3 UL)
See detailChallenges in Higher-Order Theorem Proving
Steen, Alexander UL

Article for general public (2019)

Detailed reference viewed: 18 (3 UL)
Full Text
See detailExtensional Higher-Order Paramodulation in Leo-III
Steen, Alexander UL; Benzmüller, Christoph UL

E-print/Working paper (2019)

Detailed reference viewed: 19 (0 UL)
Full Text
Peer Reviewed
See detailNAI: The Normative Reasoner
Libal, Tomer UL; Steen, Alexander UL

in Bex, Floris (Ed.) Proceedings of the Seventeenth International Conference on Artificial Intelligence and Law (2019)

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

in Benzmüller, Christoph; Stuckenschmidt, Heiner (Eds.) {KI} 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings (2019)

Detailed reference viewed: 21 (1 UL)
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: 46 (3 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: 25 (3 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: 24 (14 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: 46 (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: 53 (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: 57 (2 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: 59 (3 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: 65 (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: 44 (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: 13 (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: 9 (0 UL)