Skip to content

Instantly share code, notes, and snippets.

@y-taka-23
Last active December 23, 2015 10:04
Show Gist options
  • Save y-taka-23/de10a1f36f948cde286f to your computer and use it in GitHub Desktop.
Save y-taka-23/de10a1f36f948cde286f to your computer and use it in GitHub Desktop.
Alloy による命題論理のシークエント計算のモデリング
// ************************************
// 命題論理のシークエント計算のモデル
// ************************************
// 論理式
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment