Questions tagged [proof-search]
Use this tag for techniques related to finding a proof. Other tags to consider are *strategy*, *automatic*, *automated* and/or *automated-theorem-proving*.
6
questions
2
votes
0
answers
84
views
Algebraic manipulation: what is the best tool?
I have a set of algebraic axioms. I need to prove an equation, an algebraic law. What I did was applying "trivial" rewrite rules by a theorem prover from both ends, and then an automatic ...
- 267
-3
votes
1
answer
145
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 ...
- 269
5
votes
1
answer
78
views
Semantics verification of an LTL fragment logic
I am a beginner to Isabelle and I went over the proof documentation. I am trying to implement a fragment logic of LTL over finite intervals and finite traces called MLTL, the syntax and semantics can ...
- 53
9
votes
1
answer
437
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."
...
- 3,688
12
votes
1
answer
174
views
Integration of proof assistants and Wikipedia-like websites?
I noticed that some of the Wikipedia.org entries that describe proofs of theorems also contain links to proofs of these theorems formalized in the Mizar proof assistant (example). There was one ...
9
votes
2
answers
260
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