Named sentences - Githubissues

tillmo commented 11 years ago

Provide a possibility to name sentences. This is essential for keeping the overview when using a theorem prover with large theories.

CL-mailing-list commented 11 years ago

On Jan 21, 2013, at 16:37 , Till Mossakowski notifications@github.com wrote:

Provide a possibility to name sentences. This is essential for keeping the overview when using a theorem prover with large theories.

Second this. And better yet if there is a way to tie names to documents, although this might start to look like creep toward something like DOM.

.bill

Bill Andersen Highfleet, Inc. (www.highfleet.com) 3600 O'Donnell Street, Suite 600 Baltimore, MD 21224 Office: +1.410.675.1201 Cell: +1.443.858.6444 Fax: +1.410.675.1204

CL-mailing-list commented 11 years ago

Can you (or anyone) suggest a reasonable CLIF-stye syntax for associating a name with a sentence?
Can a sentence name be any string, or are there any restrictions (eg to URIs or IRIs, for example)? What motivates the restrictions?
Does a sentence name denote the sentence? Is this a semantic requirement on interpretations? Or is the sentential "naming" done outside the logic altogether?

Pat

On Jan 21, 2013, at 3:37 PM, Till Mossakowski wrote:

Provide a possibility to name sentences. This is essential for keeping the overview when using a theorem prover with large theories.

— Reply to this email directly or view it on GitHub.

CL mailing list CL@philebus.tamu.edu http://philebus.tamu.edu/cgi-bin/mailman/listinfo/cl

IHMC (850)434 8903 or (650)494 3973
40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 mobile phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes

tillmo commented 11 years ago

Pat,

e.g. (cl-name "commutativity" (forall (x y) (= (+ x y) (+y x))))
I would say any string. Typically, these strings are used in a theorem prover for displaying lists of sentences in a succinct way, so these strings are usually shorter than the sentences themselves (and typically not (long) IRIs).
The naming is done outside the logic. It is similar to cl-comment, but with the focus on concisely naming sentences for easy reference (whereas comments are usually longer explanations)

greenTara commented 11 years ago

In XML, such naming is typically done with an @id or @xml:id or @xyz:id attribute. The label is an xs:NCName (text string with no colons, plus a few other restrictions). An IRI is constructed by appending this label to the base IRI as a fragment identifier (after #).

This is a pattern that should be familiar to many people. It would be nice if the CLIF syntax could have a similar flavor.

(and (cl:id 'sent1') (P x) (Q y))

or, using a more general embedded comment syntax

(and (cl:comment (cl:id 'sent1')) (P x) (Q y))

CL-mailing-list commented 11 years ago

Dear Till,

Could not one achieve the same functionality by naming the axiom using the module construct? In this way, we do not need to change anything in the current CL, though it might lead to a proliferation of cl-imports...

I recall that I was doing this when writing axioms for mathematical structures.

Best, Ali

On Tue, Jan 22, 2013 at 1:52 PM, Till Mossakowski notifications@github.comwrote:

Pat,

e.g. (cl-name "commutativity" (forall (x y) (= (+ x y) (+y x))))

I would say any string. Typically, these strings are used in a theorem prover for displaying lists of sentences in a succinct way, so these strings are usually shorter than the sentences themselves (and typically not (long) IRIs).

The naming is done outside the logic. It is similar to cl-comment, but with the focus on consicesly naming sentences for easy reference (whereas comments are usually longer explanations)

— Reply to this email directly or view it on GitHubhttps://github.com/gruninger/Common-Logic/issues/44#issuecomment-12543053.

CL mailing list CL@philebus.tamu.edu http://philebus.tamu.edu/cgi-bin/mailman/listinfo/cl

greenTara commented 11 years ago

It is not possible to use the module construct inside a compound sentence, while a more general identification functionality could identify sentences inside, say, a disjunction or implication. It could also be used to identify terms inside literals.

tillmo commented 11 years ago

Also, the module construct carries a certain semantics, and I do not want this here. I want just to name a sentence.

greenTara commented 11 years ago

When you say 'name', would the name be in the universe of reference?

tillmo commented 11 years ago

When you say 'name', would the name be in the universe of reference? I would prefer not. After all, comments are not in there either, are they?

greenTara commented 11 years ago

You are correct - comments have no semantic effect. But calling it a 'name' may lead to confusion. Could we call it an 'identifier', or more emphatically an 'extralogical identifier'?

tillmo commented 11 years ago

I do not care much, but "identifier" also may lead to confusion, since usually identifiers occur in the semantics (and denote objects). Perhaps "label"?

greenTara commented 11 years ago

Label is fine. In general I agree with John Sowa's comment on the email list http://philebus.tamu.edu/pipermail/cl/2013-January/002852.html regarding structured comments. However, the label of a sentence is a special case. Once you have the sentence labelled with an IRI, you can use RDF within the existing CLIF comment syntax to express additional information about that sentence. I would call that a structured comment.

CL-mailing-list commented 11 years ago

We could follow earlier CL usage and call them 'markers'. I don't see any reason to quote the name, by the way.

Tara, I don't like your embedded syntax, at least in CLIF. Could we follow the cl-comments idea and have the syntax enclosing the expression? So have

(cl:id sent1 (and (P x)(Q y)))

rather than

(and (cl:id 'sent1') (P x)(Q y))

?

Pat

On Jan 22, 2013, at 7:51 AM, Till Mossakowski wrote:

I do not care much, but "identifier" also may lead to confusion, since usually identifiers occur in the semantics (and denote objects). Perhaps "label"?

— Reply to this email directly or view it on GitHub.

CL mailing list CL@philebus.tamu.edu http://philebus.tamu.edu/cgi-bin/mailman/listinfo/cl

IHMC (850)434 8903 or (650)494 3973
40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 mobile phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes

greenTara commented 11 years ago

If that's what CLIF users want, go for it. Personally, I much prefer an embedded comment syntax because it doesn't cover up subtypes. That is, a sentence with a comment can still be recognized as a conjunction, negation etc without burrowing in through potentially nested comments. This is critical for constructing subdialects, such as Horn logic, etc. However, this is more relevant to another issue, #26 I didn't mean to bring it up here, it just popped out that way.

fabianneuhaus commented 11 years ago

CLIF currently allows embedded comments. Do you suggest to change that? Fabian

On Jan 22, 2013, at 3:48 PM, CL-mailing-list wrote:

We could follow earlier CL usage and call them 'markers'. I don't see any reason to quote the name, by the way.

Tara, I don't like your embedded syntax, at least in CLIF. Could we follow the cl-comments idea and have the syntax enclosing the expression? So have

(cl:id sent1 (and (P x)(Q y)))

rather than

(and (cl:id 'sent1') (P x)(Q y))

?

Pat

On Jan 22, 2013, at 7:51 AM, Till Mossakowski wrote:

I do not care much, but "identifier" also may lead to confusion, since usually identifiers occur in the semantics (and denote objects). Perhaps "label"?

— Reply to this email directly or view it on GitHub.

CL mailing list CL@philebus.tamu.edu http://philebus.tamu.edu/cgi-bin/mailman/listinfo/cl

IHMC (850)434 8903 or (650)494 3973 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 mobile phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes — Reply to this email directly or view it on GitHub.

greenTara commented 11 years ago

For clarification, an embedded comment is attached to the thing that wraps it, while a wrapped comment is attached to the thing that is embedded in it. In this sense, CLIF has wrapped comments with nesting, and XCL has, and will continue to have, embedded comments with nesting.

CL-mailing-list commented 11 years ago

On Jan 25, 2013, at 12:27 PM, Tara Athan wrote:

For clarification, an embedded comment is attached to the thing that wraps it, while a wrapped comment is attached to the thing that is embedded in it. In this sense, CLIF has wrapped comments with nesting, and XCL has, and will continue to have, embedded comments with nesting.

Wouldn't it be natural to have comments as XML property values, as in

...

? Or is there some XML reason to not do this?

Pat

— Reply to this email directly or view it on GitHub.

CL mailing list CL@philebus.tamu.edu http://philebus.tamu.edu/cgi-bin/mailman/listinfo/cl

IHMC (850)434 8903 or (650)494 3973
40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 mobile phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes

greenTara commented 11 years ago

In XML, it is not natural to put comments as attributes. How would such comments be nested? How would comments with XML markup (HTML, RDF, CL, etc) be rendered?

However, as I mentioned above, labels are typically attached with attributes (illustrative syntax only)

<xcl:Atom id="sent1">
 ...
</xcl:Atom>

Note: there is an issue, #26, for the general discussion of annotation..

fabianneuhaus commented 11 years ago

In http://philebus.tamu.edu/pipermail/cl/attachments/20130204/f2437179/attachment-0001.pdf a identifier mapping (the name might be changed to "label mapping" or "marker mapping") is introduced for the purpose of handling the semantics of named/labeled texts and import statements. It is not obvious to me whether the intended semantics for labeled sentences is significantly different from the semantics for labeled texts or just mere syntactic sugar.

For example, is this (cl:id sent1 (and (P x)(Q y))) logically equivalent to (cl:txt (cl:import sent1) (cl:baptise sent1 (cl:txt (and (P x)(Q y) ))) ) ?

fabianneuhaus commented 11 years ago

Pat wrote:

Does a sentence name denote the sentence? Is this a semantic requirement on interpretations? Or is the sentential "naming" done outside the logic altogether?

I we treat labels of sentences as syntactic sugar in the way I suggested in my last email, the entity that is really labeled is a text. The labeling happens within the logic in the sense that the function that relates labels to texts is part of the interpretation. But it is a different function than the function that associates names with individuals in the universe of reference, so the same string be used as name and as label (marker, identifier ...)

We might want to add a special predicate that ensures that the label refers to the same thing as the corresponding name. Let's call it "cl:textlabel". It has the following truth-condition (cl:textlabel name) is true with respect to interpretation I iff int_I(name) = im_I(name)

This would allow to write things like

(cl:textlabel foo). (cl:baptise foo (cl:txt (bar))) (authorOf foo fabian) (versionOf foo 2.01)

greenTara commented 11 years ago

It should be possible to label sentences without naming a text. We often want to label a sentence that is part of a compound sentence. This labeling is not intended to allow the sentence to be imported. (Recall that we do not allow an importation to be part of a compound formula.)

Instead it is (often) intended to name it as an entity for use in metadata assertions. These are very different functionalities and should be kept separate, imho. If some user, or some dialect, wants to conflate them, that is their business, but it shouldn't be part of the CL abstract syntax/semantics.

Another argument, which may or may not be persuasive, depending on your perspective, is that keeping them separate allows us to remain neutral on httpRange-14. Here's an example we can use/expand on for further discussion:

(cl:id "http://example.org/myText"
  (cl:txt 
    (authorOf "http://example.org/myText" tara) 
    (authorOf "http://example.org/myText#prem1" fabian) 
    (cl:baptize "http://example.org/myText#Dog" 
      (forall (x) 
        (if
          (cl:id "http://example.org/myText#prem1"
            (http://example.org/myText#Dog x)
          )
          (http://example.org/myText#Animal x)
    ) ) )
    (baptize "http://example.org/myText#Cat" 
     (forall (x) 
        (if
          (cl:id "http://example.org/myText#prem2"
            (http://example.org/myText#Cat x)
          )
          (http://example.org/myText#Animal x)
) ) ) ) )

fabianneuhaus commented 11 years ago

Okay. So what is the intended semantics of (cl:id foo (cl:txt (bar))

In particular, is there any interpretation that satisfies (authorOf foo fabian) (cl:txt (bar) but not (authorOf foo fabian) (cl:id foo (cl:txt (bar))

And -- from a CL perspective -- is there any difference between the following examples (cl:id foo (cl:txt (bar)) (cl:id http://example.org/myfoo (cl:txt (bar)) (cl:id http://example.org/myfoo#Dog (cl:txt (bar)) except that they involve different strings.

greenTara commented 11 years ago

I'll answer the last question first - ignoring the possibility of prefixing, I don't expect any difference between the last three texts except for the different strings.

On the first question, if we claim (as has been expressed above "The naming is done outside the logic. It is similar to cl-comment") that an identifier on an expression is like a comment - it has no (CL) semantic effect, then any CL interpretation that satisfies

(authorOf foo fabian)
(cl:txt (bar)

also satisfies

(authorOf foo fabian)
(cl:id foo (cl:txt (bar))

It would be necessary to have an extension of CL semantics in order to enforce that the denotation of "foo" has anything to do with (cl:txt (bar)). It's up to individual dialects to make that happen, if they wish.

From that point of view, it was somewhat silly of me to include the sentences that use the identifiers as names in the same text. It would make more sense to put those sentences in comments, possibly in a completely different syntax (e.g. RDF or some structured comment format).

fabianneuhaus commented 11 years ago

In this case I propose to shelf this issue until we have a solution for structured comments. Afterward we can reconsider the idea to use structured comments for the purpose of naming sentences.

gruninger / Common-Logic

Named sentences #44