Algorithm for intuitionistic propositional logic

Stream: maths

[Jiatong Yang]

I've heard that it is possible to judge whether a prop of intuitionistic propositional logic(not first order logic, it only contains variables that represent prop) is provable in finite steps. What is a pratical algorithm for that?

[Eric Wieser]

Is tactic#itauto that algorithm, or is that only for FOL?

[Alexander Bentkamp]

itauto is intuitionistic propositional logic. I guess this is the relevant paper: https://drops.dagstuhl.de/opus/volltexte/2021/13904/pdf/LIPIcs-ITP-2021-9.pdf

[Mario Carneiro]

That... is actually a coincidence? I did not know there was another coq tactic by the same name

[Mario Carneiro]

I used the LJT algorithm, for example here

[Mario Carneiro]

The coq tactic is actually quite different from lean's itauto, and resembles a SAT solver.