analytic hyperbolic geometry from a logical point of view

In 1988 abraham a. ungar planted the first seeds of a theory that provided the machinery to study hyperbolic geometry in an analytical way in full analogy of analytical euclidean geometry. in this paper with the aid of logical axiomatization of hyperbolic geometry, we will check the correspondence of theorems and proofs of some more popular problems, e.g. steiner-lehmus theorem, etc. we will use automated theorem-proving methods to prove new theorems such as the hyperbolic breusch’s lemma and hyperbolic urquhart’s theorem.