search

BFO-ontology / BFO-2020

A repository for BFO 2020 artifacts specified in ISO 21838-2:2020
78 stars 28 forks source link

Consistency proof for 8792dde commit #40

Closed mereolog closed 2 years ago

mereolog commented 2 years ago

Could you share the details of how you checked the consistency of 8792dde?

I tried to use a number of reasoners, including the ones accessible from https://www.tptp.org, but all of them timed out after reasonable time limits.

alanruttenberg commented 2 years ago

I don't know about a specific commit but the the consistency proof is shown by showing there's a model. There's a clausetester (LADR tools) file to check it but clausetester blows out the stack when I try to use it. Instead I use the equivalent of clausetester that I wrote. Not sufficiently documented, but you can check it out Please close the issue if you are satisfied with this response.

mereolog commented 2 years ago

Thanks for this clarification.

However, I am after being able to verify the consistency of BFO automatically, so I would like to use a reasoner/model finder to check whether the model you refer to is indeed a model of BFO (at a given commit). I think that at the moment this is not possible because some of CLIF axioms seem to be ill-formed - see: https://github.com/BFO-ontology/BFO-2020/issues/47.

wceusters commented 2 years ago

eom-1 was found to be incorrect last year, but perhaps not updated yet. wsg-1 contained also a mistake, found at the same time.

alanruttenberg commented 2 years ago

these should be fixed now. The only model that should be checked is the most recent commit. Others are probably consistent but its only worth fixing stuff that is wrong now.

mereolog commented 2 years ago

The fix solves this issue, but see https://github.com/BFO-ontology/BFO-2020/issues/48.