跳至主要内容

续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店面转转。王先生告诉记者，"作为一家大公司应该吸取经验教训，在中国 做生意，想赚中国人的钱，就更应该尊重中国人民的感情。" 王先生告诉记者，中国老百姓应该拿出一点实际行动，给这些国外公司一些警告以及反 馈信息。王先生说希望这个事件能给更多的类似企业传递更多的信息，中国人民欢迎外 企来做生意，但是前提一定是秉持公平公正的原则，尊重中国人民的感情。 -- ...
发表评论
阅读全文

分享一下在ICC工作的经验，以及contractor行业的注意事项。

http://www.mitbbs.com/article_t/JobHunting/33509585.html 发信人: poyang (), 信区: JobHunting 标  题: 分享一下在ICC工作的经验，以及contractor行业的注意事项。 发信站: BBS 未名空间站 (Fri May 22 02:28:24 2020, 美东) 最近由于疫情很多new grad同学没法上岸，很多一线大厂更是lay off出来一批大神， new grad的简历在hr眼里更是没法看了。所以很多同学都在考虑去ICC苟住身份，楼主 作为一个在icc工作了一年多的人，写下这篇帖子介绍一下ICC里的一些情况，希望在这 个非常时期帮助到各位还在找工作的同学。 1. 什么是ICC，ICC运作模式是怎么样的？ ICC是India Consulting Company 的简称主要从事科技软件行业的外包业务。现在信息 时代每个行业都要像数字化方面转型，特别是大型企业。但除了一些大型科技公司，需 要大量稳定的Full time SDE。市场上大部分的传统行业包括医疗，金融， 通信，零售 等行业也需要大量技术支持和销售业务转型，所以也需要大量的码农。但为了维持公司 (client)的灵活性，所以只招收contractor(合同工). 这样可以简化招聘流程，不需要 承担contractor的身份问题，也可以随时进行人员精简，比如现在项目结束client可以 随时开除目前的合同工并且不给任何补助，也不需要给合同工任何福利。 一般来说Client公司不能直接到市场上招contractor,需要通过第三方公司(vendor) 来 招聘合同工，vendor手上握有大量client的招聘资源，但是手上不一定有很多 candidate 来应聘这些岗位。所以就会把资源放给别的公司（比如ICC）来收取一定的 提成。正常情况下大部分的公司都会给合同工$60~$90 一小时的rate, 但会被vendor抽 掉一部分，再被icc抽掉一部分，你能拿到手可能就只剩下$40~$70一小时。这个抽成具 体取决于icc和vend...
发表评论
阅读全文

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

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月份表示，...
发表评论
阅读全文