Изображение:Pvs tree.png

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(загружена новая версия «Изображение:Pvs tree.png»)
(Да-да, надо бы обновить)
Строка 1: Строка 1:
-
Автор: Василий Мерзляков.
+
Автор: Игорь Бронштейн.
Исходный dot-файл:
Исходный dot-файл:
Строка 31: Строка 31:
"node4" -> "node5"
"node4" -> "node5"
"node6" [
"node6" [
-
label = "{[-1] 0 \> 7\n[-2] i = 0|[1] EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}"
+
label = "{[-1] 0 \> 7|[1] EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}"
shape = "record"
shape = "record"
]
]
Строка 114: Строка 114:
"node22" -> "node23"
"node22" -> "node23"
"node24" [
"node24" [
-
label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] f!1 = 0\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 - 3) + 5 * 2}"
+
label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 - 3) + 5 * 2}"
shape = "record"
shape = "record"
]
]
Строка 130: Строка 130:
"node21" -> "node26"
"node21" -> "node26"
"node27" [
"node27" [
-
label = "(assert)"
+
label = "(replace -1)"
-
style = "filled"
+
-
fillcolor = "green"
+
]
]
"node26" -> "node27"
"node26" -> "node27"
"node28" [
"node28" [
-
label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
+
label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] j!1 + 1 \> 7|[1] t!1 - 3 \>= 0}"
shape = "record"
shape = "record"
]
]
-
"node19" -> "node28"
+
"node27" -> "node28"
"node29" [
"node29" [
-
label = "(inst 1 \"t!1 + 2\" \"f!1 - 1\")"
+
label = "(assert)"
 +
style = "filled"
 +
fillcolor = "green"
]
]
"node28" -> "node29"
"node28" -> "node29"
"node30" [
"node30" [
-
label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 + 2) + 5 * (f!1 - 1)}"
+
label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
shape = "record"
shape = "record"
]
]
-
"node29" -> "node30"
+
"node19" -> "node30"
"node31" [
"node31" [
-
label = "(assert)"
+
label = "(inst 1 \"t!1 + 2\" \"f!1 - 1\")"
-
style = "filled"
+
-
fillcolor = "green"
+
]
]
"node30" -> "node31"
"node30" -> "node31"
"node32" [
"node32" [
-
label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] f!1 - 1 \>= 0}"
+
label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 + 2) + 5 * (f!1 - 1)}"
shape = "record"
shape = "record"
]
]
-
"node29" -> "node32"
+
"node31" -> "node32"
"node33" [
"node33" [
label = "(assert)"
label = "(assert)"
Строка 167: Строка 165:
"node32" -> "node33"
"node32" -> "node33"
"node34" [
"node34" [
-
label = "{[-1] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
+
label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] f!1 - 1 \>= 0}"
shape = "record"
shape = "record"
]
]
-
"node15" -> "node34" [label = "посылку в консеквенты"]
+
"node31" -> "node34"
"node35" [
"node35" [
-
label = "(case \"j!1 = 7\")"
+
label = "(assert)"
 +
style = "filled"
 +
fillcolor = "green"
]
]
"node34" -> "node35"
"node34" -> "node35"
"node36" [
"node36" [
-
label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
+
label = "{[-1] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
shape = "record"
shape = "record"
]
]
-
"node35" -> "node36"
+
"node15" -> "node36" [label = "посылку в консеквенты"]
"node37" [
"node37" [
-
label = "(inst 2 \"1\" \"1\")"
+
label = "(case \"j!1 = 7\")"
]
]
"node36" -> "node37"
"node36" -> "node37"
"node38" [
"node38" [
-
label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] j!1 + 1 = 3 * 1 + 5 * 1}"
+
label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
shape = "record"
shape = "record"
]
]
"node37" -> "node38"
"node37" -> "node38"
"node39" [
"node39" [
-
label = "(assert)"
+
label = "(inst 2 \"1\" \"1\")"
-
style = "filled"
+
-
fillcolor = "green"
+
]
]
"node38" -> "node39"
"node38" -> "node39"
"node40" [
"node40" [
-
label = "{[-1] j!1 /= 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
+
label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] j!1 + 1 = 3 * 1 + 5 * 1}"
shape = "record"
shape = "record"
]
]
-
"node35" -> "node40"
+
"node39" -> "node40"
"node41" [
"node41" [
label = "(assert)"
label = "(assert)"
Строка 206: Строка 204:
]
]
"node40" -> "node41"
"node40" -> "node41"
 +
"node42" [
 +
label = "{[-1] j!1 /= 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
 +
shape = "record"
 +
]
 +
"node37" -> "node42"
 +
"node43" [
 +
label = "(assert)"
 +
style = "filled"
 +
fillcolor = "green"
 +
]
 +
"node42" -> "node43"
}
}
</pre>
</pre>

Версия 16:42, 6 декабря 2008

Автор: Игорь Бронштейн.

Исходный dot-файл: 

digraph PVSTree {
    "node0" [
        label = "{ |[1] FORALL (i : nat) : (i \> 7) IMPLIES EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node1" [
        label = "(induct \"i\")"
    ]
    "node0" -> "node1"
    "node2" [
        label = "{[-1] i = 0|[1] (i \> 7) IMPLIES EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node1" -> "node2" [label = "базис индукции"]
    "node3" [
        label = "(flatten 1)"
    ]
    "node2" -> "node3"
    "node4" [
        label = "{[-1] i \> 7\n[-2] i = 0|[1] EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node3" -> "node4"
    "node5" [
        label = "(replace -2)"
    ]
    "node4" -> "node5"
    "node6" [
        label = "{[-1] 0 \> 7|[1] EXIST (t : nat, f : nat) : i = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node5" -> "node6"
    "node7" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node6" -> "node7"
    "node8" [
        label = "{ |[1] FORALL (j : nat) :\n(j \> 7) IMPLIES EXIST (t : nat, f : nat) : j = 3 * t + 5 * f\nIMPLIES\n(j + 1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node1" -> "node8" [label = "индуктивный переход"]
    "node9" [
        label = "(skolem! 1)"
    ]
    "node8" -> "node9"
    "node10" [
        label = "{ |[1] (j!1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j!1 = 3 * t + 5 * f\nIMPLIES\n(j!1 + 1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node9" -> "node10"
    "node11" [
        label = "(flatten 1)"
    ]
    "node10" -> "node11"
    "node12" [
        label = "{[-1] (j!1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j!1 = 3 * t + 5 * f|[1] (j!1 + 1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node11" -> "node12"
    "node13" [
        label = "(flatten 1)"
    ]
    "node12" -> "node13"
    "node14" [
        label = "{[-1] j!1 + 1 \> 7\n[-2] (j!1 \> 7) IMPLIES EXIST (t : nat, f : nat) : j!1 = 3 * t + 5 * f|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node13" -> "node14"
    "node15" [
        label = "(split -2)"
    ]
    "node14" -> "node15"
    "node16" [
        label = "{[-1] EXIST (t : nat, f : nat) : j!1 = 3 * t + 5 * f\n[-2] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node15" -> "node16" [label = "следствие в антецеденты"]
    "node17" [
        label = "(skolem! -1)"
    ]
    "node16" -> "node17"
    "node18" [
        label = "{[-1] j!1 = 3 * t!1 + 5 * f!1\n[-2] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node17" -> "node18"
    "node19" [
        label = "(case \"f!1 = 0\")"
    ]
    "node18" -> "node19"
    "node20" [
        label = "{[-1] f!1 = 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node19" -> "node20"
    "node21" [
        label = "(inst 1 \"t!1 - 3\" \"2\")"
    ]
    "node20" -> "node21"
    "node22" [
        label = "{[-1] f!1 = 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 - 3) + 5 * 2}"
        shape = "record"
    ]
    "node21" -> "node22"
    "node23" [
        label = "(replace -1)"
    ]
    "node22" -> "node23"
    "node24" [
        label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 - 3) + 5 * 2}"
        shape = "record"
    ]
    "node23" -> "node24"
    "node25" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node24" -> "node25"
    "node26" [
        label = "{[-1] f!1 = 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] t!1 - 3 \>= 0}"
        shape = "record"
    ]
    "node21" -> "node26"
    "node27" [
        label = "(replace -1)"
    ]
    "node26" -> "node27"
    "node28" [
        label = "{[-1] j!1 = 3 * t!1 + 5 * 0\n[-2] j!1 + 1 \> 7|[1] t!1 - 3 \>= 0}"
        shape = "record"
    ]
    "node27" -> "node28"
    "node29" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node28" -> "node29"
    "node30" [
        label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node19" -> "node30"
    "node31" [
        label = "(inst 1 \"t!1 + 2\" \"f!1 - 1\")"
    ]
    "node30" -> "node31"
    "node32" [
        label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] j!1 + 1 = 3 * (t!1 + 2) + 5 * (f!1 - 1)}"
        shape = "record"
    ]
    "node31" -> "node32"
    "node33" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node32" -> "node33"
    "node34" [
        label = "{[-1] f!1 /= 0\n[-2] j!1 = 3 * t!1 + 5 * f!1\n[-3] j!1 + 1 \> 7|[1] f!1 - 1 \>= 0}"
        shape = "record"
    ]
    "node31" -> "node34"
    "node35" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node34" -> "node35"
    "node36" [
        label = "{[-1] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node15" -> "node36" [label = "посылку в консеквенты"]
    "node37" [
        label = "(case \"j!1 = 7\")"
    ]
    "node36" -> "node37"
    "node38" [
        label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node37" -> "node38"
    "node39" [
        label = "(inst 2 \"1\" \"1\")"
    ]
    "node38" -> "node39"
    "node40" [
        label = "{[-1] j!1 = 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] j!1 + 1 = 3 * 1 + 5 * 1}"
        shape = "record"
    ]
    "node39" -> "node40"
    "node41" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node40" -> "node41"
    "node42" [
        label = "{[-1] j!1 /= 7\n[-2] j!1 + 1 \> 7|[1] j!1 \> 7\n[2] EXIST (t : nat, f : nat) : j!1 + 1 = 3 * t + 5 * f}"
        shape = "record"
    ]
    "node37" -> "node42"
    "node43" [
        label = "(assert)"
        style = "filled"
        fillcolor = "green"
    ]
    "node42" -> "node43"
}

История файла

Нажмите на дату, чтобы просмотреть как тогда выглядел файл.

Дата/времяУчастникРазмерыРазмер файлыПримечание
(текущая)20:48, 14 января 2009Bronikkk (Обсуждение | вклад)1687 × 2485246 КБ
17:06, 7 декабря 2008Bronikkk (Обсуждение | вклад)1687 × 2485246 КБАвтор: Игорь Бронштейн
17:00, 7 декабря 2008Bronikkk (Обсуждение | вклад)1687 × 2485245 КБВладелец: Игорь Бронштейн
16:41, 6 декабря 2008Bronikkk (Обсуждение | вклад)1687 × 2485244 КБ
03:23, 5 декабря 2008ESyr01 (Обсуждение | вклад)1708 × 2531248 КБАвтор: Василий Мерзляков.

Следующие страницы ссылаются на данный файл:

Получено с http://esyr.us/wiki/%D0%98%D0%B7%D0%BE%D0%B1%D1%80%D0%B0%D0%B6%D0%B5%D0%BD%D0%B8%D0%B5:Pvs_tree.png
Личные инструменты
Разделы