$$ \def\por{\ \ | \ \ } \def\dom{\textsf{dom}} \def\tsf#1{\textsf{#1}} \def\unifyj#1#2#3{#1 \sim #2 \Downarrow #3} \def\dict#1#2{\textsf{Dict}\left( #1, #2 \right)} \def\pf{\hookrightarrow}%\rightharpoonup \def\tone{{t_1}} \def\ttwo{{t_2}} \def\rule#1#2#3{\dfrac{#3}{#2}\ {#1}} \def\eqdef{\overset{\textsf{def}}{=}} \def\freevars{\textsf{free}} $$ Unification is probably one of the most important concepts in computer science. If you are not aware, unification is basically the process you undergo to find out how two syntactic objects like $a+b$ and $a+2c$ can be the same thing. In this case, you replace $b$ with $2c$.

$$\def\mathblue#1{\colorbox{blue}{$#1$}} \def\mathgreen#1{\colorbox{green}{$#1$}} \def\mathred#1{\colorbox{red}{$#1$}} \def\mathhl#1{\colorbox{Orchid}{$#1$}} \def\lequiv{\fallingdotseq}$$ $\def\lequiv{\fallingdotseq}$ What mathematics describes is a long standing issue in philosophy. It is hard to break into this subject, but I hope that my intent can be shared. Since I am a mathemtics student who is interested in formal systems, I can’t help to feel nervous when my professor says $A$ is a subset of $B$ if for all $x$, $x\in B$ whenever $x \in A$,

$$\def\infer#1#2{\dfrac{#2}{#1}}$$ Rule systems are seen in almost every programming languages paper. They are a tool for conveying very precise notions of computation. In general, is not easy to give a succinct definition of a rule system, but one can be described easily by adopting a specific representation. A rule system consists of a set of statements of the form $$\infer{Q}{P_1 \quad \ldots \quad P_n}$$ where $Q,P_i$ are propositional schemata. Here, $Q$ is called the conclusion and $P_i$ are called the premises.