From: Jean-François Couchot Date: Tue, 17 Dec 2013 12:34:47 +0000 (+0100) Subject: symbols X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/bibliographie.git/commitdiff_plain/ca904fb2c99239a78882b7987764f59a48bcc202 symbols --- diff --git a/symbols/macroE.tex b/symbols/macroE.tex new file mode 100755 index 0000000..d234e71 --- /dev/null +++ b/symbols/macroE.tex @@ -0,0 +1,277 @@ +\newtheorem{Corol}{Corollary} +\newtheorem{Prop}{Proposition} +\newtheorem{Conjec}{Conjecture} +\newtheorem{lemma}{Lemma} +\newtheorem{Def}{Definition} +\newtheorem{theorem}{Theorem} + + +\newtheorem{definition}{Definition} +\newtheorem{notation}{Notation} +\newtheorem{proposition}{Proposition} +\newtheorem{corollary}{Corollary} +\newtheorem{remark}{Remark} +\newtheorem{example}{Example} +%\newtheorem{proof}{Proof} + + + + + + + +%{\theoremheaderfont{\normalfont\bfseries} +%\theorembodyfont{\slshape} +%\theoremsymbol{\ensuremath{\diamondsuit}} + +%\theoremseparator{:} + + +\newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}} +\newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}} + + + +%%%%%%%%%% outils langages dédiés +\newcommand{\harvey}[0]{\ensuremath{\textsf{haRVey}\xspace}} +\newcommand{\barvey}[0]{\ensuremath{\textsf{barvey}\xspace}} +\newcommand{\bamTorv}[0]{\ensuremath{\textsf{bam2rv}\xspace}} +\newcommand{\rvqe}[0]{\ensuremath{\textsf{rvqe}\xspace}} +\newcommand{\Why}[0]{\ensuremath{\textsf{Why}\xspace}} +\newcommand{\Be}[0]{\textsf{B}\xspace} +\newcommand{\Zed}[0]{\ensuremath{\textsf{Z}\xspace}} + + + +%%%%%%%%% Langages premier ordre +\newcommand{\Lang}[0]{\ensuremath{{\cal L}}} +\newcommand{\Sorts}[0]{\ensuremath{{\cal S}}} +\newcommand{\Vars}[0]{\ensuremath{{\cal V}}} +\newcommand{\Funcs}[0]{\ensuremath{{\cal F}}} +\newcommand{\Preds}[0]{\ensuremath{{\cal P}}} +\newcommand{\arite}[0]{\ensuremath{{\alpha}}} +\newcommand{\sorte}[0]{\ensuremath{{\sigma}}} +\newcommand{\tauTerm}[0]{\textit{$\tau$-terme}\xspace} +\newcommand{\tauITerm}[1]{\textit{$\tau_{#1}$-term}\xspace} +\newcommand{\atome}[0]{\textit{atome}\xspace} +\newcommand{\fpoms}[0]{\textit{fpoms}\xspace} +\newcommand{\VLibre}[1]{\Vars_{\textit{lib}}(#1)} +\newcommand{\congruenceE}[0]{\ensuremath{{\cal E}}} +\newcommand{\preInterpret}[1]{\ensuremath{[ #1 ]}} +\newcommand{\preInterpretSSET}[1]{\preInterpret{#1}} +\newcommand{\preInterpretBAES}[1]{I'(#1)} +\newcommand{\preinterpret}[0]{\preInterpret{\,}} +%\newcommand{\valuationX}[1]{\ensuremath{{\preInterpret{#1}}_{\rho}}} +%\newcommand{\valuation}[0]{\valuationX{\,}} +\newcommand{\valuationSSET}[1]{\valuation(#1)} +\newcommand{\valuationBAES}[1]{\valuation'(#1)} +\newcommand{\valuationX}[1]{\valuation(#1)} +\newcommand{\valuation}[0]{\ensuremath{\rho}\xspace} +\newcommand{\etat}[0]{\ensuremath{\rho}} +\newcommand{\constt}[1]{\ensuremath{\textsf{#1}}} +\newcommand{\termSet}[0]{t} + +%%%%%%%% SSET -> BAES +\newcommand{\sset}[0]{\ensuremath{\mathit{SSET}}} +\newcommand{\axCod}[0]{\ensuremath{\delta}} +\newcommand{\mty}[0]{\ensuremath{\mathsf{mty}}} +\newcommand{\ttrue}[0]{\ensuremath{\mathsf{tt}}} +\newcommand{\tfalse}[0]{\ensuremath{\mathsf{ff}}} + + + +%%%%%%%%%%%% interprétation modeles +\newcommand{\interpretI}[0]{\ensuremath{{\cal I}}\xspace} +\newcommand{\classInterpret}[0]{\ensuremath{\mathbf{I}\xspace}} +\newcommand{\ltrue}[0]{\ensuremath{\top}} +\newcommand{\lfalse}[0]{\ensuremath{\bot}} +\newcommand{\modele}[0]{\ensuremath{\Vdash}} +\newcommand{\deduc}[0]{\vdash} + +\newcommand{\conseq}[0]{\ensuremath{\vDash}} +\newcommand{\herbrandU}[0]{\ensuremath{\mathbbm{H}}\xspace} + + +%%%%%%%%% réels entiers complexes +\newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}} +\newcommand{\Z}[0]{\ensuremath{\mathbb{Z}}} +\newcommand{\R}[0]{\ensuremath{\mathbb{R}}} +\newcommand{\Bool}[0]{\ensuremath{\mathds{B}}} +\newcommand{\StratSet}[0]{\ensuremath{\mathbb{S}}} + +%%%%%%%%% logique +\newcommand{\impliq}[0]{\ensuremath{{\Rightarrow}}} +\newcommand{\equival}[0]{\ensuremath{{\Leftrightarrow}}} + + +%%%%%%%%%%%%%%% quantifs +\newcommand{\sortedForall}[3]{\ensuremath{(\forall_{#1} #2\, . \, #3)}} +\newcommand{\sortedExists}[3]{\ensuremath{(\exists_{#1} #2\, . \, #3)}} +\newcommand{\sortedQ}[3]{\ensuremath{(Q_{#1} #2\, . \, #3)}} +\newcommand{\Forall}[2]{\ensuremath{(\forall #1\, . \, #2)}} +\newcommand{\qnnf}[0]{\ensuremath{_{\textit{nf}}}} +\newcommand{\gq}{\ensuremath{\mathsf{gq}}} +\newcommand{\gqe}{\ensuremath{\mathsf{gqe}}} +\newcommand{\bdd}[1]{\textit{bdd}(#1)} + + +%%%%%%%%%%%%% grammaire +\newcommand{\regleSep}[0]{\mathtt{~\textbf{|}~}} +\newcommand{\regleDeriv}[0]{\mathtt{::=}} + +%%%%%%%%%%%% Transformation de formules +\newcommand{\transfo}[0]{\ensuremath{{\rightarrow}}} +\newcommand{\negativeForm}[1]{\ensuremath{\textit{neg}({#1})}} +\newcommand{\cnf}[1]{\ensuremath{\textit{cnf}({#1})}} +\newcommand{\dnf}[1]{\ensuremath{\textit{dnf}({#1})}} +\newcommand{\polar}[1]{\ensuremath{\textit{pol}(#1)}} + +%%%%%%%%%%%% Systèmes de transitions +\newcommand{\statesVars}[0]{\ensuremath{X}} +\newcommand{\statesSet}[0]{\ensuremath{{\Sigma}}} +\newcommand{\initialAssertion}[0]{\ensuremath{I}} +\newcommand{\transSymbol}[0]{\ensuremath{{\rightarrow}}} +\newcommand{\transLabel}[0]{\ensuremath{{\textit{act}}}} +\newcommand{\prodASync}[0]{\ensuremath{\otimes}} +\newcommand{\prodSync}[0]{\ensuremath{\oplus}} + +\newcommand{\execTS}[1]{\ensuremath{[[ #1 ]]}} + +%%%%%%%%%%%%%%%% construction de formules +\newcommand{\ite}[3]{\textit{ite}(#1,#2,#3)} +\newcommand{\iteRV}[3]{\mathsf{ite}(#1,#2,#3)} +\newcommand{\eqd}[0]{\ensuremath{=_{\textit{\small{def}}}}} +\newcommand{\instruction}[1]{\xspace{\sf #1}\xspace} +\newcommand{\ifB}[0]{\instruction{if~}} +\newcommand{\thenB}[0]{\instruction{~then~}} +\newcommand{\elseB}[0]{\instruction{~else~}} +\newcommand{\skipB}[0]{\instruction{skip}} + + +%%%%%%%%%%%%% symboles fonctionnels dans des théories +\newcommand{\select}[2]{\ensuremath{\mathsf{rd}(#1,#2)}} +\newcommand{\store}[3]{\ensuremath{\mathsf{wr}(#1,#2,#3)}} +\newcommand{\InsO}[0]{\ensuremath{\mathsf{ins}}} +\newcommand{\Ins}[2]{\ensuremath{\InsO(#1,#2)}} +\newcommand{\enumO}[0]{\ensuremath{\mathsf{enum}}} +\newcommand{\enum}[1]{\ensuremath{\enumO(#1)}} + + + +\newcommand{\PRE}[1]{\ensuremath{\langle #1 \rangle}} +\newcommand{\PREB}[1]{\ensuremath{[ #1 ]}} +\newcommand{\Pre}[2]{\ensuremath{\textit{Pre}_{#1}(#2)}} +\newcommand{\pretilde}[0]{\ensuremath{\widetilde{\textit{pre}}}} +\newcommand{\post}[0]{\ensuremath{\textit{post}}} +\newcommand{\pretildeR}[0]{\ensuremath{\widetilde{\textrm{pre}}}} +\newcommand{\postR}[0]{\ensuremath{\textrm{post}}} +\newcommand{\Succ}[0]{\ensuremath{\textit{successeur}}} +\newcommand{\Men}[0]{\ensuremath{\textit{meneur}}} +\newcommand{\Gpre}[2]{\ensuremath{G_{#1}(#2)}} +\newcommand{\Fpre}[2]{\ensuremath{F_{#1}(#2)}} +\newcommand{\POST}[1]{\ensuremath{[ #1 ]^{o}}} +\newcommand{\sem}[1]{\ensuremath{\textit{rel}_{#1}}} +\newcommand{\quantToSubst}[0]{\ensuremath{\textit{q2s}}} + + +\newcommand{\wpr}[0]{\ensuremath{\textit{wp}}\xspace} +\newcommand{\wlp}[0]{\ensuremath{\textit{wlp}}\xspace} +\newcommand{\weaklp}[2]{\ensuremath{\textit{wlp}_{#1}(#2)}\xspace} +\newcommand{\weakp}[2]{\ensuremath{\textit{wp}_{#1}(#2)}\xspace} +\newcommand{\prd}[2]{\ensuremath{\textit{prd}_{#1}({#2})}\xspace} + +%\newcommand{\true}[0]{\ensuremath{\textit{true}}} +%%%%%%%%%%%%%%%%% inclusion de fichiers MCh +\newcommand{\myInput}[1]{\begin{center}\begin{tabular}{l}\input{#1}\end{tabular}\end{center}} + + +%%%%%%%%%%%%% algorithmes d'atteignabilité +\newcommand{\Init}[0]{\ensuremath{\textit{Init}}\xspace} +\newcommand{\Target}[0]{\ensuremath{\textit{Target}}\xspace} + + +%%%%%%%%%%%%%%%% grammaire abstraite b +\newcommand{\substs}[0]{\ensuremath{\textit{Substs}}} +\newcommand{\choice}[0]{\ensuremath{[]}} +\newcommand{\paral}[0]{\ensuremath{\mid\mid}} +\newcommand{\card}[1]{\ensuremath{\textit{card}(#1)}} +%\newcommand{\dom}[0]{\ensuremath{\textit{dom}}} + + +%%%%%%%%%%%%%%%%%%%% A remplacer +\newcommand{\fs}[1]{\ensuremath{\mathsf{#1}}} +\newcommand{\sort}[1]{\mbox{\textsc{#1}}} +\newcommand{\dropE}[0]{\ensuremath{\mathsf{dropExistential}}} +\newcommand{\renameF}[0]{\ensuremath{\mathsf{renameFormula}}} +\newcommand{\ppnf}[0]{\ensuremath{\mathsf{de}}} +\newcommand{\apnx}[0]{\ensuremath{\mathsf{mini}}} +\newcommand{\apnxq}[0]{\ensuremath{\mathsf{m}_q}} +\newcommand{\sqs}[0]{\ensuremath{\mathsf{rf}}} +\newcommand{\theoryT}[0]{\ensuremath{{\cal T}}} +\newcommand{\theoryU}[0]{\ensuremath{{\cal T}}} +\newcommand{\vars}[0]{\ensuremath{\mathcal{V}}} +%\newcommand{\Vlib}{\mathcal V} + +%%%%%%%%%%%%%%%%% Abstraction +\newcommand{\latice}[0]{\ensuremath{\textit{exp}^{A}}} +\newcommand{\laticeB}[0]{\ensuremath{\latice(B_1,\ldots,B_l)}} +\newcommand{\concretisation}[0]{\ensuremath{\gamma}} +\newcommand{\abstraction}[0]{\ensuremath{\alpha}} + + +%%%%%%%% SFUNC -> BAES +%\newcommand{\dres}[0]{\mathbin{AMSa}{"43}} +%\newcommand{\bdres}[0]{\mathrel{\ooalign{$\dres$\hfil\cr$\mkern5mu$\hbox{$-$}}}} +\newcommand{\sfunc}[0]{\ensuremath{\textit{SFUNC}}} +\newcommand{\override}[2]{\ensuremath{#1 \bdres #2 }} +\newcommand{\Partition}[1]{\ensuremath{\mathbbm{P}}(#1)} +\newcommand{\fc}[1]{\ensuremath{\widetilde{#1}}} %fresh constant +\newcommand{\nul}[0]{\ensuremath{\mathsf{null}}} %fresh constant +\newcommand{\overR}[3]{\ensuremath {\mathsf{over}(#1,#2,#3)}} +\newcommand{\image}[2]{\ensuremath {\sf{image}(#1,#2)}} + + +%\input{bmacro} + +%%%%%%%%%%%%%%%%%%%%%%%%%% sortes à supprimer +\newcommand{\ind}[0]{\textit{index}} +\newcommand{\val}[0]{\textit{val}} +%\newcommand{\func}[0]{\ensuremath{\textit{F}\xspace}} +\newcommand{\arr}[0]{\textit{array}} +%\newcommand{\other}[0]{\ensuremath{\textit{other}\xspace}} +\newcommand{\iSet}[0]{\ensuremath{\textit{S}_{i}}\xspace} +\newcommand{\eSet}[0]{\ensuremath{\textit{S}_{e}}\xspace} +\newcommand{\ARR}[0]{\textit{ARRAY}\xspace} +\newcommand{\IND}[0]{\textit{INDEX}\xspace} +\newcommand{\VAL}[0]{\textit{VALUE}\xspace} +\newcommand{\constArr}{\ensuremath{\mathsf{const}}\xspace} +%\newcommand{\block}{\ensuremath{\mathsf{block}}\xspace} +\newcommand{\im}[0]{\ensuremath{\mathsf{im}}} + + +%%%%%%%%%%%%%%%%%%%%%%%%%% multi-sorted languages +\newcommand{\eJ}{\EuScript J} +\newcommand{\eF}{\EuScript F} +\newcommand{\eL}{\EuScript L} +\newcommand{\eT}{\EuScript T} +\newcommand{\eV}{\EuScript V} +\newcommand{\eP}{\EuScript P} +%\newcommand{\eC}{\EuScript C} +%\newcommand{\eR}{\EuScript R} +%\newcommand{\eI}{\EuScript I} +\renewcommand{\le}{\leqslant} +\renewcommand{\ge}{\geqslant} + +\newcommand{\any}[0]{\textrm{@}} + +\newcommand{\str}[0]{\textit{Strength}} + + +%%%%%%%%%%%%%%%%%%%%%%%% +\newcommand{\sortSet}{\mathcal{S}} +\newcommand{\sortVars}{\mathcal{X}_s} +\newcommand{\sortFunctionSet}{\mathcal{F}_s} +\newcommand{\varSet}{\mathcal{X}} +\newcommand{\functionSet}{\mathcal{F}} + +\def\unique{\sort{u}}