Contradiction Detection and Repair in a Large Theory
Adam Pease, Stephan Schulz · Proceedings of the ... International Florida Artificial Intelligence Research Society Conference · 2022
As with any software, the challenges of developing large andmanually-created axiomatizations in an expressive logic suchas first order logic with equality can be very different fromthose found in comparatively small theories. We present someof the tools and practices that have supported development ofa logical theories with tens of thousands of statements, andensured that they are free of logical contradiction, and suit-able for automated theorem reasoning.