[ontoiop-forum] [ontolog-forum] Re: DOL finalisation

[Pat Hayes]

Hi Till

I understand (and respect) your preference for 2OL over infinitary for prover-relevant reasons, but the mapping to Lw1w is semantically exact, so should be mentioned for purposes of classifying the logics in expressivity terms. I was only vaguely aware of the FOL+induction work, but again I doubt if this gives an exact mapping of CL, since CL does not impose minimality of fixedpoints in its definitions. Of course, that often arises as a side-effect of the behavior of reasoners; but again, it is not a semantic condition. 

Still, all this is terminology-niggling, and does not really impinge on the excellent work of you and your colleagues on DOL. Congratulations on the latter, and on achieving standardization. I know how large and determined an effort this represents. 

Best wishes

Pat 

> On Dec 21, 2017, at 3:20 PM, Till Mossakowski <till at iks.cs.ovgu.de> wrote:
> 
> Dear Pat,
> 
> the expressivity of CL is more precisely captured as "first-order logic
> with induction", which recently has gained interest in the theorem
> proving community [1]. The latter can be embedded both into second-order
> logic and into infinitary first-order logic. For me, infinitary
> first-order logic is much worse to handle than second-order logic: due
> to the infinitary nature, there won't be any theorem provers, even with
> your restriction to axioms. Therefore, in our graph, we only show the
> connection to second-order logic, which has theorem proving support
> (take any higher-order prover like Leo, Satallax or Isabelle).
> 
> Best, Till
> 
> [1] Koen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone: TIP:
> Tons of Inductive Problems. CICM 2015: 333-337
> http://www.cse.chalmers.se/~jomoa/papers/cicm15-TIP.pdf
> https://tip-org.github.io/
> 
> Am 20.12.2017 um 23:32 schrieb Pat Hayes:
>> I hadn’t seen that diagram before. I believe that it is inaccurate to describe CL as having ‘some second-order constructs’. Sequence markers take CL outside FO expressivity, but not to second-order. CL with sequence markers is in fact a subset of the infinitary logic Lw1-w which allows countably infinite conjunctions. This is a long way short of full second-order logic. If one restricts CL (Lw1-w) so that sequence markers (infinite conjunctions) occur only on the LHS of sequents, it is first order. So sequence makers can be used in ontologies (ie as ‘axioms’) without going beyond FO expressivity. 
>> 
>> Pat
>> 
>>> On Dec 20, 2017, at 7:01 AM, John F Sowa <sowa at bestweb.net> wrote:
>>> 
>>> Congratulations to everyone working on the DOL project.
>>> 
>>> From Fabian via ontoiop-forum,
>>>> Good news concerning the standardisation of DOL! During the last
>>>> OMG Technical Meeting the Architecture Board approved the changes
>>>> that we made to DOL during the “Finalisation Phase” (which in our
>>>> case lasted 2 years). Hence, we cleared the last major hurdle on
>>>> our way to the release of DOL 1.0. I expect that this will happen
>>>> in February 2018.
>>> And Fabian, I'm sending a copy of this note to Ontolog Forum, and
>>> I also attached a copy of an earlier diagram (dol.jpg).
>>> 
>>> Does this diagram reflect the current version?  If so (or not),
>>> could you please send the URL of the latest documentation to
>>> Ontolog Forum?
>>> 
>>> And is software available for the various mappings in that diagram?
>>> 
>>> John
>>> <dol.jpg>
>>> _________________________________________________________________
>>> 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
>> 
> 
> 
> 
> -- 
> All contributions to this forum by its members are made under an open
> content license, open publication license, open source or free software
> license. Unless otherwise specified, all Ontolog Forum content shall be
> subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
> --- You received this message because you are subscribed to the Google
> Groups "ontolog-forum" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to ontolog-forum+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
> 
> -- 
> All contributions to this forum by its members are made under an open
> content license, open publication license, open source or free software
> license. Unless otherwise specified, all Ontolog Forum content shall be
> subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
> --- You received this message because you are subscribed to the Google
> Groups "ontolog-forum" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to ontolog-forum+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
> 
> 
> _________________________________________________________________
> 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