Author name is 3em dash when using bibtex file to output bibliography in Latex

Problems

Entry in .bib file (edit by Jabref)

@INBOOK{Baier2008a,
  chapter = {4},
  pages = {170-198},
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}

The output will be like that:

[22] ——, Principles of model checking. MIT Press, 2008, ch. 4, pp. 170–198.

Try
If I remove the hyphen which is used to connect the name, it will be alright.

@INBOOK{Baier2008a,
  chapter = {4},
  pages = {170-198},
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}

The output will be like that:

[22] C. Baier and J. P. Katoen, Principles of model checking. MIT Press, 2008,
ch. 4, pp. 170–198.

However, the similar entry 

@BOOK{Baier2008,
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  pages = {I-XVII, 1-975},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}

will give the right output

[21] C. Baier and J.-P. Katoen, Principles of model checking. MIT Press, 2008.

Root Cause
If two entries in .bib file have the same author name, then one of them will become 3em dash (——).
It's default behaviour defined in IEEEtran.bst style. 


To remove this limitation, change the CTLdash_repeated_names value to no in .bib file

@IEEEtranBSTCTL{IEEEexample:BSTcontrol,
  CTLdash_repeated_names = "no"
}

Then add the following line in the tex file

\bstctlcite{IEEEexample:BSTcontrol}

However,  if the documentclass is not IEEEtrans, then this command \bstctlcite is not available. So this try will failed too.

Solution:
For the Latex file which has documentclass IEEEtrans, the above solution may be applied. For others (Article and Book class), just leave (——), it's not an error

"LaTeX Error: Too many math alphabets used in version czt"

This error means you have used more than 16 math symbol fonts (latex limitation).

Solution 1:  (http://valis.cs.uiuc.edu/blog/?cat=37)
Bypass this limit by specifying the only used font, e.g.

$\text{\usefont{U}{bbm}{m}{n}{H}}$ 

 Solution 2: (Work for this case)
 Replace the txfonts package with mathtools
Or remove the txfonts package if you don't need it

%\usepackage{txfonts} %\varparallel
 \usepackage{mathtools}

Solution 3:
too many math alphabets in version normal

\usepackage{amssymb}

\newcommand\hmmax{0} % default 3
 % \newcommand\bmmax{0} % default 4
 \usepackage{bm}

Substitution, Unification and Term Rewriting

Unification is the basis of term rewriting system, and unification algorithms is the heart of the computation model of logic programs.

Term:

terms are expressions which can be obtained from constant symbols, variables and function symbols. Constant symbols are the 0-ary functions, so no special syntactic class is needed for them.

• Function symbols: one that has no other property than its name and arity
• Terms that do not contain free variables are known as ground terms
• A ground term of a formal system is a term that does not contain any free variables;
• free variable: y is free variable in \( \forall x \in X \bullet (x+y) > 0 \)
• bound variable: x is bound variable in \( \forall x \in X \bullet (x+y) > 0 \)
• Hence \( \forall x \in X \bullet (x+y) > 0 \) is not a ground term, but \( \forall x \in X \bullet x > 0 \) is a ground term
• x and y are variables, and f is a binary function symbol, then \( f(x,y) \) is a term

Arity - the number of arguments or operands the functions or operation accepts. For example, the arity of \( f(x)=x+1 \) is 1; the arity of \( f = 3 \) is 0; the arity of \( f(x,y,z) = x + y + z \) is 3.

• 0-ary function or operation: (arity == 0) constant symbols
• unary function or operation: (arity == 1) such as \( f(x) = x * 2 \), (unary operator) \( -x \)
• binary function or operation: (arity == 2) such as \( f(x,y) = x + y \)
• ternary function or operation: (arity == 3)

Signature:

A signature \( \Sigma \) is a set of function symbols, where each \( f \in \Sigma \) is associated with a non-negative integer n, the arity of \( f \). \( \Sigma^{0} \) denotes a set of constant symbols, while \( \Sigma^{n} \) denotes a set of n-ary function symbols.

• For example, group \( \Sigma_G := \{e, i, f \} \) where e is 0-ary, i is 1-ary, and f is 2-ary
• For example, a set of non-negative integers. e for smallest non-negative integer, i denotes the successor function \( succ(x) = x + 1 \), and f denotes the addition function \( f(x,y) = x + y \)

Substitution:

Substitution is a syntactic transformation on strings of symbols of a formal language

• a substitution is a finite set of the form $$ \theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$, where 
• \(v_i\): distinct variables; 
• \( t_i \): terms with \(t_i \ne v_i\);
• \( v_i \mapsto t_i \): binding

• Substitution application:  \( E \theta \)
• E - expression
• \(\theta\) - substitution
• Simultaneously replacing each occurrence of \(v_i\) in E with \(t_i\)
• For example, \(E = p(x,y,f(a))\), \(\theta = \{x \mapsto b, y \mapsto x\}\), \(E \theta = p(b,x,f(a))\).
  

• Substitution Composition
• Two substitutions:  $$ \theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$ $$ \sigma =  \{u_1 \mapsto s_1, ..., u_n \mapsto s_n \}$$ $$\theta \sigma =  \{v_1 \mapsto t_1 \sigma, ..., v_n \mapsto t_n \sigma,  u_1 \mapsto s_1, ..., u_n \mapsto s_n\}$$
• For example, \( \theta = \{x \mapsto f(y), y \mapsto z\} \), \( \sigma = \{x \mapsto a, y \mapsto b, z \mapsto y\}\), \( \theta \sigma = \{x \mapsto f(b), z \mapsto y\} \)

• Empty Substitution \( \varepsilon \)
• Renaming substitution
• \( \theta =  \{x_1 \mapsto y_1, ..., x_n \mapsto y_n \} \) is a renaming substitution if \(y_i \) are distinct variables

• More general substitution (MGS)
• a substitution \(\theta\) is more general than a substitution \( \sigma \), written \(\theta \leq \sigma \), iff there exists a substitution \(\lambda\) that $$ \theta \lambda = \sigma $$

Abstract Reduction System:

• An abstract reduction system is a pair \( (A, \to) \), where the reduction \( \to \) is a binary relation on the set A, i.e. \( \to \subseteq A \times A \). Written \(a \to b \), instead of \( (a,b) \in \to \)
• Program evaluation: \(a0 \to a1 \to ... \). Starting from the initial program a0, and try to reach a normal formal
• Normal formal is the program which can not be reducible
• Let \(\Sigma\) be a signature and \(V\) a countably infinite set of variables disjoint from \(\Sigma\). A \(\Sigma\)-identity is a pair \((s,t) \in T(\Sigma, V) \times T(\Sigma, V)\). Identities will be written as \(s \approx t\)
• reduction relation \( \to_E \), where E is a set of \(\Sigma\)-identity
  

Unification:

Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal. Unification is widely used in automated reasoning, logic programming and programming language type system implementation

• Unification is the process of solving the satisfiability problem: given \(E\), \(s\) and \(t\), find a substitution \(\theta\) such that \(\theta s \approx_E \theta t\)
• For special case, where \(E=\emptyset \), this case of unification is called syntactic unification, because the unification aims to find a \(\theta\) such that \(\theta s = \theta t\) i.e. \(\theta s\) and \( \theta t\) are syntactically identical.
• If \(E \neq \emptyset \), this is referred to semantic unification
• Unifier of Expressions: a substitution \(\theta\) is a unifier of expressions E and F iff $$\theta E = \theta F$$
• For example, \(E = f(x,b,g(z)), F = f(f(y),y,g(u))\). Then \( \theta = \{x \mapsto f(b), y \mapsto b, z \mapsto u\}\) is a unifier of E and F since $$\theta E = f(f(b),b,g(u))$$ $$\theta F = f(f(b),b,g(u))$$

• Unifier is a solution to the equation by substitution. Find a substitution to make two expressions E and F are equal and this substitution is a solution to this equation, named unifier.

Unification in Prolog:

Unification in Perl: