[ontoiop-forum] DOL finalisation

[rick]

Danke, Till.

On 01/05/2018 06:00 AM, Till Mossakowski wrote:
> Rick,
> 
> Am 05.01.2018 um 01:18 schrieb rick:
>> Thanks Till for taking the time to answer my questions.
>>
>> I remain unconvinced that an institution that's not in the proposal is
>> in scope.
>>
>> More important though is whether an institution of "second order logic"
>> exists. 
> yes, it does. See p.415 bottom of my paper
> T. Mossakowski.  Relating CASL with Other Specification Languages: the
> Institution Level.
> Theoretical Computer Science, 286:367-475, 2002.

Could you please provide the reference to the institution of "second
order logic" in the following paper?

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.401.2100&rep=rep1&type=pdf

I could not following the pagination from the reference you provided.

> 
>> And whether the required mapping from the abstract syntax of OMS
>> to the signatures and sentences of "second order logic" exists. right?
> Hets provides an abstract syntax for second-order logic (as part of the
> CASL logic). The mapping to the institution is easy.

Where is the mapping?

>>
>> Just to be sure, when you say "second order logic" you mean Henkin
>> Semantics, right?
> no, in my paper, I used standard semantics, which I need for translating
> first-order logic with induction to second-order logic (see p.429 of my
> paper). With Henkin semantics, it is not possible to specify inductive
> datatypes (like natural numbers, lists, trees etc.) in a monomorphic
> (i.e. unique up to isomorphism) way.

Thanks.

>> I will enjoy reading the reference on type class polymorphism.
>>
>> Do you claim the paper contains the institution and the mapping? It
>> seems not as the paper predates (2004) DOL.
>>
>> If not, could you please provide a pointer?

The institution for "second order logic" is in the "Relating CASL"
paper, but not the typeclass polymorphism paper, right?

>> I briefly scanned the paper. Looks like a great paper.
> This paper (cited in my previous email) contains an institution for
> polymorphic higher-order logic, but not for system F.

Yes. Understood.

I have read a few sections, but need to spend more time.

> It does not
> contain any logic translations, except from a technical one linking two
> variants of the same logic.

> Best, Till
> 
> 
> 
> _________________________________________________________________
> To Post: mailto:ontoiop-forum at ovgu.de
> Message Archives: https://listserv.ovgu.de//pipermail/ontoiop-forum
> Config/Unsubscribe: https://listserv.ovgu.de/mailman/listinfo/ontoiop-forum
> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
> Community Wiki: http://ontoiop.org
>