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 developm...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
LibraryPress@UF
2022-05-01
|
| Series: | Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| Online Access: | https://journals.flvc.org/FLAIRS/article/view/130691 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | 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. |
|---|---|
| ISSN: | 2334-0754 2334-0762 |