From MathWeb

Contents 1 How can dependency be defined in a formal way? 1.1 Which relations are specialized dependencies? 2 How to model dependencies between proofs and assertions? 3 How to model "proof uses theorem (as a premise)"? 4 Does proof/@for refer to an assertion or to a theorem? 5 What is the meaning of the different subclasses of assertion (as set by assertion/@type)? 6 Limits of description logic / rules 7 Defining Concepts 8 has-definition functional? 9 Omtext, Omgroup, OmDoc

How can dependency be defined in a formal way?

So far, my pragmatic definition, inspired by a practical view on management of change, is:

This relation denotes that one concept A logically depends on another concept B. If the semantics of A changes, B might become invalid.

How can this be formalized? --Clange 14:13, 4 April 2007 (CEST)

An idea by Immanuel: , i.e. there are two predicates that express something like "is broken".

Example for the dependency (a symbol depends on its definition): p₂(D) would be something like ch(D) "has been changed" (should be specified more exactly!), and p₁(S) would be something like ch(sem(S)), with , i.e. the set of all formulae that use S and that are true in the theory T. --Clange 15:17, 4 April 2007 (CEST)

I suggest that we have a set of predicates p_1...n which denotes relations between classes of objects. One example for p might be: the (natural language) Sentence S 'describes' picture B. Formally: p₁(S,B) is true. If B is changed by some transformation t₁ which violates this relation, then I would call p a semantic dependency relation. This would be the case if B is changed into a picture with depicts another function, but not the original one. Formally: . Note: there might be other transformations which doesn't break p₁ like exchanging the picture by one in which the color of the curve is changed or some other irrelevant stuff. -- Ama 16:56, 13 April 2007 (CEST)

Which relations are specialized dependencies?

We (Immanuel and Christoph) found out that it should be possible to express dependencies between a theory importing another theory, as well as between a symbol and its definition in the above way. However, is there a dependency between a proof and the theorem it proves (see also below)? If so, in which direction? --Clange 15:17, 4 April 2007 (CEST)

How to model dependencies between proofs and assertions?

Starting from the pragmatic interpretation of "A depends on B" as "if B is broken, so is A", I'd like to have the following dependencies between proofs and assertions:

• A proof depends on the assertion it proves. (That's modeled in the current version of the ontology, inspired by the documentation of the MMiSSLaTeX ontology in the OMDoc book.) That is, if I change the assertion, the proof is no longer valid. (On the other hand, if I change the proof, then the proof might turn wrong, but that does not affect the integrity of the assertion.)
• A proof also depends on the assertions it uses (see below). If a certain step of a proof relies on a certain theorem and that theorem is changed, the proof step is no longer valid.
• If P proves S using T, would it make sense to have a dependency "S depends on T"?
  • Rationale: If T is broken, the proof of S is no longer valid; thus, S gets broken.
  • However, I said above that a broken proof maybe does not affect the assertion it proves.

Question: Which of these dependencies should we consider?? --Clange 20:50, 3 April 2007 (CEST)

I would postulate the following:--Mbroecheler 01:06, 18 April 2007 (CEST)

• A proof definitely depends on the assertion it proves.
• A general assertion is in no way dependent on a proof.
• It gets trickier on the subclasses of assertions, like theorem and conjecture. A theorem by definition (and I would opt for including this in the document ontology) needs to have a (valid) proof. If it does not have one or if the one which proved the theorem was significantly changed, then the theorem turns into a conjecture (assuming there are no other proofs for the theorem). As such it is not so much a semantic consistency issue, but rather a conceptual change. In particular nothing gets broken. Consistency enters the game when we look at the OMDoc markup. In the OMDoc file, an assertion might have been marked up as a theorem, which it no longer is. Still, the content of the assertion and its meaning are not broken, but the mark up is. I think it is important to make this distinction. In particular, one could automatically resolve this mark up inconsistency (simply rename), whereas semantic inconsistencies can never be (at least for a long time) and require significant user intervention.

  Why not – in theory that sounds good! But, in practice, it would make the ABox extraction harder to code, as there is no longer a static mapping from <assertion type="theorem"> to the class Theorem in the document ontology. How about considering the case strict vs. loose constraints again here? With the strict ontology, we'd map <assertion type="theorem"> to Theorem and fail when there is no proof (assuming ), whereas with the loose ontology, we'd instead map <assertion type="*"> to Assertion and disregard the subclasses. --Clange 11:53, 18 April 2007 (CEST)

How to model "proof uses theorem (as a premise)"?

I discussed this with Krzysztof Retel on the omdoc-dev list in September 2006; unfortunately, the archive is lost. --Clange 17:33, 3 April 2007 (CEST)

1. introduce a direct relation Proof-uses-Theorem?
2. or model it in accordance to the corresponding OMDoc elements, i.e. Proof-contains-DeriveStep, DeriveStep-uses-Method, Method-hasPremise-Theorem?
   • Then, we'd need some rules (see below)
   • Actually, we don't really need rules for this we just need to wait. OWL 1.1 will allow property compositions (role composition), that means one could declare where R₁ = Proof-contains-DeriveStep, R₂ = DeriveStep-uses-Method, and R₃ = Method-hasPremise-Theorem. In OWL 1.1 this will be done using propertyChain. In my opinion this is the most elegant solution.--Mbroecheler 00:48, 18 April 2007 (CEST)

So in other words, OWL 1.1 will capture , right? That would be really cool, cause it's still decidable! Please keep us informed about the progress of OWL 1.1 -- Nmueller 10:19, 18 April 2007 (CEST)

I think the official name for the description logic underlying OWL 1.1 is . Beautiful name! Even though I have been working with theses things for some time I still need to look up what the individual letters stand for. But yes, it is still decidable - that is in theory. I don't think there are any reasoners for this logic yet. --Mbroecheler 22:36, 28 April 2007 (CEST)

Does proof/@for refer to an assertion or to a theorem?

According to chapter 17.1 of the OMDoc book, proof/@for can refer to any assertion element, although an assertion that does have a proof should rather be called a theorem (via setting its type attribute to "theorem"). However, figure 15.10 of the OMDoc book (Types of Mathematical Assertions) states that "OMDoc does not enforce the meaning of the type (in this case the existence of a proof)". --Clange 17:33, 3 April 2007 (CEST)

Maybe there should be one "loose" and one "strict" version of the document ontology? The former would allow Proof-proves-Assertion, whereas the latter would only allow Proof-proves-Theorem.

• The "strict" version makes sense for validation, …
• whereas the "loose" version makes sense for daily work with OMDoc documents in an inconsistent/changing environment (think of SWiM, locutor). --Clange 17:33, 3 April 2007 (CEST)

In my opinion, we definitely need to express "strong" and "weak" inconsistencies. Whether this should be expressed in the ontology or by some other means, I'm not sure. I think, a look at how CDET does this will give better intuitions on that. -- Ama 17:03, 13 April 2007 (CEST)

Also see below.

What is the meaning of the different subclasses of assertion (as set by assertion/@type)?

1. What are the differences between Theorem/Proposition, Conjecture/Postulate and Obligation/Assumption?
   • In the OMDoc book no distinction is made between the respective types of assertions and if there is any (which I do not believe to be significant) then it most probably depends on the community of practice. Consider for example the distinction between Lemma and Theorem which is actually specified namely, in terms of importance. Now, importance is rather subjective (although it could be captured via a modal logic variant of DL :-) and can change over time (consider mathematical literature where Lemmas sometimes became more important than the corresponding theorems). In light of this it seems artificial to engrave any more semantics in those terms than is widely accepted, namely: a theorem/proposition/lemma is an assertion with a (valid) proof, a conjecture one without but also without a counter example and an obligation is an assertion on which a proof depends. Further semantics can then be specified (informally) by the CoP that uses OMDoc. Maybe one could even allow the document ontology to be extendable (compare to the MMiSS project). It is already modularized, so one could allow additional modules to be added by the CoP that adapts OMDoc to its purposes. Reasoners could make sure that the extension does not contradict the document ontology and templates could be provided to easily extend. Just an idea. --Mbroecheler 23:51, 17 April 2007 (CEST)
2. What is a Rule? It occurs in the XML schema, but is not documented in the book.

Limits of description logic / rules

• Do we need rules to express certain things?

Defining Concepts

So far the ontology consists of primitive concepts only. I would propose to actually include the defintions of those concepts that can be defined in order to make the ontology more meaningful. Even for those concepts that cannot be fully defined one could introduce more defining characteristics.

For example one could state:

These are just two examples and one can easily find more. The question is rather whether those shall be added to specifiy the semantics of the document ontology in more detail.

Of course such definitions would constrain the user (the issue of consistency was already raised above). For once, one could not declare a theorem without giving a proof (even if one wanted to supply a proof later). On the other hand such an ontology would improve consistency checking significantly (e.g. uups, we forgot to include the proof of a theorem).

As for introducing strong and weak inconsistencies (this point was raised above but applies in this context as well) I would like to remark that OWL does not support such distinctions. If an OMDoc document populates the KB with instances that are inconsistent with the document ontology, the reasoner is going to indicate that there exists an inconsistency and will halt (after all there cannot be a model). I am not aware that one can tell any reasoner that the encountered inconsistency is a weak one and should therefore be ignored. One way around this might be using the annotation in OMDoc. One could use the Dublin core meta data to indicate that some elements of the document are currently being worked on (via status for instance). When the document instance is then added to the KB (and with it all its element instances), those elements under construction could be first ignored and then later added. This way one could determine whether these elements cause inconsistencies and then determine how to react. What I am saying basically boils down to some sort of preprocessing before the reasoning/consistency checking phase and leaving the ontology as strict as it is but having other mechanisms of introducing weak inconsistencies. --Mbroecheler 01:37, 18 April 2007 (CEST)

I did not mean to have one ontology with both strong and weak constraints, but rather two separate variants of the ontology: One with strong constraints, the other one without. Applications decide on demand, which one to use. Technically, you could probably run two reasoner instances on your knowledge base – one with the strong ontology loaded (e.g. for validating the knowledge base), and the other one with the weak ontology loaded for everything else (e.g. general editing in a wiki, where temporary inconsistencies should not break the whole system). Anyway, I also like your DC metadata approach! --Clange 12:01, 18 April 2007 (CEST)

has-definition functional?

• The has-definition role is classified as functional but isn't it also possible to provide alternative defintions for symbols which are equivalent (for didactic purposes or for completeness)? --Mbroecheler 00:32, 18 April 2007 (CEST)
  • Yes, it is, but then you have to use the alternative element instead of definition. That is, has-definition is indeed functional, but we might consider modeling it as a subproperty of has-definition-or-alternative-definition (sorry, can't imagine a better name now), which is not functional. (BTW, I renamed this section. I don't think that there are major and minor concerns in this early phase ;-) --Clange 11:21, 18 April 2007 (CEST)

Omtext, Omgroup, OmDoc

Should omtext and omgroup be included in the document ontology? I know that they are sort of residual classes and do not carry any interesting semantics, but for completeness they could be included. I was thinking that if an author writes a mathematically significant statement inside an omtext (because s/he does not know better) than this could still be captured in the document ontology (and it could be referred to from the content ontology which is what I am currently working on). --Mbroecheler 22:49, 28 April 2007 (CEST)

Great idea! So far, I have not dealt with them because they were not interesting for me – but they are. At least omtext is very interesting, as it can be typed as any kind of statement (see §14.3 in the OMDoc book). That is, an <omtext type="definition"> has the same semantics as a definition element. That is, it can be represented by the Definition class of the ontology without adding anything. If we want to stick closer to the XML schema (what do you think?), we might consider introducing two subclasses of Definition, namely FormalDefinition (i.e. the definition element) and InformalDefinition (i.e. omtext). That might be interesting w.r.t. the SWiM service interface, if we think of a "formalizer" assistant. --Clange 22:52, 1 May 2007 (CEST)

How about including a class OMDocDocument which then contains OMDocConcept? From that perspective we could also import the dublin core and creative commons ontology and establish the relations/properties defined in there on the OMDocDocument class. So we could have tripples like: OMDocDocument dc:author String --Mbroecheler 22:49, 28 April 2007 (CEST)

Makes sense. At least for everything except SWiM, where documents are broken down to the statement level and most of the DC metadata are handled by the wiki. But introducing a document class would certainly help the ontology to stick closer to the document structure, which does make sense for some applications. Thanks! --Clange 22:52, 1 May 2007 (CEST)