All Questions
Tagged with automated-theorem-proving software-request
2
questions
7
votes
0
answers
78
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 + ...
15
votes
1
answer
275
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 ...