Mizar を用いた動的検証可能な数学ドキュメンテーション https://mizar.work/dokuwiki/ Thu, 30 Apr 2026 19:14:13 +0000 FeedCreator 1.8 https://mizar.work/dokuwiki/lib/exe/fetch.php?media=wiki:dokuwiki.svg https://mizar.work/dokuwiki/ https://mizar.work/dokuwiki/doku.php?id=example&rev=1748500509 第1章 TARSKIの公理系 このテキストは集合論を題材に mizar を使った数学定理の記述が実際にどのようになされているかを説明します。 mizar では，その数学記述言語によって書かれたテキストを \(x, y, z, u, N, M, X, Y, Z\)\[ ((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X=Y \]\(x\)\(x \in X \Leftrightarrow x \in Y\)\(X\)\(Y\)\(X = Y\)\(x\)\(\{x\}\)\(x\)\(y\)\(\{x, y\}\)\(y\)\(\{y\}\)\(x\)\[ x \in \{y\} \Leftrightarrow x = y \]\(y\)\(z\)\(\{y, z\}\)\(x\)\[ x \in \{y, z\} \Leftrightarrow x = y \lor x = z \]\[ \{y, z\} = \{z, y\} \]\(X\)\(Y\)\(X\)\(Y\)\(X\)\(Y\)\(X \subsete… superuser@undisclosed.example.com (superuser) Thu, 29 May 2025 06:35:09 +0000 https://mizar.work/dokuwiki/doku.php?id=wiki:syntax&rev=1745128997 Formatting Syntax DokuWiki supports some simple markup language, which tries to make the datafiles to be as readable as possible. This page contains all possible syntax you may use when editing the pages. Simply have a look at the source of this page by pressing superuser@undisclosed.example.com (superuser) Sun, 20 Apr 2025 06:03:17 +0000 https://mizar.work/dokuwiki/doku.php?id=wiki:dokuwiki&rev=1745128947 DokuWiki wiki:dokuwiki DokuWiki is a simple to use and highly versatile Open Source wiki software that doesn't require a database. It is loved by users for its clean and readable syntax. The ease of maintenance, backup and integration makes it an administrator's favorite. Built in superuser@undisclosed.example.com (superuser) Sun, 20 Apr 2025 06:02:27 +0000 https://mizar.work/dokuwiki/doku.php?id=wiki:welcome&rev=1745127111 Welcome to your new DokuWiki Congratulations, your wiki is now up and running. Here are a few more tips to get you started. Enjoy your work with DokuWiki, -- the developers Create your first pages Your wiki needs to have a start page. As long as it doesn't exist, this link will be red: superuser@undisclosed.example.com (superuser) Sun, 20 Apr 2025 05:31:51 +0000 https://mizar.work/dokuwiki/doku.php?id=start&rev=1744336091 パート1 ここには通常の内容（説明文など）が入ります。 パート2 こちらも通常の内容です。 superuser@undisclosed.example.com (superuser) Fri, 11 Apr 2025 01:48:11 +0000 https://mizar.work/dokuwiki/doku.php?id=en:sidebar&rev=1744083568 ---------- * Basic Syntax and Behavior * Interactive Demo * Mizar Verifiable Docs(English) * GitHub repository * note creator page superuser@undisclosed.example.com (superuser) Tue, 08 Apr 2025 03:39:28 +0000 https://mizar.work/dokuwiki/doku.php?id=sidebar&rev=1744083504 ---------- * 基本文法と動作 * 体験デモ * Mizar Verifiable Docs (日本語) * GitHub リポジトリ * note クリエイターページ superuser@undisclosed.example.com (superuser) Tue, 08 Apr 2025 03:38:24 +0000 https://mizar.work/dokuwiki/doku.php?id=en:example&rev=1744082392 Chapter 1 TARSKI's axiomatic system This text explains how the description of mathematical theorems is actually carried out using Mizar with set theory as the subject matter. In Mizar, texts written in its mathematical description language are called \(x, y, z, u, N, M, X, Y, Z\)\[ ((\forall x)(x \in X \Leftrightarrow x \in Y)) \Rightarrow X = Y. \]\(x\)\[ x \in X \Leftrightarrow x \in Y, \]\(X\)\(Y\)\(X = Y\)\(\{x\}\)\(x\)\(x\)\(y\)\(\{x, y\}\)\(y\)\(\{y\}\)\(x\)\[x \in \{y\} \Leftrightarrow x… superuser@undisclosed.example.com (superuser) Tue, 08 Apr 2025 03:19:52 +0000