*Coq* seems to be a widely used proof assistant language with lots of examples of use.
A recent proof system I've seen written about is *Imandra* [ https://www.imandra.ai/ ] which has been applied to the Monte Hall problem [ https://medium.com/imandra/reasoning-about-probabilities-in-reasonml-2b43bf01873e ]. As for theorem provers for modal logics, there's some reference to such in *Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers* [ http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf ] - pt On Sunday, November 25, 2018 at 12:12:18 PM UTC-6, Mark Buda wrote: > What I did at the time was write a Monte Carlo simulation. I don't know > any of those languages well enough to do anything useful with them yet. > > I want to use one of the proof assistant languages for some the AGI stuff > I am trying to work on, but I am not sure yet which one best suits my > needs. I don't know enough about them or my needs to decide yet. I am > leaning towards Coq, but if I find something that looks like it plays > better with modal logic that might sway me. > > I have to finish some poorly thought out OAuth2 code before I have enough > data sources working that I can turn my attention to how I think the system > I am trying to build should reason about those data sources. > > At that point, I will want to write statements about the data sources, and > will need to pick a language in which to write those statements. > -- > Mark Buda <[email protected] <javascript:>> > I get my monkeys for nothing and my chimps for free. > > > On Sun, Nov 25, 2018, 11:27 AM Philip Thrift <[email protected] > <javascript:> wrote: > >> >> On the other hand, some say you really don't understand something unless >> you can write a program that encodes that understanding. >> >> Can you encode your understanding of the Monte Hall problem in a >> "logical" (or proof assistant) language? >> >> - pt >> >> On Sunday, November 25, 2018 at 10:11:08 AM UTC-6, Mark Buda wrote: >>> >>> When presented with the Monty Hall problem, I could not understand it >>> without writing a program to help me. I guess that puts me in the good >>> company of Paul Erdos, according to Wikipedia... >>> -- >>> Mark Buda <[email protected]> >>> I get my monkeys for nothing and my chimps for free. >>> >>> On Sat, Nov 24, 2018, 6:58 PM John Clark <[email protected] wrote: >>> >>>> On Sat, Nov 24, 2018 at 5:01 PM Brent Meeker <[email protected]> >>>> wrote: >>>> >>>> *> The best intuition pump to solve the Monte Hall problem is to >>>>> imagine that there are 100 doors and Monte opens all the doors except the >>>>> one you chose and one other....do you switch?* >>>> >>>> >>>> 3 doors will do. If you follow the switch strategy the only way you >>>> would end up losing is if your original guess was correct, and there was >>>> only one chance in 3 of that, so if you switch you have 2 chances in 3 of >>>> winning. >>>> >>>> John K Clark >>>> >>>> >>>>> >> -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
