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!
|
| _version_ | 1849763354174816256 |
|---|---|
| author | Adam Pease Stephan Schulz |
| author_facet | Adam Pease Stephan Schulz |
| author_sort | Adam Pease |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-8f40901eca5b427396faee3a37956bc1 |
| institution | DOAJ |
| issn | 2334-0754 2334-0762 |
| language | English |
| publishDate | 2022-05-01 |
| publisher | LibraryPress@UF |
| record_format | Article |
| series | Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| spelling | doaj-art-8f40901eca5b427396faee3a37956bc12025-08-20T03:05:26ZengLibraryPress@UFProceedings of the International Florida Artificial Intelligence Research Society Conference2334-07542334-07622022-05-013510.32473/flairs.v35i.13069166890Contradiction Detection and Repair in a Large TheoryAdam Pease0Stephan Schulz1Articulate SoftwareDHBW StuttgartAs 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.https://journals.flvc.org/FLAIRS/article/view/130691 |
| spellingShingle | Adam Pease Stephan Schulz Contradiction Detection and Repair in a Large Theory Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| title | Contradiction Detection and Repair in a Large Theory |
| title_full | Contradiction Detection and Repair in a Large Theory |
| title_fullStr | Contradiction Detection and Repair in a Large Theory |
| title_full_unstemmed | Contradiction Detection and Repair in a Large Theory |
| title_short | Contradiction Detection and Repair in a Large Theory |
| title_sort | contradiction detection and repair in a large theory |
| url | https://journals.flvc.org/FLAIRS/article/view/130691 |
| work_keys_str_mv | AT adampease contradictiondetectionandrepairinalargetheory AT stephanschulz contradictiondetectionandrepairinalargetheory |