search

BFO-ontology / BFO-2020

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

Restructuring Repo to Highlight BFO-Core #67

Closed johnbeve closed 12 months ago

johnbeve commented 1 year ago

Highlights include:

  1. Moved contents of 21838-2 directory to temporal extension sub-directory for temporalized relations
  2. Renamed bfo-2020-without-some-all-times.owl to bfo-core.owl, edited for consistency throughout, corrected genuses in handful of textual definitions, added domain/range to exists at, corrected spatiotemporal projection clause of textual definition of occurs in
  3. Created mermaid-based BFO figure
  4. Renamed 'bfo-2020' files to reflect implementation language, e.g. BFO-FOL, BFO-CL, BFO-TPTP
  5. Removed temporalized relations axioms from BFO-Core implementations
  6. Added readme outlining motivations for temporalized extensions
alanruttenberg commented 1 year ago

Starting to review. Nice reorg. Will add to this thread as I look through things. So far:

johnbeve commented 1 year ago
  • Some directories labeled TPTP are not they are prover9 syntax.

Ah you're right about TPTP, but I think the syntax for prover9 and mace4 might be called LADR (Library for Automated Deduction Research).

Understood

  • The OWL files (as well as CL, P9, FOL) are all generated, so I'd rather not have changes to them made here. Preferred process would be to submit issue here, change source in bfo-theory repo, regenerate, test, deploy here. That process needs to be documented so other than I can do it - student?

Gotcha, I know just the person..

johnbeve commented 1 year ago
  • The OWL files (as well as CL, P9, FOL) are all generated, so I'd rather not have changes to them made here. Preferred process would be to submit issue here, change source in bfo-theory repo, regenerate, test, deploy here. That process needs to be documented so other than I can do it - student?
johnbeve commented 1 year ago

(Didn't mean to close; hit the wrong button)

johnbeve commented 1 year ago
  • The OWL files (as well as CL, P9, FOL) are all generated, so I'd rather not have changes to them made here. Preferred process would be to submit issue here, change source in bfo-theory repo, regenerate, test, deploy here. That process needs to be documented so other than I can do it - student?

Given the need to polish up the owl file sooner rather than later, can we make an exception in this case? I can start drafting a wiki page outlining the preferred process.

johnbeve commented 1 year ago

Sanity check (assume each is preceded by "https://raw.githubusercontent.com/BFO-ontology/BFO-2020/"

master/21838-2/owl/bfo-2020-without-some-all-times.owl replaced by - implementations/BFO-OWL/bfo-core.owl

master/21838-2/owl/bfo-2020.owl replaced by - temporal extensions/temporalized relations/implementations/BFO-TR-OWL/bfo-TR.owl

And when whenever we add stasis content to its directory, we'll have the OWL file as: temporal extensions/stases/implementations/BFO-ST-OWL/bfo-ST.owl

@alanruttenberg How does that sound?

alanruttenberg commented 1 year ago

I'm going to start adding comments as I go through this as it's a lot to go through as a whole. To start with, the TPTP directories are mislabeled as the contents are prover9 format which is a different format than TPTP

alanruttenberg commented 1 year ago

Given the need to polish up the owl file sooner rather than later, can we make an exception in this case? I can start drafting a wiki page outlining the preferred process.

Yes. Let's keep a file documenting all changes so I can incorporate them into the build process for the next time.

alanruttenberg commented 1 year ago

I'm going to start adding comments as I go through this as it's a lot to go through as a whole. To start with, the TPTP directories are mislabeled as the contents are prover9 format which is a different format than TPTP

Sorry, hadn't realized I already commented on this. Yes, LADR encompasses both prover9 and mace4 so we could name them that. However, prover9 is a better known name and we don't include anything from MACE4, so prover9 might be a better label. Also, clausetester is also part of LADR and the model is serialized in that format.

johnbeve commented 1 year ago

@alanruttenberg Yeah, I had to do some digging to find "LADR" so probably better to go with prover9 as the label. I was under the impression you'd used mace4 to generate the model, but you've since disabused me. Will update the directories.

alanruttenberg commented 1 year ago

BFO tree diagram has really tiny fonts. Even though there's a zoom button might be better to start with a larger font.

alanruttenberg commented 1 year ago

Readme says: "implementations - Contains implementations of BFO in OWL, Common Logic, and syntax readable by Prover9/Mace4."

We don' have any mace4, so just say prover9? Link to prover9: https://www.cs.unm.edu/~mccune/prover9/ (rather than current mace4 links)

alanruttenberg commented 1 year ago

I think add the case studies paper to this repository rather than depending on Philpapers.

alanruttenberg commented 1 year ago

Documentation folder is empty other than for blank readme.

alanruttenberg commented 1 year ago

I'm no longer affiliated with the dental school. I think have my affiliation be NCOR

alanruttenberg commented 1 year ago

Another change for bfo.owl - add yourself and Neil Otte as contributors. I've updated my source so those will be included in the next build.

alanruttenberg commented 1 year ago

Are the functional syntax formats gone? The labeled version is useful as it is more readable as text than the RDF/XML. I'd like that included, though I can generate a separate one for the core if you would like.

alanruttenberg commented 1 year ago

The BFO-iris and BFO-terms, although they include TRs, are not specific to them. I think either move them to a higher level or created edited versions that remove TRs and include that copy with BFO-core

alanruttenberg commented 1 year ago

The BFO-iris and BFO-terms, although they include TRs, are not specific to them. I think either move them to a higher level or created edited versions that remove TRs and include that copy with BFO-core

Unfortunately, those excel files are edited by hand and not generated, so we'll have to make sure they are individually updated if they need changes.

alanruttenberg commented 1 year ago

The CL, FOL, and Prove9 files are the same for core and temporalized, save temporalized-relations.* and I don't think we should have duplicates. Two options:

alanruttenberg commented 1 year ago

This is a style thing, so I won't insist, but I think for the folder names, the original "common logic", "prover9", and "pdf" were better than prefixing everything with "BFO-" allcaps with abbreviations. Maybe "pdf" -> "fol", though the common logic are FOL as well, which is why I didn't originally name them FOL.

alanruttenberg commented 1 year ago

"Note that BFO-OWL is an approximation to the BFO-FOL and BFO-CL implementations, which are stronger." (in the readme)

This suggests that BFO-FOL and BFO-CL are different implementations, which they aren't. They are two formats (pdf and CLIF), for the same thing, a first order theory.

alanruttenberg commented 1 year ago

gitattribute linguist: Might be worth submitting a PR for https://github.com/github-linguist/linguist/blob/916bd8f3df802fa98b0ea85539e67bd0b88ef158/lib/linguist/languages.yml so that it understands what .prover9, .ofn, .cl are.

alanruttenberg commented 1 year ago

For comments you don't want to address before merging, we can do them after merge - just add an issue so we can track it.

johnbeve commented 1 year ago

"Note that BFO-OWL is an approximation to the BFO-FOL and BFO-CL implementations, which are stronger." (in the readme)

This suggests that BFO-FOL and BFO-CL are different implementations, which they aren't. They are two formats (pdf and CLIF), for the same thing, a first order theory.

That's actually how I intend to use "implementation", i.e. to mean syntactic formalizations of the first order theory. In this sense, BFO-OWL is also an implementation. Strictly speaking, the labels should be BFO-CLIF and whatever specific name the FOL syntax in the files is, but I thought it'd be less confusing to use CL and FOL.

alanruttenberg commented 1 year ago

That's actually how I intend to use "implementation", i.e. to mean syntactic formalizations of the first order theory. In this sense, BFO-OWL is also an implementation.

Understood. Maybe implementation isn't the right word to use. There are theories, of which there are 2 or 4, depending on how they are counted: FOL core, FOL temporalized, OWL core, OWL temporalized, and renderings/formats of each: 3 for FOL: prover9, pdf, clif, 3 for OWL: .owl, .ofn, .ofn with labels, 2 as spreadsheet/natural language. (.xlsx, .csv).

Yah I know picky. Occupational hazard.

johnbeve commented 1 year ago

That's actually how I intend to use "implementation", i.e. to mean syntactic formalizations of the first order theory. In this sense, BFO-OWL is also an implementation.

Understood. Maybe implementation isn't the right word to use. There are theories, of which there are 2 or 4, depending on how they are counted: FOL core, FOL temporalized, OWL core, OWL temporalized, and renderings/formats of each: 3 for FOL: prover9, pdf, clif, 3 for OWL: .owl, .ofn, .ofn with labels, 2 as spreadsheet/natural language. (.xlsx, .csv).

Yah I know picky. Occupational hazard.

Man, you know I love it when you're picky; will reflect a bit more