Differences

This shows you the differences between two versions of the page.

--- start [2026/06/22 07:29] – [不動点論理] kenji_saotome
+++ start [2026/06/25 12:39] (current) – hiroshi_unno
@@ Line 24: / Line 24: @@
 	* **2025年4月**. Professor **Hiroshi Unno**'s project, "Foundations and Applications of Program Verification Techniques," has been selected for funding under the [[https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-25H00446/|KAKENHI Grant-in-Aid for Scientific Research (S)]].
 	* **2025年2月**. The paper "Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking" by Professor **Hiroshi Unno** et al. was presented at [[https://aaai.org/conference/aaai/aaai-25/|AAAI 2025]].
-	* **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor Hiroshi Unno et al. received a **Distinguished Paper Award** at [[https://popl25.sigplan.org/|POPL 2025]].
+	* **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor **Hiroshi Unno** et al. received a **Distinguished Paper Award** at [[https://popl25.sigplan.org/|POPL 2025]].
 	* **2025年1月**. The paper "A Primal-Dual Perspective on Program Verification Algorithms" by Professor **Hiroshi Unno** et al. was presented at [[https://popl25.sigplan.org/|POPL 2025]].
 	* **2025年1月**. The paper "Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs" by Professor **Hiroshi Unno** et al. was presented at [[https://popl25.sigplan.org/|POPL 2025]].
@@ Line 97: / Line 97: @@
 //不動点論理//（Fixpoint Logics）は、最小不動点および最大不動点を扱う論理体系の総称であり、演繹的検証で生成された制約を記述するための有力な枠組みである。
 基本的な考え方として、多くの異なる意味論において、プログラムのループの意味論をある作用素の最小不動点として表現できる。したがって、プログラム全体の意味論を計算する問題は、本質的には最小不動点を計算する問題へと帰着される。
 解きたい問題によっては、不動点論理の方程式の下界や上界を求める問題などの不動点論理の問題として帰着できる場合がある。
 こうした問題を自動化するための代表的な手法の一つが、テンプレートの利用である。
-例えば不動点の下界や上界を求める場合、テンプレートを用いたアプローチでは、求める境界が予め与えられた形状（例えば　固定次数の多項式）を持つと仮定する。
+例えば不動点の下界や上界を求める場合、テンプレートを用いたアプローチでは、求める界が予め与えられた形状（例えば　固定次数の多項式）を持つと仮定する。
-これにより、境界が満たすべき条件は、テンプレートのパラメータに関する制約（例えば　多項式の係数に関する制約）へと変換される。
+これにより、界が満たすべき条件は、テンプレートのパラメータに関する制約（例えば　多項式の係数に関する制約）へと変換される。
-その結果、不動点の境界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換できる。
+このように、不動点の界を求める問題をテンプレートのパラメータを未知数とする制約充足問題へと変換できる。
-==== SATとSMTソルバー ====
+==== SATソルバーとSMTソルバー ====
-演繹的検証によって生成さられる制約を解く方法はいくつか存在する。
+演繹的検証によって生成された制約を解く方法はいくつか存在する。
-一つの方法は、定理証明ソフトウェア（proof assistants）を利用することである。
+一つの方法は、定理証明ソフトウェア（proof assistants）を利用する方法で、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
-定理証明ソフトウェアを用いると、人間が形式的な証明を書いて、その正しさを機械的に検査することができる。
 この手法は、人間の創意工夫に依存するため、原理的には非常に幅広い種類の制約を扱うことができる。
-しかし、その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
+その一方で、証明の構築には人間の介入が必要であり、自動化の程度は限定的である。
 これに対し、特定の形式の制約を自動的に解くことを目的として設計された専用ソルバーを利用する方法もある。
 その代表例が、充足可能性（Satisfiability, SAT）ソルバーや、述語理論充足可能性（Satisfiability Modulo Theory, SMT）ソルバーである。
@@ Line 121: / Line 121: @@
 | 教授 | [[https://www.riec.tohoku.ac.jp/~unno/|海野 広志]] |
 | 助教 | [[https://www.riec.tohoku.ac.jp/~eberhart/|Eberhart Clovis]] |
-| 博士研究員 | [[https://researchmap.jp/k_saotome?lang=en|早乙女 献自]] |
+| 特任研究員 | [[https://researchmap.jp/k_saotome?lang=ja|早乙女 献自]] |
 | 秘書 | 寒河江 香子 |
 | 修士課程  | [[takuma_monma|門馬 琢磨]] |
@@ Line 152: / Line 152: @@
 研究室は[[https://www.riec.tohoku.ac.jp/ja/top/access/|東北大学電気通信研究所]]本館の五階にあります。
-教員達と研究員達はM518室とM519室にいます。
+教員と研究員はM518室とM519室、学生はM536室とM537室にいます。
-学生達はM536室とM537室にいます。
+また、輪読とセミナーにM522室を使用しています。
-M522室は輪読とセミナーに使います。
 ===== リンク =====