Further Tackling Post Correspondence Problem and Proof Generation

on YouTube ↗31m

" summary

Claim: all but two PCP[3,4] instances are decided — 368 instances solved — using two new invariant-finding methods plus a manual invariant editor; one method exhaustively searches infix/prefix/suffix patterns and the other abstracts sets as NFAs with concatenation and left-quotient operations. Implementations produce thousands of lines of code and an automatic proof generator that emits machine-checkable proofs verified with Isabelle/HOL proof generation, with a few proofs requiring manual guidance but overall successful.

AI-written summary · about

" chapters (18)

1. 0:00Introduction
2. 0:25PCP overview and motivation
3. 1:09Formalizing the Post Correspondence Problem
4. 3:15PCP 3 4 instances
5. 4:37Contributions and solved instances
6. 5:22Automated proof generation
7. 7:12Inductive invariants for unsolvable
8. 11:13Two invariant discovery methods
9. 14:31Infix prefix suffix method
10. 15:37Regular language method details
11. 17:04Manual invariant discovery tool
12. 18:11Proof graphs from invariants
13. 20:20Nodes and automata in proofs
14. 21:01Inclusion relations between states
15. 22:29Inductive invariant conditions
16. 23:35Unverified instances and reversals
17. 24:18Conclusion and future work
18. 25:27Q&A