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
11 votes
1 answer
243 views

auto-generating the proof of infinitude of primes

The chess computer which beat the human world champion in 1997 had a huge database of openings inbuilt into it. However my understanding of Deep Mind's alpha zero is that it is capable of generating ...
user avatar
5 votes
0 answers
69 views

Is any theorem prover able to prove quadratization relations without knowing the proof strategy that humans used?

Motivation In discrete optimization, our goal is often to optimize a function of binary variables, such as: $$\tag{1} {\scriptsize 5 - 3b_1 - b_2 - b_3 + 2b_1b_3 - 3b_2b_3 + 2b_1b_2b_3 - 3b_4 + ...
user avatar
  • 1,090
11 votes
0 answers
172 views

Do any automated theorem provers have the ability to stop, save state, reboot computer, restore state, continue?

With automated theorem provers knowing ahead of time how long the search will take or even if it will find a solution is unknown. Often for long running searches one eventually just has to halt the ...
user avatar
  • 2,676
5 votes
1 answer
110 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 ...
user avatar
  • 2,467
6 votes
1 answer
107 views

Understanding "saturating" theorem provers

The documentation for the E Theorem Prover explains this as the first step in its process: A clausification algorithm translates first-order input into clause normal form, such that the resulting ...
user avatar
  • 489
7 votes
2 answers
234 views

Are search heuristics the main bottleneck for automated theorem provers?

My understanding of most automated theorem provers (which is possibly an incorrect understanding!) is that they start with some premises stored as unprocessed statements, and repeatedly select one to &...
user avatar
  • 489
14 votes
1 answer
179 views

Are there automated theorem provers for constructive logics? What strategy do they use?

I know of a handful of automated theorem provers for classical first-order logic such as Vampire (source code). Internally, I think most of these provers work by translating premises and the negated ...
user avatar
  • 2,467
21 votes
2 answers
211 views

Successes of machine learning in formal theorem proving

Attempts to apply machine-learning (as opposed to hand-crafted automation) to formal theorem proving are still in their infancy. Still, there have been some successes. GPT-f found some proofs that ...
user avatar