I am wondering if they are automated theorem provers which can take as input known models of the theory, for example to help discard statements which are not correct. For example, if the statements are about group theory, the prover could have access to a collection of examples of groups. This approach has been used in synthetic geometry by Gelernter using the standard euclidean model (see "An Examination of the Geometry Theorem Machine" by P. C. Gilmore, page 179). I wonder if it has been used in other fields ?

  • 1
    $\begingroup$ This question is probably better asked in Proof Assistants. $\endgroup$
    – Pseudonym
    Commented Apr 28, 2023 at 11:39
  • $\begingroup$ I don't immediately see how examples would be useful for automated theorem proving. Are you asking about automated theorem discovery (finding new theorems, rather than finding a proof of a proposed thoerem)? $\endgroup$
    – D.W.
    Commented Apr 28, 2023 at 18:25
  • $\begingroup$ @Pseudonym no my question is about automated theorem proving, not interactive theorem proving. $\endgroup$ Commented Apr 29, 2023 at 10:12
  • $\begingroup$ @D.W. using backward chaining it may be useful. For example, if I want to prove that I is the midpoint of AC, I may try to prove that ABCD is a parallelogram for some given B and D. But, using a model and an example of a figure one can see that ABCD is not a parallelogram, so it is not worth trying. $\endgroup$ Commented Apr 29, 2023 at 10:15

1 Answer 1


This is more of a long comment than an answer, but here goes. There's lots of stuff based on the paper you cite, starting with this Ray Reiter paper. This paper in turn seems to have kicked off all kinds of papers. David Plaisted has also done work in this area.

  • $\begingroup$ Thank you for the pointer ! $\endgroup$ Commented Apr 29, 2023 at 10:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.