I have the important documents as follows: I would like to know further information
I have the important documents as follows: I would like to know further information: On February 16, 2019 Professor H. Okumura introduced the surprising news in Research Gate:\index{Okumura, H.} \medskip \begin{quote} \noindent José Manuel Rodríguez Caballero \\ \index{Caballero, J. M. R.} \noindent Added an answer \\ \noindent In the proof assistant Isabelle/HOL we have $x/0 = 0$ for each number $x$. This is advantageous in order to simplify the proofs. You can download this proof assistant here: \\ {\bf https://isabelle.in.tum.de/} \index{https://isabelle.in.tum.de/} \medskip \end{quote} J.M.R. Caballero kindly showed surprisingly several examples by the system that $$ \tan \frac{\pi}{2} =0, $$ $$ \log 0 =0, $$ $$ \exp \frac{1}{x} (x=0) =1, $$ and others. %It seems that the division by zero calculus was implimented to the computer system already. The relation of Isabelle/HOL \index{Isabelle/HOL} and division by zero is unclear at this moment, however, the following document will be interested in: \medskip \begin{quote} Dear Saitoh, In Isabelle/HOL, we can define and redefine every function in different ways. So, logarithm of zero depends upon our definition. The best definition is the one which simplify the proofs the most. According to the experts, z/0 = 0 is the best definition for division by zero. $$ \tan(\pi/2) = 0 $$ $$ \log 0 = $$ is undefined (but we can redefine it as $0$) $$ e ^0 = 1 $$ (but we can redefine it as $0$) $$ 0^0= 1 $$ (but we can redefine it as $0$). In the attached file you will find some versions of logarithms and exponentials satisfying different properties. This file can be opened with the software Isabelle/HOL from this webpage: https://isabelle.in.tum.de/ Kind Regards, José M. (2017.2.17.11:09). \end{quote} \medskip At 2019.3.4.18:04 for my short question, we received: \medskip It is as it was programmed by the HOL team. Jose M. On Mar 4, 2019, Saburou Saitoh wrote: Dear José M. I have the short question. For your outputs for the division by zero calculus, for the input, is it some direct or do you need some program??? With best regards, Sincerely yours, Saburou Saitoh 2019.3.4.18:00 \medskip Furthermore, for the presentation at the annual meeting of the Japanese Mathematical Society at the Tokyo Institute of Technology: \medskip March 17, 2019; 9:45-10:00 in Complex Analysis Session, {\it Horn torus models for the Riemann sphere from the viewpoint of division by zero} with \cite{dops19}, \medskip \noindent he kindly sent the message: \medskip \begin{quote} It is nice to know that you will present your result at the Tokyo Institute of Technology. Please remember to mention Isabelle/HOL, \index{Isabelle/HOL} which is a software in which x/0 = 0. This software is the result of many years of research and a millions of dollars were invested in it. If x/0 = 0 was false, all these money was for nothing. Right now, there is a team of mathematicians formalizing all the mathematics in Isabelle/HOL, where x/0 = 0 for all x, so this mathematical relation is the future of mathematics. https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/ %It seems that the division by zero calculus seems to be implimented to the computer system already in a sense. \medskip \end{quote} Surprisingly enough, he sent his e-mail at 2019.3.30.18:42 as follows: \medskip \begin{quote} Nevertheless, you can use that $x/0 = 0$, following the rules from Isabelle/HOL and you will obtain no contradiction. Indeed, you can check this fact just downloading Isabelle/HOL: https://isabelle.in.tum.de/ and copying the following code theory DivByZeroSatoih imports Complex Main begin theorem T: ‹x/0 + 2000 = 2000› for x :: complex by simp \end{quote} \bigskip Copilot回答を生成しています…
出産・子育て
ファッション
美容・コスメ
健康・ダイエット
生活・インテリア
料理・食べ物
ドリンク・お酒
ペット
趣味・ゲーム
映画・ＴＶ
音楽
読書・コミック
旅行・海外情報
園芸
スポーツ
アウトドア・釣り
車・バイク
パソコン・家電
そのほか
すべてのジャンル
