This approach sounds like "expert systems" ( https://en.wikipedia.org/wiki/Expert_system) from 80's AI. My understanding is that it's more or less discredited these days, and machine learning systems have little to no resemblance to expert systems. That is not to say that ML is necessarily better, in particular when it comes to deliberate exploitation, but the data is on their side - ML approaches are far more effective on real world problems with much less human intervention (which is important because that means they scale better). An expert system requires you to collect the knowledge of a lot of experts, which is time consuming, and the result is still exploitable (after all, the legal system is essentially one big expert system and it's full of loopholes).
So for my part, although I find ML to be philosophically unsatisfactory when it comes to explainability, when we are doing large scale numbers games like diagnosing disease, I would rather put my life in the hands of a well trained ML system than a simplistic model with some logical deduction abilities. On Sun, Mar 29, 2020 at 8:30 PM José Manuel Rodríguez Caballero < [email protected]> wrote: > David A. Wheeler wrote: > >> But I don't see how to match proof tools to this problem at this time. >> I'd be delighted to be proven wrong :-). > > > One way may be to develop a really huge set of propositions, which are > "medically true" (maybe using a combination of modal logic, deontic logic, > and many other logical systems at the same time). For example, > (1) If the patient has a bacterial infection and the patient is not > allergic to antibiotics then it should take antibiotics. > > Using (1) we cannot prescribe antibiotics as a treatment to a person who > is infected by a virus and has no symptoms of bacterial infection. There > are many people out there who do not know this and think that COVID-19 can > be cure using penicillin. Using a proof assistant with a set of "medically > true" propositions these people can not derive the fake statement: > > (2) If the patient has COVID-19 then the patient should take antibiotics. > > Of course, there are cases when COVID-19 and is accompanied by a bacterial > infection, but this is not the same as (2). One of the goals of a proof > assistant is to avoid writing stupidity and for many people, including > myself, it is easy to write stupidity about medicine, because it is beyond > our field of expertise. So, having a proof assistant with a really huge > library of medically true statements may be the only way to guide us in the > absence of a medical doctor as in the current situation (as a Millenial, I > think that I am young enough to survive the COVID-19 if I get it in the > near future, but it is important to think about the boomers out there). > > Another medically true proposition may be: > > (3) If the patient is secreting green fluid by his/her nose, then the > patient has a bacterial infection. > > Using (1) and (3) the patient can deduce by himself/herself: > > (4) If the patient is secreting green fluid by his/her nose, then the > patient should take antibiotics. > > I am not claiming that this approach is scalable. This is just > brainstorming. > > Kind regards, > José M. > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAA8xVUgr%3DfRxRiyfGN2PaUALfVK%2B_sTwnD4U3hU%3DAa4tEeWVZw%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAA8xVUgr%3DfRxRiyfGN2PaUALfVK%2B_sTwnD4U3hU%3DAa4tEeWVZw%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsFsrPVaUPpxvhyDnTaX_juNEFVwUaBTN%3D8-vsJttEKHQ%40mail.gmail.com.
