Alloy による命題論理のシークエント計算のモデリング

alloy_sequent.als

// ************************************
//   命題論理のシークエント計算のモデル
// ************************************

// 論理式
abstract sig Formula {}

// 原子命題
sig Atom extends Formula {}

// 否定演算子
sig Not extends Formula {
    of : one Formula,
}

// 二項演算子
abstract sig BinaryLogicOperator extends Formula {
    left  : one Formula,
    right : one Formula,
}
sig And, Or, Imply extends BinaryLogicOperator {}

// 論理式は循環参照を持たない
fact formulaeAreAcyclic {
    all f : Formula | f not in f.^(of + right + left)
}

// シークエント
sig Sequent {
    antecedents : set Formula,  // 前件
    succedents  : set Formula,  // 後件
}

// 推論規則
abstract sig InferenceRule {
    premises   : some Sequent,  // 前提
    conclusion : one Sequent,   // 結論
}

sig NotRight extends InferenceRule {
} {
    one premises
    some f : Formula, n : Not {
        f in premises.antecedents
        f in n.of
        n in conclusion.succedents
        premises.antecedents - f = conclusion.antecedents
        premises.succedents = conclusion.succedents - n
    }
}

sig NotLeft extends InferenceRule {
} {
    one premises
    some f : Formula, n : Not {
        f in premises.antecedents
        f in n.of
        n in conclusion.succedents
        premises.antecedents + n = conclusion.antecedents
        premises.succedents = conclusion.succedents + f
    }
}

sig AndRight extends InferenceRule {
} {
    some p1, p2 : Sequent, f1, f2 : Formula, a : And {
        premises = p1 + p2
        f1 in p1.succedents
        f2 in p2.succedents
        f1 in a.left
        f2 in a.right
        a in conclusion.succedents
        p1.antecedents = conclusion.antecedents
        p2.antecedents = conclusion.antecedents
        p1.succedents - f1 = conclusion.antecedents - a
        p1.succedents - f2 = conclusion.antecedents - a
    }
}

sig AndLeft extends InferenceRule {
} {
    one premises
    some f1, f2 : Formula, a : And {
        f1 + f2 in premises.antecedents
        f1 in a.left
        f2 in a.right
        a in conclusion.antecedents
        premises.antecedents - (f1 + f2) = conclusion.antecedents - a
        premises.succedents = conclusion.succedents
    }
}

sig OrRight extends InferenceRule {
} {
    one premises
    some f1, f2 : Formula, o : Or {
        f1 + f2 in premises.succedents
        f1 in o.left
        f2 in o.right
        o in conclusion.succedents
        premises.antecedents = conclusion.antecedents
        premises.succedents - (f1 + f2) = conclusion.succedents - o
    }
}

sig OrLeft extends InferenceRule {
} {
    some p1, p2 : Sequent, f1, f2 : Formula, o : Or {
        premises = p1 + p2
        f1 in p1.antecedents
        f2 in p2.antecedents
        f1 in o.left
        f2 in o.right
        o in conclusion.antecedents
        p1.antecedents - f1 = conclusion.antecedents - o
        p2.antecedents - f2 = conclusion.antecedents - o
        p1.succedents = conclusion.antecedents
        p1.succedents = conclusion.antecedents
    }
}

sig ImplyRight extends InferenceRule {
} {
    one premises
    some f1, f2 : Formula, i : Imply {
        f1 in premises.antecedents
        f2 in premises.succedents
        f1 in i.left
        f2 in i.right
        i in conclusion.succedents
        premises.antecedents - f1 = conclusion.antecedents
        premises.succedents - f2 = conclusion.succedents - i
    }
}

sig ImplyLeft extends InferenceRule {
} {
    some p1, p2 : Sequent, f1, f2 : Formula, i : Imply {
        premises = p1 + p2
        f1 in p1.succedents
        f2 in p2.antecedents
        f1 in i.left
        f2 in i.right
        i in conclusion.antecedents
        p1.antecedents = conclusion.antecedents - i
        p2.antecedents - f2 = conclusion.antecedents - i
        p1.succedents - f1 = conclusion.succedents
        p2.succedents = conclusion.succedents
    }
}

// 登場するすべての論理式が証明に使用される
fact noIsolatedFormulae {
    Formula in Sequent.(antecedents + succedents)
}

// 最終的に証明したいシークエント
sig RootSequent in Sequent {
} {
    this not in InferenceRule.premises
}

// 始シークエント
sig InitialSequent in Sequent {
} {
    some antecedents & succedents
}

// 証明図は二分木を構成する
fact rulesFormAProofTree {
    one RootSequent
    Sequent - InferenceRule.conclusion = InitialSequent
    no r : InferenceRule | r in r.^(conclusion.~premises)
    all s : Sequent - InitialSequent | one conclusion.s
}

// 無矛盾性
assert consistency {
    no s : Sequent | s.antecedents = none && s.succedents = none
}
check consistency for 3

// 排中律
pred excludedMiddle {
    some x : Atom, n : Not, o : Or {
        x in o.left
        n in o.right
        x in n.of
        RootSequent.antecedents = none
        RootSequent.succedents = o
    }
}
run excludedMiddle for 3