[评论]为什么越出国越爱国？听听海外党们自己的故事

[nvod11111111]

说话要有根据。大学本科教不教这门课花两分钟查一下就知道。
（顺便说下，您这么容易就看不起人，正是暴露您自身是什么货色。
您看，像您这样满口胡喷的，俺说过俺看不起您吗？有这个必要吗？）https://www.cs.cmu.edu/~fp/courses/atp/index.html
浏览附件416377

书的介绍已经明确了是关于数理逻辑的教材，你看不懂吗？

 

[oldbei]

书的介绍已经明确了是关于数理逻辑的教材，你看不懂吗？

给您贴出来了，您都看不明白？俺不得不得相信您连搜索看来都不大会：
Foundations of Automatic Theorem Proving

 

[nvod11111111]

给您贴出来了，您都看不明白？俺不得不得相信您连搜索看来都不大会：
Foundations of Automatic Theorem Proving

神人，这是机器证明的英文吗？
您水平最高
您在哪看出吴文俊的研究与这相关啊
这混乱联系的能力，能赶上我儿子了

 

[网洋中的一条鱼]

你知道机器证明的英文是什么吗？

你是说MP吗？

 

[nvod11111111]

给您贴出来了，您都看不明白？俺不得不得相信您连搜索看来都不大会：
Foundations of Automatic Theorem Proving

再给你长点见识
数理逻辑在上世纪30年代就有了
大师中也有华人哦
是谁，看你能不能搜到
注意，是数理逻辑，不是机器证明
提示：是计算机领域的，不是数学的

 

[nvod11111111]

你是说MP吗？

我不告诉你
自己上网去查
查与吴文俊相关的
别把它跟数理逻辑混了
拜托了

 

[oldbei]

神人，这是机器证明的英文吗？
您水平最高
您在哪看出吴文俊的研究与这相关啊
这混乱联系的能力，能赶上我儿子了

这比您说机器证明还要精确。俺真同情您儿子有您这么个不学无术的父亲。自己看：
The research of Wu includes the following fields: algebraic topology, algebraic geometry, game theory, history of mathematics, automated theorem proving. His most important contributions are to algebraic topology. The Wu class and the Wu formula are named after him. In the field of automated theorem proving, he is known for Wu's method.
不能说得更明白了吧？俺真是高估了您。您要是稍微有点儿学识，就不会继续咬着这个问题不放了。

 

[网洋中的一条鱼]

我不告诉你
自己上网去查
查与吴文俊相关的
别把它跟数理逻辑混了
拜托了

这个也要上网查？

机器证明的英文翻译就是ATP（Automatic Theorem Proving），MP是我瞎写的。对不住了。

 

[未尝不可]

神人，这是机器证明的英文吗？
您水平最高
您在哪看出吴文俊的研究与这相关啊
这混乱联系的能力，能赶上我儿子了

不就是用计算机证明数学定理嘛，怎么是无关呢？
即便懂也没必要嘲笑别人，何况你也似是而非的。

 

[nvod11111111]

这个也要上网查？

机器证明的英文翻译就是ATP（Automatic Theorem Proving），MP是我瞎写的。对不住了。

这比您说机器证明还要精确。俺真同情您儿子有您这么个不学无术的父亲。自己看：
The research of Wu includes the following fields: algebraic topology, algebraic geometry, game theory, history of mathematics, automated theorem proving. His most important contributions are to algebraic topology. The Wu class and the Wu formula are named after him. In the field of automated theorem proving, he is known for Wu's method.
不能说得更明白了吧？俺真是高估了您。您要是稍微有点儿学识，就不会继续咬着这个问题不放了。

1998年，将1997年以来关于数学机械化的工作总结成书，书名为Mathematics Mechanization：Geometry Theorem Proving，Geometry Problem-Solving and Polynomial Equation-Solving将由科学出版社出版。

 

[nvod11111111]

不就是用计算机证明数学定理嘛，怎么是无关呢？
即便懂也没必要嘲笑别人，何况你也似是而非的。

我讲得是吴文俊的机器证明
他给我贴出本数理逻辑的书
你看着事实而非
我看着确不是

 

[网洋中的一条鱼]

1998年，将1997年以来关于数学机械化的工作总结成书，书名为Mathematics Mechanization：Geometry Theorem Proving，Geometry Problem-Solving and Polynomial Equation-Solving将由科学出版社出版。

你还是觉得机器证明翻译成GTP（Geometry Theorem Proving）更恰当一些？

 

[oldbei]

1998年，将1997年以来关于数学机械化的工作总结成书，书名为Mathematics Mechanization：Geometry Theorem Proving，Geometry Problem-Solving and Polynomial Equation-Solving将由科学出版社出版。

还想接着玩，俺奉陪：https://en.wikipedia.org/wiki/Mathematics_Mechanization_and_Automated_Reasoning_Platform
Mathematics Mechanization and Automated Reasoning Platform (Chinese: 数学机械化自动推理平台), or Mathematics-Mechanization Platform (MMP, code named elimino), is a group of automated theorem proving software based on an internal computer algebra system. It can be used on proving algebra and geometry theorems. This system is led by Wu Wenjun and based on Wu's method.

 

[nvod11111111]

你还是觉得机器证明翻译成GTP（Geometry Theorem Proving）更恰当一些？

你怎么会这么认为呢？
书的名字都给出来了，你看了吗？

 

[未尝不可]

我讲得是吴文俊的机器证明
他给我贴出本数理逻辑的书
你看着事实而非
我看着确不是

我是这么看的，吴法是归于“Automated Theorem Proving”，
而你们的讨论一个焦点是大学里教不教“Automated Theorem Proving”，
那个课本虽说是数理逻辑，但书名说了“ Foundations of Automated Theorem Proving”，
要说没关系，倒也不是。

 

[未尝不可]

你怎么会这么认为呢？
书的名字都给出来了，你看了吗？

1984年 由W. W. Bledsoe等编辑的《Automated Theorem Proving:After 25 Years》出
版，收入吴文俊的奠基性论文，吴文俊的机械化数学思想在国际上得到广泛传播。

 

[网洋中的一条鱼]

专业五毛有种撞了南墙也不回头的，死缠烂打的，永不认输的劲头。

 

[nvod11111111]

还想接着玩，俺奉陪：https://en.wikipedia.org/wiki/Mathematics_Mechanization_and_Automated_Reasoning_Platform
Mathematics Mechanization and Automated Reasoning Platform (Chinese: 数学机械化自动推理平台), or Mathematics-Mechanization Platform (MMP, code named elimino), is a group of automated theorem proving software based on an internal computer algebra system. It can be used on proving algebra and geometry theorems. This system is led by Wu Wenjun and based on Wu's method.

你是想通过这个帮我举证吴文俊是机器证明的的奠基人吗？

 

[nvod11111111]

1984年 由W. W. Bledsoe等编辑的《Automated Theorem Proving:After 25 Years》出
版，收入吴文俊的奠基性论文，吴文俊的机械化数学思想在国际上得到广泛传播。

看来你是承认吴文俊是机器证明的奠基人。

 

[oldbei]

你是想通过这个帮我举证吴文俊是机器证明的的奠基人吗？

不是啊，他就是在自动定理证明这个学科里，做了一些工作（主要是几何定理方面的）。至于您说的“机器证明”，英文里没有对应的说法，哪儿还谈得上什么奠基人。最接近的恐怕是Automated Reasoning。学科的范围越大，吴文俊相对的贡献就越小。