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.
2
questions
1
vote
0
answers
45
views
Integrating SAT solvers supporting only a finite set of variables into proof assistants
We're currently looking at how to integrate neural network solvers into general proof assistants. One of the issues we're running into is that, unlike general SAT/SMT solvers like Z3, queries for ...
- 191
4
votes
2
answers
186
views
Ltac - run tactic for each hypothesis of given pattern
Especially in the context of lia, which can sometimes fail to prove a theorem in the form of
forall x, x <> 0 -> P x
...
- 171