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

[GoogleCodeExporter]

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

Original issue reported on code.google.com by alanruttenberg@gmail.com on 9 May 2012 at 3:30

[GoogleCodeExporter]

On first thought, I'd say yes.

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

Original comment by ontolo...@yahoo.com on 9 May 2012 at 9:24

[GoogleCodeExporter]

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

Original comment by cmung...@gmail.com on 10 May 2012 at 1:16

[GoogleCodeExporter]

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. 

Original comment by alanruttenberg@gmail.com on 10 May 2012 at 3:23

[GoogleCodeExporter]

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.

Original comment by jacu...@gmail.com on 14 May 2012 at 7:23

[GoogleCodeExporter]

HETS for Common Logic Users:

https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk/doc/UserGuideCommonLogic.p
df
http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/ins
tallation_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!

Original comment by alanruttenberg@gmail.com on 25 May 2012 at 2:17

• Changed state: Accepted