glossary.tex

\usepackage{glossaries}

\newacronym{atp}{ATP}{automated theorem prover}
\newacronym{fol}{FOL}{first order logic}
\newacronym{kbo}{KBO}{Knuth-Bendix Ordering}
\newacronym{lpo}{LPO}{Lexicographic Path Ordering}
\newacronym{cnf}{CNF}{clausal normal form}

\newglossaryentry{problem}
{
	name=problem,
	description={a collection of zero or more premises and one or more conjectures}
}

\newglossaryentry{precedence}
{
	name=precedence,
	description={a total order on symbols in a given \gls{problem}}
}

\newglossaryentry{pairwise-preference-function}
{
	name=pairwise preference function,
	description={a function that assigns a preference value to each pair of symbols in a given problem}
}

\newglossaryentry{preference-value}
{
	name=preference value,
	description={a real number that expresses the expected contribution of a symbol being ordered before another symbol}
}

\newglossaryentry{preference-matrix}
{
	name=preference matrix,
	description={a square matrix populated with \glspl{preference-value} of all the pairs of symbols in a given \gls{problem}}
}

\newglossaryentry{order-matrix}
{
	name=order matrix,
	description={a binary square matrix with value 1 for each pair of elements \(a, b\) ordered \(a < b\) according to a given order}
}

\newglossaryentry{vampire}
{
	name=Vampire,
	description={a saturation-based \gls{atp} \cite{Kovacs2013}}
}

\newglossaryentry{abstract-solving-time}
{
	name=abstract solving time,
	description={the number of iterations of the saturation algorithm}
}