Contradiction Detection and Repair in a Large Theory
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.
How to Cite
Copyright (c) 2022 Adam Pease, Stephan Schulz
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.