Plans for automated theorem proving using computer algebra systems.
A longterm goal is to provide a experimental systems where SAT and ATP coexist, so that approaches for integrating SAT into ATP can be studied.
 Todo:
 Clausebased approach

First we need a representation of terms.

Then we need to implement unification algorithms.

Then the various inference rules need to be implemented:

resolution rules

equality rules.

Finally, the strategies guiding the inference process are implemented.
 Todo:
 Connections
 Todo:
 Firstorder theory of the reals

Are there implementations of the decision procedure for this theory in computeralgebra systems?

See "Firstorder theory of the reals" in Buildsystem/ExternalSources/SpecialBuilds/plans/ATP.hpp.

Perhaps this topic should go to ComputerAlgebra/FirstOrderStructures ?

But ATP seems alright, since here theorems are proved automatically (though not with general logical methods, but with specialised algorithms  but that should also belong to here).

In [A decision procedure for probability calculus with applications; Fitelson, 2008. The review of symbolic logic] an interesting application is discussed (only with a mathematicaprogram, but perhaps it's not too hard to learn from that).
Definition in file general.hpp.