Abstract. Pocket KRHyper is a reasoning system for Java-enabled mobile devices. The core of the system is a first order theorem prover and model generator based on the hyper tableau calculus. The development of Pocket KRHyper was motivated by the arising need for reasoning on mobile devices for mobile semantic web applications. To satisfy this need, a Description Logics (DL) interface is provided, which allows DL reasoning by transforming DL Expressions into first order clausal logic.