decidable_separationLogic/doc/ds.tex

32 \newcommand{\modelsds}{{\models_{\textit{ds}}\ }}
463 \texttt{ds\_value}, expressions by the $\HOL$ datatype
464 \texttt{ds\_expression}. Using these basic datatypes, the datatypes \texttt{ds\_pure\_formula} and
465 \texttt{ds\_spatial\_formula} are defined for pure and spatial formulae,
561 \subsubsection{\texttt{ds\_inference\_REMOVE\_TRIVIAL}}
606 The $\HOL$ conversion \texttt{ds\_inference\_REMOVE\_TRIVIAL\_\_\_CONV} is an
615 \subsubsection{\texttt{ds\_inference\_AXIOM}}
635 This inference is implemented by \texttt{ds\_inference\_AXIOM\_\_\_CONV}.
638 \subsubsection{\texttt{ds\_inference\_SUBSTITUTION}}
650 This inference is implemented by \texttt{ds\_inference\_SUBSTITUTION\_\_\_CONV}.
653 \subsubsection{\texttt{ds\_inference\_HYPOTHESIS}}
684 \texttt{ds\_inference\_HYPOTHESIS\_\_\_CONV}. Additionally, this conversion
688 \subsubsection{\texttt{ds\_inference\_FRAME}}
746 These inferences are implemented by \texttt{ds\_inference\_FRAME\_\_\_CONV}
750 theorem. \texttt{ds\_inference\_FRAME\_\_\_IMPL\_\_\_CONV} applies the general
754 \subsubsection{\texttt{ds\_inference\_INCONSISTENT}}
791 \texttt{ds\_inference\_INCONSISTENT\_\_\_CONV}.
794 \subsubsection{\texttt{ds\_inference\_NIL\_NOT\_LVAL}}
811 \texttt{ds\_inference\_NIL\_NOT\_LVAL\_\_\_CONV}. To prevent the inference
816 \subsubsection{\texttt{ds\_inference\_PARTIAL}}
850 \texttt{ds\_inference\_PARTIAL\_\_\_CONV}. To prevent the inference
856 \subsubsection{\texttt{ds\_inference\_SIMPLE\_UNROLL}}
887 These inferences are implemented by \texttt{ds\_inference\_SIMPLE\_UNROLL\_\_\_CONV}.
891 \subsubsection{\texttt{ds\_inference\_STRENGTHEN\_PRECONDITION}}
915 These inferences are implemented by \texttt{ds\_inference\_PRECONDITION\_STRENGTHEN\_\_\_CONV}.
918 \subsubsection{\texttt{ds\_inference\_PRECONDITION\_CASES}}
928 This inference is implemented by \texttt{ds\_inference\_PRECONDITION\_CASES\_\_\_CONV}.
931 \subsubsection{\texttt{ds\_inference\_UNROLL}}
973 \texttt{ds\_inference\_UNROLL\_LIST\_\_\_CONV} implements the list
977 \texttt{ds\_inference\_UNROLL\_LIST\_\_\_NON\_EMPTY\_\_\_CONV}.
979 \texttt{ds\_inference\_UNROLL\_BIN\_TREE\_\_\_CONV}.
982 \subsubsection{\texttt{ds\_inference\_UNROLL\_RIGHT\_CASES}}
1004 \texttt{ds\_inference\_UNROLL\_RIGHT\_CASES\_\_\_CONV}.
1007 \subsubsection{\texttt{ds\_inference\_APPEND\_LIST}}
1008 A combination of the inferences \texttt{ds\_inference\_UNROLL},
1009 \texttt{ds\_inference\_SIMPLE\_UNROLL} and \texttt{ds\_inference\_FRAME} leads
1037 These inferences are implemented by \texttt{ds\_inference\_LIST\_APPEND\_\_\_CONV}.
1044 form a decision procedure (\texttt{ds\_DECIDE\_CONV}) for entailments not containing the general $\sftree$
1262 \bibliography{ds}