\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{graphicx}
\usepackage{float}
\usepackage{verbatim}
\usepackage{enumerate}
\usepackage{mathtools}
\usepackage{accents}
\usepackage{bm}% boldmath

\usepackage[acronym,hyperfirst=false]{glossaries}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}{Proposition}[section]
\newtheorem{example}{Example}
\newtheorem{lemma}{Lemma}[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}{Definition}[section]
\newtheorem{remark}{Remark}

\newcommand{\Definition}[1]{Definition~\ref{#1}}
\newcommand{\Section}[1]{Section~\ref{#1}}
\newcommand{\Chapter}[1]{Chapter~\ref{#1}}
\newcommand{\Theorem}[1]{Theorem~\ref{#1}}
\newcommand{\Proposition}[1]{Proposition~\ref{#1}}
\newcommand{\Example}[1]{Example~\ref{#1}}
\newcommand{\Lemma}[1]{Lemma~\ref{#1}}
\newcommand{\Figure}[1]{Figure~\ref{#1}}
\newcommand{\Corollary}[1]{Corollary~\ref{  #1}}
\newcommand{\Remark}[1]{Remark~\ref{#1}}
\newcommand{\Algorithm}[1]{Algorithm~\ref{#1}}
\newcommand{\Line}[1]{line~\ref{#1}}

\renewcommand{\P}{\mathcal{P}}
\newcommand{\Not}{\textrm{\bf not\,}}
\newcommand{\head}{head}
\newcommand{\intersect}{\cap}
\newcommand{\union}{\cup}
\newcommand{\atoms}{Atoms}
\newcommand{\bodyp}{body^{+}}
\newcommand{\bodyn}{body^{-}}
\newcommand{\body}{body}
\newcommand{\op}[1]{\textbf{#1}}
\newcommand{\pmodels}{\models}

\newcommand{\KB}{\mathcal{K}}
\newcommand{\bfK}{\textit{\em \textbf{K}}}
\renewcommand{\O}{\mathcal{O}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\KAK}{\textbf{KA}(\KB)}
\newcommand{\Katom}{\textbf{K}-atom~}
\newcommand{\Katoms}{\textbf{K}-atoms~}
\newcommand{\comp}[1]{\overline{#1}}

\newcommand{\A}{\textbf{A}}
\newcommand{\T}{\textbf{T}}
\newcommand{\F}{\textbf{F}}

\newcommand{\boldK}{\bf {K}}
\newcommand{\PP}{\mathcal{x}_{\KBB}}
\newcommand{\M}{\mathcal{M}}
\newcommand{\Ma}{M_0}
\newcommand{\Mb}{M_1}
\newcommand{\MM}{\langle M, M_1 \rangle}
\newcommand{\N}{\mathcal{N}}
\newcommand{\Na}{N_0}
\newcommand{\Nb}{N_1}
\newcommand{\NN}{\langle N, N_1 \rangle}
\newcommand{\MN}{\langle M, N \rangle}
\newcommand{\ff}{{\bf f}}
\newcommand{\uu}{{\bf u}}
\renewcommand{\tt}{{\bf t}}
\newcommand{\mneval}[1]{(I, \MN, \MN)( #1  )}
\newcommand{\meval}[1]{\mneval{#1}}
\newcommand{\mmeval}[1]{\mneval{#1}}
\newcommand{\KBA}{\textsf{KA}}
\newcommand{\OO}{\mathcal{O}}
\newcommand{\OBO}[1]{{{\sf OB}_{\OO,#1}}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\Q}{\mathcal{Q}}
\newcommand{\Pcomp}{\P_{\textrm{\tiny COMP}}}
\newcommand{\Ploop}{\P_{\textrm{\tiny LOOP}}}
\newcommand{\Atoms}{Atoms}
\newcommand{\Loops}{Loops}
\renewcommand{\implies}{\supset}
\renewcommand{\impliedby}{\subset}
\newcommand{\Rule}{rule}
\newcommand{\eval}[2]{#1\big\{#2\big\}}
\newcommand{\lub}[1]{{\bf lub_{#1}~}}
\newcommand{\glb}[1]{{\bf glb_{#1}~}}
\newcommand{\lfp}{{\bf lfp}}
\newcommand{\fix}[1]{{\bf broken} ~{#1}}
\newcommand{\fixpoints}{\textbf{fixpoints}}

% https://tex.stackexchange.com/questions/118240/how-to-draw-a-border-around-character-in-a-formula
\makeatletter
\renewcommand{\boxed}[1]{\text{\fboxsep=.2em\fbox{\m@th$\displaystyle#1$}}}
\makeatother
\newcommand{\boxedt}[1]{\boxed{\textrm{#1}}}

\newcommand{\argblank}{\underline{\hspace{.3cm}}}
\renewcommand{\L}{\mathcal{L}}
\newcommand{\squnion}{\sqcup}
\renewcommand{\implies}{\Rightarrow}
\newcommand{\define}{\coloneqq}
\newcommand{\lcomp}[1]{{#1}^{\mathbf{\hspace{.075em}c}}}

\newcommand{\noncompare}{\bowtie}
% https://tex.stackexchange.com/questions/378087
\makeatletter
\newcommand\ineq{}% for safety
\DeclareRobustCommand{\ineq}{\mathrel{\mathpalette\rance@ineq\relax}}
\newcommand{\rance@ineq}[2]{%
  \vcenter{\hbox{%
    $\m@th#1\mkern1.5mu\underline{\mkern-1.5mu\bowtie\mkern-1.5mu}\mkern1.5mu$%
  }}%
}
\makeatother
\newcommand{\noncompareeq}{\ineq}




\newcommand{\omax}{\textbf{max}}
\newcommand{\omin}{\textbf{min}}

\newcommand{\project}[2]{\Pi_{#1}(#2)}

\newcommand{\mknfmodels}{\models_{\mbox{\tiny{\sf MKNF}}}}