Agent-Based Proof Design via Lemma Flow Diagram

Keehang Kwon, Daeseong Kang

We discuss an agent-based approach to proof design and implementation, which we call {\it Lemma Flow Diagram} (LFD). This approach is based on the multicut rule with $shared$ cuts.…