Named sentences

[tillmo]

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

[CL-mailing-list]

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]

1. Can you (or anyone) suggest a reasonable CLIF-stye syntax for associating a name with a sentence?
2. Can a sentence name be any string, or are there any restrictions (eg to URIs or IRIs, for example)? What motivates the restrictions?
3. 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]

Pat,

1. e.g. (cl-name "commutativity" (forall (x y) (= (+ x y) (+y x))))
2. 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).
3. 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]

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]

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,

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

2. 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).

3. 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/Named sentences #44#issuecomment-12543053.

---

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

[greenTara]

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]

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

[greenTara]

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

[tillmo]

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]

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]

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]

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]

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]

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]

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.