NAMOR: a New Agda Library for Modal Extended Sequents

This paper introduces NAMOR (New Agda MOdal Realization), a comprehensive Agda library for mechanizing modal proof theory through extended sequents. Our approach employs position-based reasoning that mirrors first-order logic structures while maintaining implicit accessibility relations. Building on our previous investigation of extended deductive systems, NAMOR provides a unified framework for formalizing proof-theoretical properties across normal extensions of modal logic K, from basic K through S5. The library is founded on our novel sequent calculus E, which exhibits remarkable modularity: all captured logics share identical inference rules, differing mainly in their modal constraints. This enables systematic verification of meta-theoretical properties while preserving the intuitive structure of paper-and-pencil proofs. By leveraging Agda’s expressive type system, NAMOR establishes a direct correspondence between formal proofs and their mathematical counterparts, creating a robust platform for symbolic reasoning in domains where modal logic naturally applies