跳至主要内容

续a decision......


http://www.mitbbs.com/article_t/Programming/31572287.html

发信人: ReedToBe (ReedToBe), 信区: Programming
标  题: 续a decision......
发信站: BBS 未名空间站 (Sun May 31 02:01:46 2020, 美东)

此帖之前的话都是为了说平面几何形式化之后是完备的，其判定程序的复杂度是NP-
hard的。涉及到Herbrand基，Buchberger算法，Tarski关于实闭域的判定定理都是论证
引出来的。

补充点东西，当然是网上现成的，google来比自己写省劲，叫科里-霍华德同构定理，
又可叫数学证明（形式化的，可看作以符号逻辑写成的证明）和计算机程序(自动化)的
等价性定理：
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence

我决心自言自语，把这个帖子涉及的自动证明相关的东西都google了来，:)
--

评论

发表评论

此博客中的热门博文

记者探访H&M实体店，店员：我们也爱国，希望明天就关门

http://www.mitbbs.com/article_t/ChinaNews/32684337.html 发信人: jiuna (), 信区: ChinaNews 标  题: 记者探访H&M实体店，店员：我们也爱国，希望明天就关门 发信站: BBS 未名空间站 (Thu Mar 25 02:55:55 2021, 美东) 3月25日中午，《环球时报》记者走访了北京市三里屯核心商区，探访新疆棉事件对H&M 及Nike等品牌实体店的影响。记者发现，在整整占据了三层的北京最大的H&M店之一的 店铺内，顾客稀少，门可罗雀，一些路人进店挑选后也选择不购买其产品即离开。 "看到了H&M和Nike的声明之后，近期不会再购买他们的产品了。既然想在中国做生意 ，还侮辱中国人，那中国人肯定不会支持，"一位路人在接受《环球时报》采访时表示 。"抵制他们的产品对我们并不会产生什么影响，因为替代产品有很多。国内很多品牌 都有很好的设计和质量，大多数时间也都在网上逛淘宝，样式和质量都比H&M好很多， "一位姓赵的北京居民表示。 在接受采访时，一些路人表示，除非H&M展现出道歉的诚意，否则将来也不会再选择这 个品牌。 位于上海某繁华商业街的一家HM店，今天门口有保安值守，店员十分警戒，不让记者拍 摄。两名店员对《环球时报》记者表示他们也希望明天就关店，也不希望发生这样的事 情，他们也是爱国的，但他们只是店员，希望得到记者理解。 王先生是一位在上海南京西路附近上班的打工族，由于听到关于HM的消息，他特地在午 休时间来HM店面转转。王先生告诉记者，"作为一家大公司应该吸取经验教训，在中国 做生意，想赚中国人的钱，就更应该尊重中国人民的感情。" 王先生告诉记者，中国老百姓应该拿出一点实际行动，给这些国外公司一些警告以及反 馈信息。王先生说希望这个事件能给更多的类似企业传递更多的信息，中国人民欢迎外 企来做生意，但是前提一定是秉持公平公正的原则，尊重中国人民的感情。 --
发表评论
阅读全文

应该等Novavax疫苗么？辉瑞和moderna有什么显著副作用么？

http://www.mitbbs.com/article_t/Biology/32113013.html 发信人: james1007 (bondjames), 信区: Biology 标  题: 应该等Novavax疫苗么？辉瑞和moderna有什么显著副作用么？ 发信站: BBS 未名空间站 (Thu Mar 25 01:14:24 2021, 美东) 应该等Novavax疫苗么？辉瑞和moderna有什么显著副作用么？ 自己是中年，父母65，现在面临选择 1_虚无飘渺的等Novavax? 2_另外是否考虑强生的，貌似强生虽然有效率貌似不高，但是副作用小很多，至少不会 紫癜那么夸张的案例。另外强生貌似实验室已经有变种了，所以数据貌似不如辉瑞和 moderna 3_尽量选择辉瑞或者moderna 本人一直认为AP秒杀码工。来这里就是问医药生物大牛，所以说出都差不多等结论，就 有点业余了... 期待惊艳最优化后的建议，才不枉我对这版的信心。谢谢！ --
发表评论
阅读全文

汽车芯片巨头工厂失火 全球供应链雪上加霜

http://www.mitbbs.com/article_t/Automobile/36217659.html 发信人: carkong (千里马), 信区: Automobile 标  题: 汽车芯片巨头工厂失火 全球供应链雪上加霜 发信站: BBS 未名空间站 (Thu Mar 25 01:35:48 2021, 美东) 一家全球主要汽车芯片生产商的一个工厂发生火灾，令已因芯片短缺而减产的汽车厂商 雪上加霜。 上周五的大火导致这家工厂一片区域的设备被烧焦。该工厂位于东京东北方向的 Hitachinaka，隶属于瑞萨电子（Renesas Electronics Co. , 6723.TO , RNECY）的一家 子公司。瑞萨电子表示，至少需要一个月时间才有可能重新启动受损的业务。 日本三大主要汽车生产商的股价周一均下跌超过3%，跌幅大于整体市场，而瑞萨电子的 股价下挫4.9%。这三家汽车厂商包括丰田汽车公司（Toyota Motor Corp., 7203.TO ） 、日产汽车（Nissan Motor Co., 7201.TO ）和本田汽车（Honda Motor Co., 7267.TO ）。 瑞萨电子称，一台设备发生的一些电气问题，导致过热起火，火灾同时还污染了一些生 产半导体的无尘室。该公司表示，该工厂生产的芯片中有三分之二是汽车芯片。 瑞萨电子首席执行官柴田英利（Hidetoshi Shibata）周日称，这将对全球芯片供应产 生重大影响。 Moody's Japan的信用分析师Mariko Semetko表示，此次火灾可能会抑制 今年全球汽车生产的复苏，而汽车生产商则表示它们还在评估由此造成的影响。 柴田英利称，瑞萨电子正设法找其他生产场地弥补损失的产能，但不知道这是否可行。 该公司估算，由此造成的损失可能会高达每月1.6亿美元。 汽车制造商已经在为半导体短缺而苦恼。去年新冠疫情暴发后需求意外强势回升，在一 定程度上造成半导体供应短缺。这让工厂难以迅速增产。 福特汽车公司（Ford Motor Co., F） 2月份表示，
发表评论
阅读全文