search

zhengj2007 / bfo-trunk

0 stars 0 forks source link

Should FOL be run through prover to check for consistency before being released to a wider audience? #29

Open zhengj2007 opened 9 years ago

zhengj2007 commented 9 years ago

From alanruttenberg@gmail.com on May 09, 2012 11:30:16

I think yes, but we should make a decision and then follow it.

Original issue: http://code.google.com/p/bfo/issues/detail?id=30

zhengj2007 commented 9 years ago

From ontolo...@yahoo.com on May 09, 2012 14:24:33

On first thought, I'd say yes.

But what, if any, are the disadvantages to using prover (do you mean prover9?) ?

zhengj2007 commented 9 years ago

From cmung...@gmail.com on May 09, 2012 18:16:09

perhaps Alan just meant theorem prover generically. P9 is an option but you'd have to convert the CLIF using some tool (I have some adhoc tools for this), and P9 may have some limitations.

HETS might be a good choice as this will maximize interoperability with bfo-owl

zhengj2007 commented 9 years ago

From alanruttenberg@gmail.com on May 09, 2012 20:23:16

I meant a theorem prover generically. Don't know HETS. Latest version sent by Mark includes a clif format version. Chris - you should have received that email.

zhengj2007 commented 9 years ago

From jacu...@gmail.com on May 14, 2012 12:23:55

I don't think it is possible to use a reasoner on BFO-FOL as it stands... For one thing '=df' is not a connective in FOL. For another, the specification as it stands is incoherent.

zhengj2007 commented 9 years ago

From alanruttenberg@gmail.com on May 24, 2012 19:17:09

HETS for Common Logic Users: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk/doc/UserGuideCommonLogic.pdf http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/installation_e.htm Looks like a consistency check can be done by translation to the format SPASS uses.

On this page, bottom, there is a CLIF validation tool. It says, about the most recent release by Mark: "BFO-FOL-alpha-2012-05-21.clif is valid". Woot!

Status: Accepted