general.hpp File Reference

Plans for automated theorem proving using computer algebra systems. More...

Go to the source code of this file.

Detailed Description

Plans for automated theorem proving using computer algebra systems.

A long-term goal is to provide a experimental systems where SAT and ATP coexist, so that approaches for integrating SAT into ATP can be studied.

Clause-based approach
  • First we need a representation of terms.
  • Then we need to implement unification algorithms.
  • Then the various inference rules need to be implemented:
    1. resolution rules
    2. equality rules.
  • Finally, the strategies guiding the inference process are implemented.
First-order theory of the reals
  • Are there implementations of the decision procedure for this theory in computer-algebra systems?
  • See "First-order 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 mathematica-program, but perhaps it's not too hard to learn from that).

Definition in file general.hpp.