Skip to main content

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*.

Filter by
Sorted by
Tagged with
1 vote
2 answers

Topic for undergraduate thesis

I'm an undergraduate student in my final year studying applied mathematics. To graduate, I need to present a thesis, and I'm considering using Lean and first-order predicate logic for my thesis. My ...
Hackerman's user avatar
  • 111
2 votes
0 answers

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 ...
Gergely's user avatar
  • 311
-3 votes
1 answer

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 ...
HighAsAKiteOnMath's user avatar
5 votes
1 answer

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 ...
Gokul's user avatar
  • 53
9 votes
2 answers

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." ...
Trebor's user avatar
  • 3,967
13 votes
1 answer

Integration of proof assistants and Wikipedia-like websites?

I noticed that some of the entries that describe proofs of theorems also contain links to proofs of these theorems formalized in the Mizar proof assistant (example). There was one ...
user9716869 - supports Ukraine's user avatar
9 votes
2 answers

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 &...
Reubend's user avatar
  • 519