Orbital library


The Orbital library is a Java class library providing object-oriented representations and algorithms for logic, mathematics, and computer science. This Java library provides computer algebra, numerical algorithms, theorem proving, search and planning etc. Generally speaking, the conceptual idea behind the Orbital library is to provide extensional services and components for Java, which surround the heart of many scientific applications. Hence the name Orbital library. Orbital library is designed with the goals of flexibility, conceptual simplicity and general applicability. You can get this Java library and its documentation here:



The Orbital library provides you with access to mathematical, algorithmic, and logical functionality.

Selected Publications

The Orbital library is used in a fair number of projects. It has also been mentioned in the following papers (among other publications) and is used in the underlying implementations:
  1. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real world verification.
    In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE'09, Montreal, Canada, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | slides | TR | smtlib | abstract]
    Introduces a decision procedure for universal nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the Real Nullstellensatz. An extended set of real arithmetic benchmarks from KeYmaera is available in smtlib, including the examples from CADE'09 paper and from some other KeYmaera-related papers.

  2. André Platzer and Jan-David Quesel.
    KeYmaera: A hybrid theorem prover for hybrid systems.
    In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | slides | tool | abstract]