Contradiction Detection and Repair in a Large Theory

Abstract

As with any software, the challenges of developing large and
manually-created axiomatizations in an expressive logic such
as first order logic with equality can be very different from
those found in comparatively small theories. We present some
of the tools and practices that have supported development of
a logical theories with tens of thousands of statements, and
ensured that they are free of logical contradiction, and suit-
able for automated theorem reasoning.