Search results

MyORBi^lu

Browse ORBi^lu by

Open Access

ORBi^lu

The ORBi^lu Project

ISSN: 2354-5011

ORBi^lu is a project developed by


	New search Results 21-40 of 54. 1 2 3 RuleML+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: 47 (1 UL) Higher-Order Theorem Proving and its Applications Steen, Alexander in IT-Information Technology (2019), 61(4), 187-191 Detailed reference viewed: 120 (3 UL) Challenges in Higher-Order Theorem Proving Steen, Alexander Article for general public (2019) Detailed reference viewed: 48 (5 UL) Selected Student Contributions and Workshop Papers of LuxLogAI 2018 Benzmüller, Christoph ; Parent, Xavier ; Steen, Alexander Book published by EasyChair (2019) Detailed reference viewed: 85 (7 UL) The Higher-Order Prover Leo-III Steen, Alexander Presentation (2019, April 26) Detailed reference viewed: 45 (1 UL) Extensional Higher-Order Paramodulation in Leo-III Steen, Alexander ; Benzmüller, Christoph E-print/Working paper (2019) Detailed reference viewed: 50 (2 UL) The Higher-Order Prover Leo-III (Extended Abstract) Steen, Alexander ; Benzmüller, Christoph 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: 78 (1 UL) NAI: The Normative Reasoner Libal, Tomer ; Steen, Alexander in Bex, Floris (Ed.) Proceedings of the Seventeenth International Conference on Artificial Intelligence and Law (2019) Detailed reference viewed: 53 (5 UL) The NAI Suite - Drafting and Reasoning over Legal Texts Libal, Tomer ; Steen, Alexander in Araszkiewicz, Michal; Rodriguez-Doncel, Victor (Eds.) Legal Knowledge and Information Systems - JURIX2019: The Thirty-second Annual Conference, Madrid, Spain, December 11-13, 2019 (2019) Detailed reference viewed: 52 (0 UL) NAI – The Normative Reasoner Libal, Tomer ; Steen, Alexander Software (2019) Detailed reference viewed: 98 (9 UL) Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III Steen, Alexander Book published by AKA-Verlag (2018) Detailed reference viewed: 108 (4 UL) System Demonstration: The Higher-Order Prover Leo-III Steen, Alexander ; Benzmüller, Christoph in CEUR Workshop Proceedings (2018), 2095 Detailed reference viewed: 50 (15 UL) The Higher-Order Prover Leo-III Steen, Alexander ; Benzmüller, Christoph 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: 94 (3 UL) GCAI-2018. 4th Global Conference on Artificial Intelligence Lee, Daniel; Steen, Alexander ; Walsh, Toby Book published by EasyChair (2018) Detailed reference viewed: 56 (4 UL) Leo-III Version 1.1 (System description) Benzmüller, Christoph ; Steen, Alexander ; 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: 114 (3 UL) Going Polymorphic - TH1 Reasoning for Leo-III Steen, Alexander ; Wisniewski, Max; Benzmüller, Christoph 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: 103 (4 UL) Capability Discovery for Automated Reasoning Systems Steen, Alexander ; 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: 112 (2 UL) Theorem Provers for Every Normal Modal Logic Gleißner, Tobias; Steen, Alexander ; Benzmüller, Christoph 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: 148 (2 UL) The Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument Fuenmayor, David; Benzmüller, Christoph ; Steen, Alexander et al in The 2nd World Congress on Logic and Religion -- Book of Abstracts (2017) Detailed reference viewed: 126 (2 UL) TPTP and Beyond: Representation of Quantified Non-Classical Logics Wisniewski, Max; Steen, Alexander ; Benzmüller, Christoph in Benzmüller, Christoph; Otten, Jens (Eds.) ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics (2016, December) Detailed reference viewed: 39 (0 UL) 1 2 3

Creative Commons Licence

University of Luxembourg Library | Feedback | Legal notices