gaxiiiiiiiiiiii

From mathcomp Require Import all_ssreflect.
Require Import Bool.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Class poSet := PoSet {
  base : finType;

gaxiiiiiiiiiiii

From mathcomp Require Export fintype finset ssrbool ssreflect eqtype.


Module Type SIG.
  Parameter T : finType.
  Parameter A : {set T}.
  Parameter F : {set T} -> {set T}.
  Parameter mono : forall (X Y : {set T}), X \subset Y -> F X \subset F Y.
End SIG.

gaxiiiiiiiiiiii

From mathcomp Require Export fintype finset ssrbool ssreflect.



Module Type FinTypeSig.
  Parameter T : finType.
End FinTypeSig.

Module Type ArgFrame (FTS : FinTypeSig).
  Import FTS.

gaxiiiiiiiiiiii

Require Import Ensembles.
From mathcomp Require Import ssreflect.

Arguments Singleton {U}.
Arguments Union {U}.
Arguments Setminus {U}.
Arguments Included {U}.
Arguments Couple {U}.
Arguments Empty_set {U}.

gaxiiiiiiiiiiii

Require Import List Bool  Classical.

Import ListNotations.
From mathcomp Require Import ssreflect ssrbool.
Require Import Ensembles ProofIrrelevance Classical_sets.



Definition var := nat.
Variable fls tru : var.

gaxiiiiiiiiiiii

Require Import List.
Import ListNotations.

Variable var : Type.
Variable tru fls : var.

Inductive prop :=
  | Var : var -> prop
  | Not : prop -> prop
  | And : prop -> prop -> prop

gaxiiiiiiiiiiii

From mathcomp Require Import all_ssreflect.


Variables argument position : finType.
Definition A := [set : argument].
Definition X := [set : position].

Definition Rel := rel position.

Axiom axiomA : 0 < #|argument|.

gaxiiiiiiiiiiii

Require Export Classical.

Module ACTL.
Section Def.


Context {state action : Set} {trans : state -> action -> state -> Prop}
        {tau : action} {tau_eq : forall  s s', trans s tau s' <->  s = s'}.

gaxiiiiiiiiiiii

Parameter Act var : Set.

Axiom var_nat : exists srj : var -> nat, forall n, exists x, srj x = n.

Inductive o : Set := 
    | ff : o 
    | Not : o -> o 
    | Imp : o -> o -> o 
    | Box : Act -> o -> o 
    | Var : var -> o 

gaxiiiiiiiiiiii

提案手法

この章では、行政の性質を証明可能な命題として表現する方法を示す。具体的には、LTS（Labeld Transition System）モデルを用いて、行政を意味するステートマシンGSM（Government State Machine）を定義した。LTSとは、PDL（Propositional Dynamic Logic）やμ計算などの様相論理にて用いられる状態遷移のモデルである。GSMを用いれば、各論理体系において行政の性質を論理命題として記述可能となる。尚、本論文の内容は定理証明支援系のCoqで実装されている。

定義(LTS)

状態の集合Sと、アクションの集合Aが与えられた時、⇒ ⊆ S × A × S となる集合 ⇒ をLTSと呼ぶ