Questions tagged [automated]
Use this tag when a Proof Assistant is relying on automation. The automation can be internal or external to the proof assistant. An typic external form of automation is an automatic theorem prover. Consider also using the tag atp if that applies.
5
questions
3
votes
1
answer
122
views
Do implementations of a PA and of ATP have overlap?
I'm wondering how much overlap (read: code-reusage) there is between a PA and an ATP system.
Are they based upon the same type system at least?
I'm wondering, because right now I'm working on ...
-3
votes
1
answer
150
views
Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?
So I'm not sure how things are done in Lean4 or Coq, but I'm interested in their search features. For example, "Search for all theorems that get satisfied given a user-defined list of ...
9
votes
2
answers
590
views
What is the state of the art in proof automation in HoTT/CuTT?
One of the frequent criticisms of HoTT is that it requires a lot of lemmata keeping track of which types are sets/propositions etc. And a frequent counterpoint is "It can be automated."
...
- 4,025
7
votes
1
answer
142
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 ...
- 519
9
votes
2
answers
276
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 &...
- 519