Pocket KrHyper
About
Pocket KrHyper is a theorem proving library for J2ME mobile devices. It supports reasoning in propositional, first order, and description logics and is aimed at mobile knowledge management or semantic web applications.
Features
- The first reasoner for mobile phones
- Java library, works both with J2ME (mobile) and J2SE (desktop)
- Uses little resources
- interfaces for clausal first order logic and description logic
Todos
- comprehensive Manual, please use publications of the authors
- DIG interface, as defined here
- Other interfaces
Links
Related Work
- Prolog KrHyper, the first implementation of the hyper tableau calculus by Peter Baumgartner.
- KrHyper, the reference implementation in OCaml by Christoph Wernhard.
- cardTAP, the first theorem prover on JavaCard.
- TPTP library, a very important collection of theorem proving problems useful for benchmarking and debugging ATP systems. One example application for Pocket KrHyper includes some TPTP problems to solve on your mobile phone.
About the Authors
This ATP is a joint work of Alex Sinner and Thomas Kleemann. Among our publications you will find additional material concerning the use cases of this prover.
The software was initially developed while the authors were members of the IASON project at the University of Koblenz-Landau.
Acknowledgements
Many thanks to Christoph Wernhard, the author of the desktop KRHyper system for many valuable tips on things to consider for the implementation.
Many thanks also to Geoff Sutcliffe for his support and the excellent TPTP (Thousands of Problems for Theorem Provers) library.