出版者・発行元：Nanzan University  

古典命題論理CL では，m 個の命題変数p_1,...,p_m から構成される任意の論理式Aに対して，Aと同値な主和積標準形の論理式Bが存在して，Aを偽にするような付値関数をすべて求めることで，このBを求めることができる．佐々木は2013年に，K4を含む様相論理Lにおいて，CLの主和積標準形に対応するLの標準形と，CLの付値関数に対応するLのイグザクトモデルを構成し，CLと同等の定理を証明した．本稿は，佐々木の方法を用いて，様相論理K5において，CLの主和積標準形に対応するK5の標準形とCLの付値関数に対応するK5のイグザクトモデルを構成し，同等の定理を証明する．とくに，命題変数の個数が2つ以下の場合は，その標準形とイグザクトモデルを具体的に記述する．

出版者・発行元：Nanzan University  

本稿では，中点連結定理を用いた問題を統合的・発展的に考察し，数学教育における題材を提供する．より具体的には，問題の条件変えの考察により，難易度の異なる複数の類似問題を作成する基礎，および，複数の問題を，それらの共通点をもとに統合的に捉える具体例を提供する．

出版者・発行元：Nanzan University  

直接推論のシークエント体系と様相論理における必然記号□のふるまいの関係を明らかにする．

出版者・発行元： Polish Ministry of Science and Higher Education  

自然演繹体系におけるproperな推論規則とimproperな推論規則を区別するシークエント体系を導入し，その完全性を示した．

出版者・発行元：Nanzan University  

証明のフローチャートをもとにした n-同値関係の図式を導入し，この図式を用いて逆命題を考察する．具体的には，中学校数学の内容を対象として， 3 つの証明問題の逆命題を考察する．

出版者・発行元：Nanzan University  

メネラウスの定理の証明における多様な見方・考え方を考察する．この考察は，中込の2016年の論文でも行われているが，本稿では，さらに多様な見方・考え方を考察する．より具体的には，中込の論文で紹介された証明よりも一般的な証明を示し，この一般的な証明の特殊化を考察することで，中込の論文で紹介された証明がどのように特殊化されるかを明記すること，および，別の見方・考え方の証明が見出せることを示す

出版者・発行元：数理解析研究所  

逆命題を作るときに結論と入れ替える仮定のどの部分を選択するかについて，フローチャートを用いて適切に行う方法を提案し，例証した．

出版者・発行元：数理解析研究所  

証明活動における形式体系，とくにシークエントの役割とよさを明らかにし，シークエントの証明図とフローチャートの両方のよさをもつLKP構想図と提案し，その効果を例証した．

出版者・発行元：南山大学  

知識構成型ジグソー法の数学の授業の型は，組み合わせ型と多思考型に分類されている．本稿では，高等学校数学の内容を対象として，組み合わせ型の実践例を1つと多思考型の実践例を2つ挙げ，2つの型で期待される効果をより高めるための方法を考察する．

出版者・発行元：南山大学  

本稿は，証明活動における証明の構想を表現する図式について考察する．証明の図式は，フローチャートの他に，Gentzen が与えた形式体系LK における証明図が知られている．その証明図では，「証明をシークエントの変化としてとらえる」という考え方を基本としている．佐々木は，2015年に，この考え方が証明の構想の図式化に適していることを示し，体系LK の証明図にフローチャートのよさを加える形で，証明の構想を表現する図式を導入した．本稿は，その図式をさらに実際の証明の構想に近い形に整えたLKP 構想図を導入し，そのよさを，実際の証明の構想をLKP 構想図で表現することで示す．

出版者・発行元：Nanzan University  

逆命題は，もとの命題の仮定の1 つと結論を入れかえた命題である．もとの命題は成立するものとして，本稿では，逆命題が成立しない場合に，もとの命題の仮定を結論と同値になるまで弱めるという考え方を考察し，数学教育におけるその考え方のよさを2つ挙げる．

出版者・発行元：南山大学  

平行線，角の二等分線，二等辺三角形の関係に注目し，それを用いた証明問題を作成した結果を示した．より具体的には，証明問題を作成するある手法を提案し，その手法に従って作成した証明問題(30題)を紹介した．

出版者・発行元：Nanzan University  

In 2010, by using normal forms and exact models, we provided a detailed description of the mutual relation of formulas with finite propositional variables p_1,...,p_m in the modal logic S4. In the present paper, we extend most of the results to normal modal logics containing the modal logic K4.

出版者・発行元：University of Lodz  

2007年のMossの問題に対して、否定的な解を与えた。すなわち、S4を含む様相論理で、その深さnの標準形の論理式からMossの方法で構成される有限モデルが推移的でないものの例を挙げた。

出版者・発行元：南山大学  

シークエント体系に基づいて、集合の分野で扱われているド・モルガン律と分配律の証明の分析を行った。具体的には、18冊の文献から証明を抽出し、それらを体系SNKに基づいた方法で表現し、分類・整理した。また、この分類毎に、多く用いられた推論規則を用いた証明の形を作成した。

出版者・発行元：南山大学  

ε-N論法の証明における、変数に代入すべき項の選択方法を系統的にまとめた。対象とした証明は、数列の収束に関する11の基本的性質の証明である。代入すべき項が依存する変数の傾向を示してから、具体的な選択方法を示した。選択方法を構成する手法は、5つの文献で個別の性質に対して用いられているものを採用した。

出版者・発行元：南山大学  

シークエント体系の証明図から、実際の証明を作る手続きを示す。また、この手続きを素朴集合論における証明の作成に適用した例を示す。

出版者・発行元：京都大学数理解析研究所  

Here, we discuss normal modal logics containing the normal modal logic K4. To do so, we use normal forms introduced by K. Sasaki in 2010. For two normal modal logics L_0 and L satisfying K4 ⊆ L_0 ⊆ L, we show relation between normal forms in L and normal forms in L_0.

出版者・発行元：The Association of Symbolic Logic  

Here, we provide a detailed description of the mutual relation of formulas with finite propositional variables p_1,＼cdots,p_m in modal logic S4. Specifically, we construct normal forms, which behave like the principal conjunctive normal forms in the classical propositional logic. The results include finite and effective methods to find a normal form equivalent to a given formula $A$ by clarifying the behavior of connectives and giving a finite method to list all exact models.

出版者・発行元：Nanzan University  

様相論理K4において、固定された有限個の命題変数からできる論理式で、様相記号の深さがnに制限されたものの集合を対象としたときの、すべてのexact　modelを列挙する方法を述べた。

出版者・発行元：Nanzan University  

様相論理S4の標準形に関する論文(The review of Symbolic Logic, vol. 3, pp. 600-627, 2010)において、いくつかの性質の証明が省略されている。ここでは、その証明の詳細を示す。

出版者・発行元：Nanzan University  

様相論理S4の標準形の2つの構成法が、(The review of Symbolic Logic, vol. 3, pp. 600-627, 2010)によって与えられた。1つは、S4の証明可能性に依存するが、もう一つは独立である。ここでは、その1つ目の方法を様相論理K4を含む正規様相論理全体に拡張する。また、2つ目の方法の一部を変更し、K4にも適用させる。

出版者・発行元：Nanzan University  

Here, we consider the set F^n of formulas with modal degree k (＼le n) and having only propositional variables p_1,...,p_m in modal logic S4. An exact model M for F^n is one of the simplest Kripke models satisfying M ＼models A iff A in S4, for any A in F^n. We construct an exact model for F^n without using the provability of {＼bf S4}.

出版者・発行元：Nanzan University  

We discuss two constructions of non-equivalent modal formulas for normal modal logics. One is basically same as the dual of the construction by L. S. Moss in 2007 and the other is the construction by K. Sasaki in 2008. The former is useful for any normal modal logics, while the latter has much more information for modal logic S4. Here we define two constructions in sequent style and discuss the difference between them.

出版者・発行元：Nanzan University  

Rosserの証明可能性の論理R^-に対するシークエント体系の研究を行い、GLのカットなしのシークエント体系の自然な拡張な形で、部分論理式特性をもつシークエント体系を得た。すなわち、Witness comparison のない部分については、GLと同じで、さらに部分論理式特性をもつ体系を得た。2004年に発表したR^-の体系は、部分論理式特性はもつが、上記の意味でGLの自然な拡張にはなっていなかった。

出版者・発行元：Nanzan University  

We construct the $m$-universal model $＼langle W,R,P ＼rangle $ for the modal logic {＼bf S4}, using an induction on the depth of the modal connective $＼Box$. Main difference from the construction given by Shehtman in 1978 is that our construction gives an effective description of the image of the valuation $P$, $ ＼{ P(A) ＼mid A ＼in {＼bf S} ＼} (＼subsetneq 2^W) $, where {＼bf S} is the set of formulas constructed from $＼bot$ and propositional variables $p_1,＼cdots,p_m $.

出版者・発行元：Nanzan University  

The structure (S/≡,≦) corresponds to Lindenbaum algebra of Lewis Logic {＼bf S4} and $ ＼le $ is the derivation of {＼bf S4}. Here we treat the structure (S/≡,≦); where (S/≡) is the quotient, modulo the provability of {＼bf S4}, of the set $S$ of all formulas constructed from a finite set $V$ of propositional variables and whose depth of $＼Box$ is less than a given number $n$; and [A]≦[B] if and only if A⊃B ∈S4. It is known that this structure is Boolean. We give an inductive construction of concrete representatives for the generators of the Boolean without using the provability of {＼bf S4}.

出版者・発行元：京都大学数理解析研究所  

Here we discuss the set S(p) of the formulas having only one atomic formula p in Grzegorczyk logic Grz and the set S(＼bot) of the formulas having only one atomic formula ＼bot in provability logic GL. We give an inductive construction of representatives in the quotient set S(p)/＼equiv modulo the provability of Grz. Also we modify the results by Boolos and give representatives in the quotient set S(＼bot)/＼equiv, which correspond to the representatives for Grz. Comparing these two reresentatives, we also give a way to express the GL-provability of formulas in S(＼bot) in Grz.

出版者・発行元：MLG  

Here we consider structures of the form (S/ ≡,≦) for a modal logic L, where S is a set of formulas closed under ⊃ (implication) and ∧ (conjunction), A≡B if and only if (A⊃B)∧(B⊃A)　∈L, [A]≦[B} if and only if A⊃B ∈L. If S/ ≡L is finite, then the structure can be clarified by an exact model; if not, however, there still have some difficulties. We point out these difficulties; and in a simple case, we show a solution.

出版者・発行元：MLG  

様相記号の深さの帰納法によりS4の導出構造を構成し、そこから、S4の証明可能性を有限的に判定するアルゴリズムを真理値表で表現した。

出版者・発行元：Nanzan University  

Here we discuss the formulas having only one atomic formula ⊥ in provability logic GL and the formulas having only one atomic formula p in Grzegorczyk logic Grz. We define a function g satisfying, for any formula A having only one atomic formula ⊥, A is provale in GL if and only if g(A) is provable in Grz.

出版者・発行元：MLG  

In the classical propositional logic, we can know mutual relation between formulas by comparing their truth tables. Exact models are a kind of extension of truth tables into non-classical logics. So, exact models give an effective way to understand mutual relation between formulas like truth tables in the classical propositional logic. Here we construct exact models in S4 for the sets of formulas with only one propositional variable p and the finite depth of ＼Box.

出版者・発行元：MLG  

Here we discuss relation between the provability of Grzegorczyk logic Grz and the provability of provability logic GL.

出版者・発行元：Nanzan University  

Here we treat modal formulas with only one propositional variable p in Lewis logic S4. The quotient set of the set of formulas modulo the provability of S4 is Boolean with respect to the derivation of S4 (cf. Chagrov and Zakharyaschev [CZ97]). We give an inductive construction of the representatives of the quotient set of the set of formulas with only one variable p and with a finite number of occurrences of ＼Box

出版者・発行元：MLG  

様相論理S4,様相論理S4Grzにおいて1変数で互いに非同値な論理式の集合を帰納的に構成した。

出版者・発行元：Nanzan University  

Grzegorczyk logic, GRZ, is the normal modal logic obtained by adding Grzegorczyk axiom ＼Box(＼Box(p ＼supset ＼Box p) ＼supset p ) ＼supset p to the smallest normal modal logic K. The quotient set of the set of formulas modulo the provability of GRZ is Boolean with respect to the derivation of GRZ. Here we give an inductive construction of the representatives of the quotient set of the set of formulas with only one propositional variable and with a finite number of occurrences of ＼Box.

出版者・発行元：University of Lodz  

To discuss Rosser sentences, Guaspari and Solovay enriched the modal language by adding, for each $＼Box A$ and $＼Box B$, the formulas $ ＼Box A ＼prec ＼Box B $ and $ ＼Box A ＼preceq ＼Box B $. They axiomatized modal logics ${＼bf R}^{-}$, which satisfies a kind of arithmetic completeness theorem. Here we introduce a sequent system for {＼bf R}$^{-}$ with a kind of subformula property.

証明可能性の論理R^- に対して、カットのないシークエント体系を与えた。これまでの体系の公理を推論規則で表現することで、
公理をカットの役割の理解を深めることができた。

出版者・発行元：Nanzan University  

Here a cut-free sequent system of the provability logic R^- for Rosser sentences is given. Comparing to the previous system for R^-, the rules corresponding to cut are restricted. Also another proof of the completeness theorem is given. The new proof clearly gives a concrete countermodel for a given sequent without cut-free proof, while previous proof doesn’t.

出版者・発行元：Nanzan University  

Guaspari and Solovay enriched the modal language by adding, for each □A and □B, the formulas □A ＼prec □B( and □A ＼preceq □B). Their arithmetic realizations are the Σ1-sentences ``A* is provable by a proof that is smaller than(is smaller than or equal to) any proof of B*''. They axiomatized modal logic R^{-} complete for this arithmetic realization. Also Rosser sentences in arithmetic theory can be treated by these Σ1-sentences. Here we introduce a sequent system for R^{-} with a kind of subformula property.

出版者・発行元：Kluwer Academic publishers  

We introduce a Gentzen style formulation of Basic Propositional Calculus (BPC), the logic that is interpreted in Kripke models similarly to intuitionistic logic except that the accessibility relation of each model is not necessarily reflexive. The formulation is presented as a dual-context style system, in which the left hand side of a sequent is divided into two parts. Giving an interpretation of the sequents in Kripke models, we show the soundness and completeness of the system with respect to the class of Kripke models. The cut-elimination theorem is proved in a syntactic way by modifying Gentzen's method. This dual-context style system exemplifies the effectiveness of dual-context formulation in formalizing various non-classical logics.

出版者・発行元：南山大学経営学会  

２つの厳密順序＜,＜1をもつクリプケフレーム<W,＜,＜1>（ただし、＜1⊆＜などが成立する）は、２つの様相記号□と∇をもつ様相論理PRL1を特徴付けることが、Smory’{n}skiにより述べられている。さらに、PRL1のカットなしのシークエント体系は、Sasaki により与えられている。ここでは、２つの順序≦と≦1を持つクリプケフレーム<W,≦,≦1>（ただし、≦1⊆≦などが成立する）が特徴付ける論理の公理系を２つの様相記号□と∇をもつ言語で与える。さらに、この論理に対するカットなしのシークエント体系も与える。

出版者・発行元：Nanzan University  

The smallest interpretability logic IL is an extension of provability logic GL with a binary operator ＼rhd. IL is obtained by adding axioms concerning ＼rhd to GL. The logic IK4 is a sublogic of IL and is obtained by adding the same axioms to normal modal logic K4 as the additional axioms of IL. A cut-free sequent system for IK4 was given by Sasaki. Here we give another cut-free system for IK4. Both of the systems satisfy kinds of subformula property, however, our new system has nicer one.

Here, we show some cut-free sequent systems for provability and interpretability logics.

To discuss Rosser sentences, Guaspari and Solovay enriched the modal language by adding, for each □A and □B, the formulas □A ＼prec □B( and □A ＼preceq □B), with their arithmetic realizations the Σ1-sentences ``A* is provable by a proof that is smaller than(is smaller than or equal to) any proof of B*''. They axiomatized modal logic R^{-} complete for the above arithmetic interpretation. Here we introduce a sequent system for R^{-} with a kind of subformula property.

出版者・発行元：京都大学数理解析研究所  

佐々木は、レーブの公理のある性質を用いて、証明可能性の論理GLのカット除去定理の別証明、および最小の解釈可能性の論理IL のカット除去定理の証明を与えた。しかしながら、この証明は複雑な部分がある。ここでは、この複雑な部分を帰納的な証明で置き換え、より整理された証明を与える。同時に、解釈可能性の論理の１つであるILPのカット除去定理を証明する。

出版者・発行元：Nanzan Daigaku Keiei Gakkai  

Visser's propositional logic(VPL) and formal propositional logic(FPL) are the propositional logics embedded into the modal logics K4 and GL by Gödel's translation. A cut-elimination theorem for VPL given by Sasaki in 1998 has an unclear part. Here we give a complete proof of the theorem. Also we give a cut-free Gentzen style system for FPL by modifying the system for VPL.

出版者・発行元：University of Lodz  

We treat two bimodal provability logics MOS and PRL1 described by Smory'{n}ski. We give cut-free sequent systems for these two logics by modifying a system by Avron for unimodal provability logic GL.

出版者・発行元：Nanzan University  

2様相論理PRL_1とMOSに対して、部分論理式特性が成立するようなシークエント体系を構成した。

出版者・発行元：Kluwer Academic Publishers  

The idea of interpretability logics were arose by Visser as extensions of the provability logic GL with a binary modality ＼rhd. The arithmetic realization of A ＼rhd B in a theory T will be that T plus the realization of B is interpretable in T plus the realization of A. Here we give a cut-free sequent system for the smallest interpretability logic IL. First, we give a cut-free system for the sublogic IK4 of IL. The theorem is proved using the system for IK4 and a property of Löb's axiom.

出版者・発行元：Nanzan University  

A cut-free sequent system for the smallest interpretability logic IL was given by Sasaki. Here, using the method by Sasaki, we give a sequent system for the interpretability logic ILP obtained by adding the persistence axiom to IL.

2つの様相記号を□、▽をもつ様相論理で、どちらの記号もある算術での証明可能性を表現するようなもののシークエント体系について述べた。

出版者・発行元：Nanzan University  

レーブの公理のある性質を用いて、証明可能性の論理GLのカット除去定理の証明を与えた。

出版者・発行元：Center for Management Studies, Nanzan University  

様相論理の1つであるpropositional lax logicにおいて、選言のない論理式の個数が、命題変数の個数を有限個に制限したとき、本質的に有限個であることを示した。さらにそれらを帰納的に構成する方法、対応するクリプケモデルについてもきちんと記述した。

出版者・発行元：Center for Management Studies, Nanzan University  

最小の解釈可能性の論理ILに対してカットのないシークエントの体系を与えた。ある意味で部分論理式特性をみたしているが、その点は詳細には述べられていない。

出版者・発行元：Center for Management Studies, Nanzan University  

Visser論理の言語に直観主義論理の「ならば」を加えることで、Visser論理に部分論理式特性が成り立つようなカットなしのシークエント体系を与えた。証明も丁寧に記述した。さらに、その体系をもとにFormal propositional logicに対しても、カットなしのシークエント体系を与えた。

出版者・発行元：Center for Management Studies, Nanzan University  

命題論理において、推論規則A/Bによる公理化と公理A→Bによる公理化が本質的に同じになるという性質を調べた。そして、レーブの公理とレーブの推論規則はこの性質をもっていることを述べ、それより大きな論理でこの性質をもつものはないことを証明した。カット除去定理にもこの性質が有効であることも述べた。

出版者・発行元：Nanzan Daigaku Keiei Gakkai  

出版者・発行元：Jagiellonian University Press  

出版者・発行元：Nanzan Daigaku Keiei Gakkai  

出版者・発行元：京都大学数理解析研究所  

出版者・発行元：南山大学経営学会  

出版者・発行元：南山大学経営学会  

出版者・発行元：Science University of Tokyo  

出版者・発行元：Kluwer Academic Publishers  

出版者・発行元：京都大学数理解析研究所  

出版者・発行元：University of Lodz  

出版者・発行元：京都大学数理解析研究所  

出版者・発行元：東京理科大学  

出版者・発行元：Kluwer Academic Publishers  

出版者・発行元：University of Lodz  

出版者・発行元：University of Lodz  

推論規則としてカットのみをもつ体系は，「ならば」の導入規則や「または」の除去規則などの一時的な仮定をもつ推論を含まず，単純な証明を表すと捉えられる．この体系では，無矛盾である限り，それらの一時的な仮定をもつ推論を導出できないことがわかっている．本発表では，その体系と様相論理との関係を明らかにする．

In natural deduction system for classical propositional logic, there are some inference rules withtemporal assumptions, e.g., implication introduction rule and disjunction elimination rule. Prawitz callssuch inference rules improper inference rules, and the others proper inference rules. Here, we distinguishbetween improper and proper derivations. Speci cally, we prove that any sequent system for classicalpropositional logic with only one inference rule cut does not allow improper derivations in general, while itallows proper ones. For instance, in such systems, the sequent ⇒p→q can not derive from the sequent p⇒q and axioms using cut. In order to prove the impossibility of improper derivations, we modify truthvaluation and prove completeness for sequent systems having only one inference rule cut.

背理法，場合分け，全称化などを用いた証明は，単純な文の変化では表現できず，難しいと捉えられることが多い．本講演では，単純な文の変化だけで表現できる証明の形式体系を導入しその完全性を示す．そして，その体系では，背理法，場合分け，全称化などに対応する導出が導けないことを示す．

自然演繹法の体系では，一時的な仮定をもつ推論規則がある．それらに対応づけられる推論は，そうでない推論と比べ，難しいと捉えられることが多い．本発表では，その2種類の推論を区別する形式体系を整理しその意味付けを行う．

数学教育の視点での逆命題を考察は，もとの命題の証明の過程をn-同値関係を単位とした図式にまとめることよって効率的に行えるという仮説を立て，それをいくつかの例で確認した．

証明活動における形式体系，とくにシークエントの役割とよさを明らかにし，シークエントの証明図とフローチャートの両方のよさをもつLKP構想図と提案し，その効果を例証した．

逆命題を作るときに結論と入れ替える仮定のどの部分を選択するかについて，フローチャートを用いて適切に行う方法を提案し，例証した．

証明活動における難しい推論と易しい推論を区別する必要性を述べ，形式体系に基づいてそれらを区別する方法示した．

1971年にMakinsonは証明した定理は、ある条件をみたす無矛盾なCongruential logicはidentity logic, complement logic, unit logic, zero, logicのいずれかのsub logicであるという定理に容易に拡張できる。この報告では、変数のない論理式に範囲を絞ったときに、どの無矛盾なcongruential logicの極大論理のうち、深さ2の論理式で公理化できるものの例を複数示した。

実証明をシークエントで捉えることが、証明の理解の助けになることの典型的な例をいくつか挙げた。

証明の構想におけるシークエントのよさを述べ，実際の証明の日本語表現とシークエント体系の証明図の対応を明らかにする．

証明の構想におけるシークエントのよさを述べ，証明の構想にできるだけ忠実なシークエント体系を提案する．

本発表は，学校教育における証明の構想を表現できる新しい図式を提案する．証明を表現する図式には，G.Gentzenが与えた形式体系LKの証明図や，中学校の証明教育での効果が知られているフローチャートなどがある．本稿は，LKの証明図に，証明の構想を表現する要因があることを示し，その要因を保存しつつフローチャートのよさを持つようにLKの証明図を変形する．結果として得られる図式は，LKの証明図のよさとフローチャートのよさの両方をもつ図式である．

We treat modal logics S4 and K4, and consider related exact models. In MSJ spring meeting 2014, we gave a method to list all the exact K4-models for F(n) in S4, where F(n) is the set of modal formulas with finite propositional variables p_1,...,p_m and with finite modal degree ≦n. Here, we give an easier method to list them by using the exact S4-models listed by the author in 2010.

固定された有限個の命題変数からできる論理式で様相記号の深さを有限に制限したものの集合を対象とした、様相論理S4のK4-イクザクトモデルについて述べた。そのすべてのモデルをS4のS4-exact modelを用いて列挙する方法を述べ、それが定義に基づくこれまでの方法よりも簡単であることを示した。

In 2010, we list all the exact S4-models for F(n) in S4, where F(n) is the set of modal formulas with finite propositional variables p_1,...,p_m and with finite modal degree <n+1. However, considering the case that n=0, we can easily observe that an exact model for F(0) in S4 does not have to be reflexive (i. e. S4-model). For example if m=1, W={α,β}, R={}, and P(p_1)={α}, then M=<W,R,P> is an exact model for F(0) in S4, but it is not S4-model. Here, we give a method to list all the exact K4-models for F(n) in S4.

固定された有限個の命題変数からできる論理式で様相記号の深さを有限に制限したものの集合を対象とした、様相論理S4のイクザクトモデルについて述べた。そのモデルがS4-モデルである必要でないことを具体例を挙げて説明し、そのモデルでK4-モデルであるものを全部列挙する方法を示した。

　実際の証明をシークエントの視点から分析する方法とその方法に基づく結果を示した。このアイデアは2011年度・加藤・佐々木の論文にもとづくが、方法等を一部改善している。その方法は、実際の証明をシークエントの変化で表現すること、その表現の各規則から定義による推論など、明らかな推論を切り離すこと、それらを分類することなどで構成される。

In 2010, we constructed normal forms and the exact model for the set F of formulas with finite propositional variables p_1,...,p_m in the modal logic S4; and provided a detailed description of the mutual relation of formulas in F in S4. The construction of normal forms can be naturally extended into the normal modal logics containing K4. The construction of the exact model can also be extended, but the Kripke model obtained by this construction is not generally exact. Here, we prove the equivalence between the following two conditions: (1) the resulting Kripke model is exact, (2) there exists an exact model.

シークエント体系の証明図から実証明を作る手続きを具体的に提示した。文のかたまりを作る推論規則と実証明の表現の関係にも言及した

2007年にMossが提示した問題に対し、標準形の独自の構成法をもとにした手法でn=2の場合の反例を挙げた。

実証明におけるシークエントの役割を確認し、実証明に近いシークエント体系から実証明を作る手続きを具体的に提示した。

様相論理Grzにおける標準形の論理式とexactモデルの構成法を示し。様相記号□の深さの小さいものについては、それらを具体的に示した。

様相論理S4における論理式の導出関係は、標準形の論理式およびexactモデルを用いる方法で、その詳細が明らかにされてきている。本報告は、この方法をS4以外の正規様相論理Lに適用するための、Lの条件を示した。

　2つの様相論理S4.1とS4.2は、どちらも極大元の条件により定められるクリプケモデルで特徴付けられる論理である。本報告では、標準形の論理式とexactモデルを用いて様相論理S4の論理式の導出関係を明らかにする方法が、このタイプのクリプケモデルで特徴付けられる論理に有効であることを述べ、実際にその方法を適用した結果を述べた。

正規様相論理における標準形の論理式について述べた。具体的には、固定したm個の命題変数から構成される深さd以下の論理式に対する標準形で、深さが最小のものを構成した。

様相論理S4の標準形に関する結果を、S4を含む一般の正規様相論理へ拡張する1つの方法を述べた。

様相論理K4の標準形の論理式について、様相論理S4の標準形の論理式を比較しながら述べた。とくに、任意の論理式に対し、その標準形の論理式を求める手続きのうち、論理式の構成にしたがうものを示した。

様相論理S4を含む正規様相論理Lにおける標準形の論理式について述べた。具体的には、固定したm個の命題変数から構成される深さd以下の論理式に対する標準形で、深さが最小のものを構成した。

S4を含む正規様相論理の標準形について述べた。S4での結果の一部をこれらの論理に一般的に拡張し、2つの論理S4.1,S4.2については具体的な標準形の例を示した。

正規様相論理における、非同値論理式の構成法について述べた。具体的には、これまでS4のみに適用していた構成法の正規様相論理への拡張を述べた。また、この方法と、L. S. Mossの2007年の論文で用いられた構成法との比較も述べた。

様相論理S4のn-universe modelを構成する方法で、その構成方法からS4の決定可能性が導かれるものを与えた。

様相論理S4のn-universe modelについて述べる。このmodelは1978年にShehtmanに よって与えられている。しかし、そのmodelの付値の部分は、帰納的には定義され ておらず、その意味でその構造は明確ではない。ここでは、この付値の部分も帰納 的に表現できるように、n-universal model を構成する。

様相論理S4の真理値表の作り方を述べた。この真理値表は無限の行をもつが、与えられた論理式に対応した真理値表の有限部分からその論理式の恒真性を判断できる。

Universal model 解明の意味、無限のn-universal modelを解明するために必要なことを述べた。さらに、その実現例を示した。

無限を対象としたときの、exact modelの2つの問題点を述べ、それを解決する方法を提案した。

無限を対象としたときの、exact modelの問題点を指摘し、Vの像を具体的に記述することの必要性を述べた。様相論理Grzを例にあげて具体的に記述した結果も述べた。

Sheftmanの与えたn-universal modelでは表現しきれない部分を指摘し、その部分を明確あるいは帰納的に表現した。

様相論理GLにおける変数のない論理式の証明可能性を様相論理Grzで判定する方法を述べた。具体的には、関数の列g_0,g_1,...を定義し、変数のない論理式Aに対し、AがGLで証明可能であることとg_0(A)がGrzで証明可能であることを示した。

様相論理S4において、命題変数としてpのみをもつ論理式の集合S(p)に対する exact model を構成する方法について述べた。具体的にはS(p)を様相記号□の深さで分類し、深さn以下の論理式の集合S^n(p)のexact model を構成する方法を示した。n=0,1,2に対しては、具体的なexact modelの例も示した。

Grzegorczyk logic において⊥のみから構成される論理式のふるまいとprovability logicにおいて命題変数pのみから構成される論理式のふるまいの関係について述べた。

SLACS2004において、1変数でしかも⊥が現れない論理式の集合Sに対して、順序集合(S/\equiv,\leq)を帰納的に構成する方法を述べた。 ただし、\equivはS4の同値性、\leqはS4の導出関係である。その方法は、順序集合がブール代数であることを利用し、そのブール代数の生成元の代表元(非同値論理式)だけを構成するもので、その中でS4の証明可能性が用いられている。 本報告では、この結果をn変数で⊥も対象とした論理式へ拡張し、上の方法で用いられていたS4での証明可能性を、論理式の形のみから判断する方法を述べる。

日本数学会2005年度年会で、様相論理S4において、1つの命題変数から⊃,∧,∨,□を用いて構成される論理式で□の深さが有限であるもの集合を対象とし、このリンデンバウム代数およびその代表元を帰納的に構成する方法を与えた。ここでは、これをn変数でしかも⊥を含む場合に拡張する方法を2つ報告する。1つは定義が簡潔でわかりやすいが、実際に計算するときは時間がかかる。もう1つは、定義は複雑であるが、実際の計算は1つ目の方法より速い。

　様相論理S4において、1つの命題変数から⊃,∧,∨,□を用いて構成される論理式で□の深さが有限であるもの集合を対象とし、このリンデンバウム代数およびその代表元を帰納的に構成する方法を与えた。

リンデンバウム代数は、非古典論理において、形式体系の代数的完全性を証明するのによく用いられる代数である。しかし、一般に知られている完全性の証明は、その代数の具体的な構造は必要としていない。故に、その証明からは、形式体系における論理式の相互関係について、具体的な構造のわからない代数との関係以上のことは導かれない。ここでは、exact model とよばれる Kripke model を用いて、いくつかの非古典論理に対するリンデンバウム代数の構造を明らかにした結果を紹介する。

様相論理S4,様相論理S4Grzにおいて1変数で互いに非同値な論理式の集合を帰納的に構成した。

本報告では、命題変数pから∧(論理積),∨(論理和),⊃(含意),□(必然) を用いて構成される様相論理の論理式の集合S(p)を対象とする。そして、順序集合(S(p)/≡,≦) の構造を明らかにする。ただし、≡は様相論理S4での証明可能性を法 とする同値関係、≦はS4での導出関係、すなわち 　　[A]≦[B]　⇔　あるA'∈[A]とB'∈[B]に対して、A'⊃B'がS4で証明可能 である。この順序集合は、既にブール代数であることが知られているが、ここでは、 その同値類の代表元を帰納的に構成することで、そのより詳細な構造を明らかにする。

古典論理、様相論理S5、直観主義論理、直観主義様相論理PLLを対象とし、それらのリンデンバウム代数の部分構造を帰納的に構成する方法を述べた。

様相論理Grzにおいて、1つの命題変数から⊃,∧,∨,□を用いて構成される論理式の集合を対象とし、この任意の有限集合のリンデンバウム代数およびその代表元を帰納的に構成する方法を与えた。

Rosser sentences を表現するために導入された3つの論理R,R^-,R^ωのシークエント体系について述べた。

証明をシークエントの変化として眺めることで形式化を行う方法について述べた。とくに、シークエントの変化としてとらえることの有効性を述べた。具体的な証明の例もあげ、シークエントの変化として捉えた場合と、ふつうの場合を比較した。

２つの強い順序＜,＜1をもつクリプケフレーム<W,＜,＜1>（ただし、＜1⊆＜などが成立する）は、２つの様相記号□と∇をもつ様相論理PRL1を特徴付けることが、Smory’{n}skiにより述べられている。さらに、PRL1のカットなしのシークエント体系は、Sasaki により与えられている。ここでは、２つの順序≦と≦1を持つクリプケフレーム<W,≦,≦1>（ただし、≦1⊆≦などが成立する）が特徴付ける論理の公理系を２つの様相記号□と∇をもつ言語で与える。さらに、この論理に対するカットなしのシークエント体系も与える。

To discuss Rosser sentences, Guaspari and Solovay enriched the modal language by adding, for each □A and □B, the formulas □A \prec □B( and □A \preceq □B), with their arithmetic realizations the Σ1-sentences ``A* is provable by a proof that is smaller than(is smaller than or equal to) any proof of B*''. They axiomatized modal logic R^{-} complete for the above arithmetic interpretation. Here we introduce a sequent system for R^{-} with a kind of subformula property.

いくつかの証明可能性の論理、解釈可能性の論理のシークエント体系を紹介した。各体系のカット除去定理の証明方法も複数紹介した。

最小の解釈可能性の論理ILのカットのないシークエント体系とVeltmanモデルとのある関係について述べた。

いくつかの証明可能性の論理、解釈可能性の論理のシークエント体系を紹介した。とくにレーブの公理を用いたカット除去定理の証明方法について述べた。

2つの様相記号をもつprovability logicの中で，MOSと呼ばれるもののシークエント体系について，講演した。

解釈可能性の論理ILおよびILPに対して、カットなしのシークエント体系を導入した。

形式体系におけるシークエントの役割、シークエント体系におけるカット除去の意味を説明し、Interpretability logicでの具体例を示した。

直観主義様相論理PLLのリンデンバウム代数の部分構造に対応するクリプケモデルを具体的に構成する方法を述べた。

直観主義命題論理における選言のない論理式に関するDiego,Urqhartらの結果が、直観主義様相論理PLLに拡張できることを示し、実際にPLLでの結果を示した。

2015年度に行う研究会のとりまとめを行う．

「セメスター方式による「ディジタルクリエイター」育成カリキュラムの開発及び地域イノベーション創出モデルへの参画」を研究テーマとした事業/岐阜県立岐阜各務野高等学校

日本私立大学連盟教育研究委員会委員

日本数学会数学基礎論および歴史分科会運営委員

2005年度第39回MLG数理論理学研究集会の世話人を務めた。

2004年度第38回MLG数理論理学研究集会の世話人を務めた。

教員免許状更新講習「図形問題を発展的に考察する手法」　8月30日 6時間

振り返りを促す課題の実践[2020年度Q2　論理と集合]
　課題，誤答例の解説，同様の課題で再確認という流れを繰り返し，理解を深められたと考える。

振り返りを促す課題の実践[2019年度Q2　論理と集合]
　中間試験の答案と採点結果を返却し、その間違いを考察する課題を与えた。自身の間違いを振り返ることでき、理解を深められたと考える。

3年次の演習での実践[2018年度　システム数理演III,IVソフトウェア工学演習III,IV] 1つの問題から、発展的な考察を行う課題を与え、自発的に学習できる形の授業を展開した

教員免許状更新講習「証明問題を発展的に考察する手法」　9月1日 6時間

教育方法の実践例
3年次の演習での実践[2017年度　システム数理演III,IVソフトウェア工学演習III,IV] 1つの問題から、発展的な考察を行う課題を与え、自発的に学習できる形の授業を展開した。

教員免許状更新講習「数学教育における記号化の役割」　8月26日 6時間

教育方法の実践例
「演習II」での実践[2016年度秋　情報システム数理演II,ソフトウェア工学演習II] 1つの問題から、発展的な考察を行う課題を与え、自発的に学習できる形の授業を展開した。

教員免許状更新講習「数学教育における記号化の役割」　9月3日 6時間

振り返りを促す課題の実践[2016年度春　情報数学]
　中間試験の答案と採点結果を返却し、その間違いを考察する課題を与えた。自身の間違いを振り返ることでき、理解を深められたと考える。

「演習II」での実践[2015年度秋　情報システム数理演II,ソフトウェア工学演習II]
1つの問題から、発展的な考察を行う課題を与え、自発的に学習できる形の授業を展開した。

教員免許状更新講習「数学教育における記号化の役割」　9月5日 6時間

講義内容のWebページ作成[2015年度春　情報数学、数理論理学、位相幾何入門]
　講義別のWebページを作成し、講義で配布した資料の一部、および、講義を補充する資料をこのページからダウンロードできるようにした。

次の講義資料を更新した：
・「情報数学」
・「数理論理学」
・「位相幾何入門」
・「情報システム数理演習I,II，ソフトウェア工学演習I,II」
・「数学科教育法B」
・「数理論理学研究」
・「教員免許状更新講習」

教員免許状更新講習「数学教育における記号化の役割」　9月6日 6時間

講義内容のWebページ作成[2014年度春　情報数学、数理論理学、位相幾何入門]
　講義別のWebページを作成し、講義で配布した資料の一部、および、講義を補充する資料をこのページからダウンロードできるようにした。

次の講義資料を更新した：
・「情報数学」
・「数理論理学」
・「位相幾何入門」
・「情報システム数理演習I,II，ソフトウェア工学演習I,II」
・「数学科教育法B」
・「数理論理学研究」
・「教員免許状更新講習」

次の講義資料を新規に作成した．
・「理工学概論」(3週分) （テーマを変更し新規に作成した）
・「科学技術英語」(4週分)

次の講義資料を新規に作成した．
・「理工学概論」(3週分)

教員免許状更新講習「記号表現から理解する数学文の構造と表現法」6時間

次の講義資料を更新した：
「情報数学」 (110ページ)　総合問題では，過去の経験から間違いやすい問題を，その間違いに気付けるような形で，整理した．
「数理論理学」 (64ページ+解答例)　黒板・ノート形式の部分を増やし，資料としては，昨年の80ページから64ページに単純化した．とくに，例題と練習問題との関連を強めた．・「位相幾何入門」(25ページ) 例題に関連性を持たせ，各週の内容がつながるようにした．
「情報システム数理演習I、ソフトウェア工学演習I」10ページ
「数学科教育法B」(12ページ+補充資料)
「数理論理学研究」(22ページ)
「教員免許状更新講習」(12ページ)　記号導入による記号化の利点の説明を追加した．

講義内容のWebページ作成[情報数学、数理論理学、位相幾何入門]
　講義別のWebページを作成し、講義で配布した資料の一部、および、講義を補充する資料をこのページからダウンロードできるようにした。

教員免許状更新講習「記号表現から理解する数学文の構造と表現法」
6時間

情報理工学部カリキュラム改正ワーキンググループリーダー

次の講義資料を新規に作成した：
・「数理論理学研究」(22ページ)
・「教員免許状更新講習」(12ページ)

次の講義資料を更新した：
・「情報数学」 (114ページ)　昨年の146ページの資料の焦点を絞り、要点を強調した。
・「数理論理学」 (80ページ+解答例+補充資料)　昨年の92ページから80ページに、要点を強調する形で簡素化した。　
・「位相幾何入門」(24ページ)
・「情報システム数理演習I、ソフトウェア工学演習I」10ページ
・「数学科教育法B」(12ページ+補充資料)

講義資料とPCプロジェクタを用いたプレゼンテーション
　　　　　　　[2012年度春　情報数学(2クラス)、数理論理学]
　講義資料およびそれに対応したスライドを用意し、授業を進めた。黒板・白板の利用が少ないので、多人数を対象としても、教師が学生の様子をみる機会が増え、学生を授業に集中させることができた。

情報理工学部教育業績賞(2011年6月)
　平成19年度および平成20年度に担当した「情報表現論」のための講義資料が評価され、表彰された。この資料は担当者および講義名称が代わっても継続して利用されている。

次の講義資料を更新した：
・「情報数学」 (146ページ)　
・「数理論理学」 (92ページ+解答例+補充資料)　　
・「情報システム数理演習I、ソフトウェア工学演習I」8ページ
・「数学科教育法B」(12ページ)

講義資料とPCプロジェクタを用いたプレゼンテーション
　　　　　　　[2011年度春　情報数学(2クラス)、数理論理学]
　講義資料およびそれに対応したスライドを用意し、授業を進めた。黒板・白板の利用が少ないので、多人数を対象としても、教師が学生の様子をみる機会が増え、学生を授業に集中させることができた。

次の講義資料を新規に作成した：
・「位相幾何入門」(30ページ)

次の講義資料を更新した：
・「数理論理学」 (98ページ+解答例)　　
次のプレゼンテーションファイルを更新した：
・「数理論理学」 (約5.30MB)

練習問題とその解説[2010年度春　数理論理学]
　授業の後半にその授業の復習を目的とした練習問題を行なう時間を設けた。解答は次の授業の冒頭で解説し、さらに、その解説に用いた資料をWebにも公開した。同様の内容を異なる形で繰り返すことによる知識の定着を目的としている。

講義資料とPCプロジェクタを用いたプレゼンテーション[2009年度春　情報数学(4クラス)、数理論理学、代数系入門]
この教育方法は、授業前に、書き込み式の講義資料の作成・配布、およびその資料に対応したプレゼンテーションファイルの作成を行ない、授業においては、スクリーン上で資料に書き込むべきことを示しながら進める方法である。受講生80名〜180名の講義科目で実践した。この方法から、次の3つの効果を期待している：すなわち、黒板等をうつすだけの授業にしないこと、担当者の説明に集中させること、重要な点はペンを使わせて記憶に残させることである。資料に書き込むべき場所は、重要度、学生のノートをとるスピードなど考慮して決めた。書き込むべき内容は、赤系統の文字を用いて、すでに配布物にかかれていることと区別した。この方法は、1994年から継続して実践しているが、配布資料と板書が対応していることから、ノートがとりやすい、授業がわかりやすいとの意見がきかれている

「情報システム数理演習I」での実践[2009年度春　情報システム数理演I]
少人数クラスであることを活かし、推論の形式体系を構築する過程を、授業で体験できるような形で授業を展開した。形式体系の意味をより深く理解し、活用できること、および別の新しい理論を構築するための材料となることを目的としている。

次の講義資料を新規に作成した：
・「代数系入門」 (104ページ+解答例)　

「数学科教育法B」についての学生による授業評価 2010年1月
2009年度に担当した「数学科教育法B」に関する「学生による授業評価」結果について述べる。授業内容に関わる設問4〜18の平均値は、4.52(1〜5の5段階評価)であり、概ね良い結果であった。また、裏面の自由記述欄には、「指導法」の授業に関するものなど6件のよいコメントが得られた。

テーマ科目等科目についての授業案内リーフレットの作成　
テーマ科目等委員会委員長として、2010年度のリーフレット作成をとりまとめた。

次の講義資料を更新した：
・「数学科教育法B」14ページ
・「情報数学」 (128ページ)　
・「数理論理学」 (102ページ+解答例)　　
・「情報システム数理演習I」8ページ

講義内容のWebページ作成[2009年度春　情報数学、数理論理学、代数系入門]
講義別のWebページを作成し、講義で配布した資料をこのページからダウンロードできるようにした。以下の項目で示すいくつかの資料もここにまとめて閲覧できるようにした。

練習問題とその解説[2009年度春　情報数学、数理論理学、代数系入門]
授業の後半にその授業の復習を目的とした練習問題を行う時間を設けた。解答は次の授業の冒頭で解説し、さらに、その解説に用いた資料をWebにも公開した。同様の内容を異なる形で繰り返すことによる知識の定着を目的としている。

マルチメディア教育ワーキンググループリーダー
　大学全体の情報教育、マルチメディア機器を利用した教育について検討し、12月に答申をまとめた。

次の講義資料を更新した：
・「情報数学」 (121ページ)　
・「数理論理学」 (102ページ+解答例)　　
・「情報表現論」 (50ページ)
・「数理情報学概論A」 (5ページ)　
・「情報システム数理演習I」(20ページ)

　講義内容のWebページ作成[2008年度春秋　情報数学、数理論理学、数理情報学概論A(1週分)]
　講義別のWebページを作成し、講義で配布した資料をこのページからダウンロードできるようにした。以下の項目で示すいくつかの資料もここにまとめて閲覧できるようにした。

　練習問題とその解説[2008年度春　情報数学、数理論理学]
　授業の後半にその授業の復習を目的とした練習問題を行なう時間を設けた。解答は次の授業の冒頭で解説し、さらに、その解説に用いた資料をWebにも公開した。同様の内容を異なる形で繰り返すことによる知識の定着を目的としている。

　「情報システム数理演習I」での実践[2008年度春　情報システム数理演I]
　2007年度の授業は、推論の形式体系を構築する過程を体験できるような形で構成した。今年度はそれをより系統だてた形で実践した。形式体系の意味をより深く理解し、活用できること、および別の新しい理論を構築するための材料となることを目的としている。

「情報数学」についての学生による授業評価 2008年7月
2008年度に担当した「情報数学」に関する「学生による授業評価」結果について述べる。授業内容に関わる設問4〜18の平均値は、4.02(1〜5の5段階評価)であり、昨年より低いものの裏面の自由記述欄には、「わかりやすい」、「楽しい」に類するコメントが得られた(6件)。

名古屋キャンパスにおける韓国朝鮮語I,IIに続く科目の検討
　外国語委員会委員長として、標記科目の需要を調べ、2009年度からの開講の立案・検討を行なった。

　講義資料とPCプロジェクタを用いたプレゼンテーション[2008年度春秋　情報数学、数理論理学、数理情報学概論A(1週分)]
　この教育方法は、授業前に、穴埋め式の講義資料の作成・配布、およびその資料に対応したプレゼンテーションファイルの作成を行ない、授業においては、スクリーン上で資料の穴を埋めながら進める方法である。この方法から、次の3つの効果を期待している：すなわち、黒板等をうつすだけの授業にしないこと、担当者の説明に集中させること、重要な点はペンを使わせて記憶に残させることである。空欄の(穴埋めすべき)場所は、講義における重要な部分、学生のノートをとるスピードなど考慮して決めた。空欄にかくべきことは、赤系統の文字を用いて、すでに配布物にかかれていることと区別した。この方法は、1994年から継続して実践しているが、配布資料と板書が対応していることから、ノートがとりやすい、授業がわかりやすいとの意見がきかれている。

テーマ科目等科目についての授業案内リーフレットの作成　
　テーマ科目等委員会委員長として、2008年度の標記リーフレットをもとにした2009年度のリーフレット作成をとりまとめた。

　次の講義資料を新規に作成した：
・「数学科教育法B」14ページ

次の講義資料を更新した：
・「情報数学」 (131ページ)　LaTeXで作成しなおし、記号をはっきり識別できるようにした。
・「数理論理学」 (98ページ)　
・「情報数学特別講義」 (76ページ)　前年度のものを構成からみなおし、整理した。69ページ以降は新規の話題である。
・「数理情報学概論A」 (5ページ)

　「情報表現論」(8クラス)の内容整理およびとりまとめ
　この科目のとりまとめ役を務めた。これまで学科毎に独立に運営をしてきていたが、学部一括募集にともない今年度から両学科共通の授業となった。そのために、その内容から検討する必要があった。結果、学修目標に整合するように内容を整理し、両学科の同意を得た。その内容にそう講義資料(50ページ)も作成した。新しい話題もかなりとりいれた。また、とりまとめ役として、2回の会合を開き、授業の基本的な運営方針をまとめた。

　共通教育科目における留学生サポート
　教務部次長として、瀬戸キャンパスにおける留学生が共通教育履修するためのサポートを行なった。具体的には、Webで学内公開されているINFOSS情報倫理教科書にルビをふる作業をとりまとめた。

　講義資料とPCプロジェクタを用いたプレゼンテーション[2007年度春秋　情報数学、情報数学特別講義、数理情報学概論A(1週分)]
　穴埋め式の講義資料の作成・配布、およびその資料に対応したプレゼンテーションファイルを作成を事前に行ない、授業は、スクリーン上で資料の穴を埋めながら進める方法をとった。この効果として、次の3つを意図している：すなわち、黒板等をうつすだけの授業にしないこと、担当者の説明に集中させること、重要な点はペンを使わせて記憶に残させることである。空欄の(穴埋めすべき)場所は、講義における重要な部分、学生のノートをとるスピードなど考慮して決めた。空欄にかくべきことは、赤系統の文字を用いて、すでに配布物にかかれていることと区別した。この方法は、1994年から継続して実践しているが、配布資料と板書が対応していることから、ノートがとりやすい、授業がわかりやすいとの意見がきかれている。

　練習問題とその解説[2007年度春　情報数学]
　授業の後半にその授業の復習を目的とした練習問題を行なう時間を設け、次の授業の冒頭で解説した。さらに、その解説に用いた資料をWebにも公開した。同様の内容を異なる形で繰り返すことによる知識の定着を目的としている。

　サンプルプログラムのWeb公開(学内のみ)[2007年度秋　情報数学特別講義]
　プログラム実習のためのサンプルプログラムをWebで閲覧できるようにした。この効果として、次の2つを意図している：すなわち、授業で説明したアルゴリズムを、プログラムを動かすことで即座に体験でき、理解度があがること、サンプルプログラムを一部修正することで、練習問題のプログラムを作成でき、達成感があること である。

「数理情報学概論A」（オムニバス形式14名が担当)のとりまとめ役として、運営方針の確認、全体にかかわることの学生への案内を行なった。

「情報数学」についての学生による授業評価 2007年7月
2007年度に担当した「情報数学」(2クラス)に関する「学生による授業評価」結果について述べる。授業内容に関わる設問4〜18の平均値は、4.24と4.23(1〜5の5段階評価)であり、全体的によい評価であった。とくに、配布資料・スクリーンを用いた授業について高評価が得られたと思う(裏面の自由記述欄によかったとのコメントが各クラスで8件あった)。

次の講義資料を新規に作成した：
・「情報表現論」50ページ
・「数理科学演習I」17ページ

　「数理科学演習I」での実践[2007年度春　数理科学演習I]
　少人数クラスであることをいかし、推論の体系を構築する過程を、授業で体験できるような形で授業を構成した。その体系の意味をより深く理解し、活用できること、および別の新しい理論を構築するための材料となることを目的としている。

　講義内容のWebページ作成[2007年度春秋　情報数学、情報数学特別講義、数理情報学概論A(1週分)]
　講義別のWebページを作成し、講義で配布した資料をこのページからダウンロードできるようにした。以下の項目で示すいくつかの資料もここにまとめて閲覧できるようにした。

　数理情報学部JABEE申請準備委員会委員
　数理情報学部のJABEE(日本技術者教育認定機構)申請検討委員会の一員として、申請の可能性などを調査し、本学部の教育システムを改善する業務を行なっている。