References of "Wisniewski, Max"
     in
Bookmark and Share    
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: 83 (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 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: 37 (0 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: 43 (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: 41 (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 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 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)
Full Text
See detailComputational Metaphysics
Benzmüller, Christoph UL; Wisniewski, Max; Steen, Alexander UL

Report (2015)

Detailed reference viewed: 22 (0 UL)
Full Text
Peer Reviewed
See detailThe Leo-III Project
Wisniewski, Max; Steen, Alexander UL; Benzmüller, Christoph UL

in Bolotov, Alexander; Kerber, Manfred (Eds.) Proceedings of the Joint Automated Reasoning Workshop and Deduktionstreffen: As part of the Vienna Summer of Logic – IJCAR 23-24 July 2014 (2014)

Detailed reference viewed: 13 (0 UL)