Skip to main content

Questions tagged [automated-theorem-proving]

For questions regarding ATP's (Automatic Theorem Provers), which attempt to prove a theorem without any assistance. If you are using a Proof Assistant or an interactive theorem prover and are providing help to the prover, then do not use this tag.

Filter by
Sorted by
Tagged with
8 votes
1 answer
431 views

What are some automated theorem generators? What background logic do they use and what heuristics do they use for theorem-goodness?

This paper describes a theorem generator called MetaGen. MetaGen's purpose is to make larger training sets to train provers, by producing theorems similar to ones a human might select for inclusion in ...
Greg Nisbet's user avatar
  • 2,771