import f11,f26,f27,...
# 年金原簿 honnin_ladyA, setainushi_ladyA, haiguusha_ladyA s日本国内に住所を有する="DD((1955,5,10),(2020,12,31))"
s保険料納付済み="MM((1999,12),(2007,1))"
s保険料半額免除="MM((2007,2),(2008,1))"
...
日本国内に住所を有する=eval(s日本国内に住所を有する) 保険料納付済み=eval(s保険料納付済み)
保険料半額免除=eval(s保険料半額免除) ...
# 年金原簿操作関数
ADD=lambda x,y: "OR(" + x + ",M(" + y + "))"
DEL=lambda x,y: "AND(" + x + ",NOT(M(" + y + ")))"
...
# 年金処理関数
def 保険料を納付(y,m): # y,m:int m1=Int(’m1’)
t=Solver()
t.add(m1==通月(y,m),
And(f11.第一号被保険者期間(m1),Not(保険料納付済み(m1)))) if t.check()==sat:
s保険料納付済み=ADD(s保険料納付済み,’(’ + str(y) + ’,’ + str(m) + ’)’) else:
print(’保険料納付不要’) def 年金額確認(y,m,d):
t=Solver()
t.add(f26.老齢基礎年金の受給権者(通日(y,m,d))) if t.check()==sat:
return f27.老齢基礎年金額 else:
print(’受給資格なし’) ...
# Main Loop while True:
val=input("処理の種類を入力 ") if val=="現在の年金額":
m=input("月を入力 ") d=input("日を入力 ")
print(年金額確認(int(y),int(m),int(d))) elif val=="保険料納付":
y=input("年を入力 ") m=input("月を入力 ")
保険料を納付(int(y),int(m)) elif ...
...
else:
print("処理終了") break
付録 A 論理式化から見た条文
国民年金法は，国民年金基金及び国民年金基金連合会，附則を除くと165条からなるが，ここで は，各条文がその内容に関して論理式記述にもとづく検査や検証が有意義なものであるかについて 概観した．結論的には，全165条は以下の３つのカテゴリーa,b,cに分類される．この分類は概略 的なものではあるが，広い意味で形式化が有効のものが全体の7割，その内で述語論理による形式 化が有効なものが約6割あることがわかる．
a 条文中の用語や概念などに関して論理的関係が書かれており，論理式記述を行う事が条文の 理解や分析に有効であるもの 73条
b 複雑な論理的関係は書かれいないが，組織間の関連や権限の委譲などの書かれており，その 形式化が法令の構造的理解や分析に有効なもの 42条
c 財政，罰則などが書かれ，論理式記述の必要性が低いもの 50条
以下，各条文ごとにカテゴリーを示す．（ただし，第十章国民年金基金及び国民年金基金連合会，附 則は除く）
第一章 総則
第一条〜第四条の三 c,目的や財政など
第五条 用語の定義 a,保険料の納付や免除に関する定義 第六条 事務の区分 b,市町村における受託事務
第二章 被保険者
第七条 被保険者資格 a,被保険者の資格の定義
第八条 資格取得の時期 a,条文は不完全，また，その意味は薄い 第九条 資格喪失の時期 a,同上
第十条 削除
第十一条,十一条の二 被保険者期間の計算 a,被保険者期間の計算に必要な定義
第十二条,十二条の二 届け出 b,被保険者の資格の変更などの届け出に関連して，被保険者や事 業主，自治体，厚労大臣など関連組織の役割と関係
第十三条 年金手帳 b,年金手帳の作成と交付 厚労大臣⇒ 被保険者 第十四条 年金原簿 a,年金業務に必要な被保険者データの記録
第十四条の二〜四 訂正の請求，方針，措置 b,被保険者による年金原簿訂正請求⇒厚労大臣，社 会保障審議会
第十四条の五 被保険者に関する情報の提供 b,厚労大臣⇒ 被保険者 第三章 給付
第一節 通則
第十六条 裁定 b, 厚労大臣、被保険者
第十六条の二 調整期間 c, 政府が年金当別会計積立金などを勘案して給付額の調整 第十七条 端数処理 a, 50銭四捨五入
第十八条 年金の支給期間及び支給期月 a,年金の支給，停止を定める基本論理 第十八条の二 二月期支給の年金加算 a,切り捨て端数の二月期への加算 第十八条の三 死亡の推定 a,死亡に時期が明確で内場合の死亡推定の論理 第十八条の四 失踪 a,失踪に関して同上
第十九条 未支給年金 a,受給権者死亡の場合に年金を実際に受け取る人間の指定 第二十条 併給の調整 a,複数の基礎年金が受給可能となった場合の選択方式 第二十条の二 受給権者の申出による支給停止 a
第二十一条、二十一条の二 年金の支払の調整 a, 誤って支払った年金は他の年金給付の内金 第二十二条 障害賠償請求権 b,第三者が原因の傷害に関して，政府が受給権者から請求権を取得 第二十三条 不正利得の徴収 b,偽りによる不正受給受給者⇒厚労大臣
第二十四条 受給権の保護 c, 年金権は担保，譲渡，差し押さえ不可 第二十五条 公課の禁止 c,年金額を税金の算定額にできない
第二節 老齢基礎年金 第二十六条 支給要件 a 第二十七条 年金額 a
第二十七の二、三、四、五 改定率の改定等 a 第二十八条 支給の繰下げ a
第二十九条 失権 a 第三節 障害基礎年金
第三十条、三十条の二、三、四 支給要件 a,初診日，障害の程度，年齢などとの関係 第三十一条、三十二条 併給の調整 a,新たな障害による受給権が発生した場合の調整 第三十三条、三十三条の二 年金額 a
第三十四条 障害の程度が変わつた場合の年金額の改定 a 第三十五条 失権 a
第三十六条、三十六条の二，三，四 支給停止 a 第四節 遺族基礎年金
第三十七条 支給要件 a,被保険者の子または配偶者に支給 第三十七の二 遺族の範囲 a
第三十八条 遺族の範囲 a
第三十九条、三十九条の二 年金額 a 第四十条 失権 a
第四十一条、四十一条の一、四十二条 支給停止 a 第五節 付加年金、寡婦年金及び死亡一時金 第一款 付加年金
第四十三条 支給要件 a,付加的保険料納付者が老齢基礎年金受給時 第四十四条 年金額 a
第四十五条 国民年金基金又は国民年金基金連合会の解散の場合の取扱い c 第四十六条 支給の繰下げ a,老齢基礎年金の繰下と同期
第四十七条 支給停止 a,老齢基礎年金と同期 第四十八条 失権 a,同上
第二款 寡婦年金
第四十九条 支給要件 a,夫が年金を貰う前に死亡した時に妻が受給 第五十条 年金額 a,夫が貰う額の3/4
第五十一条 失権 a 第五十二条 支給停止 a 第三款 死亡一時金
第五十二条の二 支給要件 a,年金の受給まえに死亡した人の遺族に 第五十二条の三 遺族の範囲及び順位等 a
第五十二条の四、五 金額 a
第五十二条の六 支給の調整 a, 一時金 or寡婦年金 第五十三条〜六十八条 削除
第六節 給付の制限
第六十九条〜七十三条 c,故意の事故、書類の不提出、犯罪行為などの場合は支給しない。
第四章 国民年金事業の円滑な実施を図るための措置 第七十四条 c, 教育、広報、年金機構など
第五章 積立金の運用
第七十五条〜八十条 c, 目的、運用、職員の責務、秘密保持義務、処分 第八十一条〜八十四条 削除
第六章 費用
第八十五条 国庫負担 c,毎年の国庫負担額を規定する数式 第八十六条 事務費の交付 c, 地方自治体に
第八十七条 保険料 a,保険料の月額
第八十七条の二 a,保険料の追加400円の納付,付加年金のため 第八十八条 保険料の納付義務 b,配偶者、世帯主、被保険者 第八十八条の二 a,妊婦は免除
第八十九条 a, 法定免除
第九十条、九十条の二、三 a, 申請免除、学生特例 第九十一条 保険料の納期限 b, 被保険者⇒厚労大臣？
第九十二条 保険料の通知及び納付 b,厚労大臣⇒被保険者（毎年度）
第九十二条の二 口座振替による納付 b, 通知：被保険者⇒厚労大臣
第九十二条の三〜六 保険料の納付委託 b, 被保険者、厚労大臣、納付受託者(年金基金，市 町村、．．．）、帳簿の立ち入り検査
第九十三条 保険料の前納 a
第九十四条 保険料の追納 a, 免除された保険料の納付
第九十四条の二、三、四 基礎年金拠出金 c, 共済年金、厚生年金などから基礎年金に一定 額の拠出
第九十四条の五 報告 c, 厚労大臣、実施期間（共済組合など）
第九十四条の六 第二号被保険者及び第三号被保険者に係る特例 c,第二、三号被保険者は保険料 納付不要
第九十五条 徴収 c, 国税に倣って徴収
第九十五条の二 国民年金基金又は国民年金基金連合会の解散に伴う責任準備金相当額の徴収 c 第九十六条 督促及ぶ滞納処分 c,具体的な督促、処分の方法
第九十七条 延滞金 c,滞納者に対する延滞金の計算方法
第九十八条 先取特権 c,徴収金の先取り特権の順位 国税、地方税の次 第九十九、百条 削除
第七章 不服申し立て
第百一条 不服申し立て c,被保険者⇒社会保険審議会 第百一条の二 審査請求と訴訟との関係 c
第八章 雑則
第百二条 時効 c,給付を受ける権利は5年，保険料の請求は2年
第百三条 期間の計算 c, この法律内で定義されていなものは、民法による 第百四条 戸籍事項の無料証明 c
第百五条 届出等 b,被保険者、受給権者、厚労大臣、市町村長 第百六条 被保険者に関する調査 b,厚労大臣⇒被保険者 第百七条 受給権者に関する調査 b, 厚労大臣⇒受給権者
第百八条、第百八条の二、二の二，三 資料の提供など b,厚労大臣⇒関連諸機関 第百八条の四 基礎年金番号の利用制限等 b,住民基本台帳に準ずる
第百九条 国民年金事務組合 b, 被保険者の行う届出(第十二条）を行ってくれる事務組織 第百九条の二 全額免除申請の事務手続に関する特例 b, 被保険者に代わって申請手続き行う
もの
第百九条の二の二 学生納付特例の事務手続に関する特例 b, 被保険者に代わって申請手続き行 うもの
第百九条の三 保険料納付確認団体 b, 団体の被保険者の保険料が納付されていないことを確認
⇒被保険者
第百九条の四 年金機構への厚生労働大臣の権限に係る事務の委任 b,厚労大臣⇒機構 第百九条の五 財務大臣への権限の委譲 b,保険料未納者の対応を税務署に行わせるために、関連
の権限を財務大臣に委譲