[04:23] <dmiles> I was trying to format that to..
[04:23] <dmiles> (implies (and (dateOfEvent ?EVENT ?DATE) (ist-Asserted ?MT (organismKilled ?EVENT ?ORGANISM)))
[04:23] <dmiles>          (ist (MtSpace ?MT (MtTimeWithGranularityDimFn (IntervalStartedByFn ?DATE) TimePoint))
[04:23] <dmiles>              (preventsFromPlayingRoleInType ?EVENT ?ORGANISM deliberateActors Event)))
-
* Flood protection: 1 message(s) in queue
-
* Flood protection: 0 message(s) in queue
-
[04:24] <dmiles> That is a rule used in the proof that means: "if an organism is killed in an event, then forever after this event the organism is prevented from being a deliberate actor in any other (future) event. "
[04:29] <dmiles> what my question was is if this system of logic is a completely separate thing than what is sudied by students studying mathematical logics
[04:31] <dmiles> for years my assumption has been that this was not a separate field
[04:32] <dmiles> but the last 5 years I have not seeing anything like this creep into Coq/Isabelle
[04:33] <ski> i think Coq and Isabelle are more oriented towards math
[04:34] <dmiles> So my new assumption is despite this being a computational logic system designed for mechanical reasoning it is not yet considered an everyday sort of thing
[04:35] <ski> i don't know enough about this use of logic to be able to tell what it's more closely related to
[04:36] <ski> from what i understand, it appears to be a variant of (single-sorted, i think) predicate calculus, with (i think) modal constructions
[04:36] <ski> perhaps also other novel features
[04:37] <ski> (and then i'm thinking of "logical" issues (whatever that is exactly), rather than ontological ideas (which i don't understand well) about how to structure knowledge)
[04:37] <dmiles> 1-sort but also could be called unsorted
[04:38] <ski> *nod*, the same thing
[04:40] <dmiles> Ontology is used by this logical system in order to create a vocabulary so logicains can understand the terms used in proofs
[04:40] * pie___ is now known as pie_
[04:41] <dmiles> (so when new posits, theorems and axioms are created they can be aligned with the system)
[04:43] <dmiles> so we know that (IntervalStartedByFn ?TimePoint)  takes a TimePoint and constructs an interval beganning at that
[04:43] <dmiles> (Is a TotalFunction over TimePoints)
[04:48] <dmiles> also ontologies help us know that "(and (deliberateActors ?Situation ?Agent) (holdsIn ?Situation ?Truth))" quantifies over an infinate number of possible ?Truth deductions for a given ?Situation involving the ?Agent
[04:50] <ski> mhm
[04:50] <dmiles> So ontology, specifically Ontological Engineering is about creating a universal language that can be reasoned with by computers
[04:54] <dmiles> I should say that it is only partly related to artificial intelligence.. when it merely is a tool to allow computers to do usefull constructions and calculations that machines are good at
[04:55] <dmiles> (saying there isnt anything AI-ish or probabilistic or philosophical about this logic)
[04:57] <dmiles> Just somehow this sort of engineering of logical reasoning has perhaps seems too futuristic
[04:59] <dmiles> But Ontology is the only possible pathway to getting computers to understand how to construct new software based on changing human needs
[05:00] <dmiles> at least in a completely human understandble manner
[05:02] <dmiles> yet there are 10,000 people working on other logics in which i dont understand how they can be usefull :)
[05:03] <dmiles> I mean i dont understand what the end usage of a logic of mathematics
[05:04] <dmiles> unless it is a segway to get to the logic of Ontology
[05:04] <dmiles> (which is the only thing that makes any sense)
[05:41] <dmiles> it also makes sense to me that I am taking way too long writting the software that does ontological processing.. i am jsut one person and it is not easy to do
[05:42] <dmiles> but it makes no sense as to why there isn't already 10 impls of the logic
[05:53] <dmiles> The only conclusions i am able to come to is: 1) Cycorp has be faking its results to the us govt for 35 years.  OR  2) no one besides a small handfull of people (less than 100) even know it is possible to do this kind of logic on computers
[05:54] <dmiles> Which both conclusions are wildly improbable
[05:54] <dmiles> Is there another explaination?