diff --git a/src/format.rs b/src/format.rs
index a4495bd..a201c44 100644
--- a/src/format.rs
+++ b/src/format.rs
@@ -1,2 +1,21 @@
 mod formulas;
 mod terms;
+
+pub trait Format
+{
+	fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter,
+		variable_declaration: &std::rc::Rc<crate::VariableDeclaration>)
+		-> std::fmt::Result;
+}
+
+pub struct DefaultFormat;
+
+impl Format for DefaultFormat
+{
+	fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter,
+		variable_declaration: &std::rc::Rc<crate::VariableDeclaration>)
+		-> std::fmt::Result
+	{
+		write!(formatter, "{:?}", variable_declaration)
+	}
+}
diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 4651be3..47bfc0f 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -35,14 +35,19 @@ enum FormulaPosition
 	ImpliesAntecedent,
 }
 
-struct FormulaDisplay<'formula>
+struct FormulaDisplay<'formula, 'format, F>
+where
+	F: super::Format,
 {
 	formula: &'formula crate::Formula,
 	parent_formula: Option<&'formula crate::Formula>,
 	position: FormulaPosition,
+	format: &'format F,
 }
 
-impl<'formula> FormulaDisplay<'formula>
+impl<'formula, 'format, F> FormulaDisplay<'formula, 'format, F>
+where
+	F: super::Format,
 {
 	fn requires_parentheses(&self) -> bool
 	{
@@ -112,19 +117,24 @@ impl<'formula> FormulaDisplay<'formula>
 	}
 }
 
-fn display_formula<'formula>(formula: &'formula crate::Formula,
-	parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition)
-	-> FormulaDisplay<'formula>
+fn display_formula<'formula, 'format, F>(formula: &'formula crate::Formula,
+	parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition, format: &'format F)
+	-> FormulaDisplay<'formula, 'format, F>
+where
+	F: super::Format,
 {
 	FormulaDisplay
 	{
 		formula,
 		parent_formula,
 		position,
+		format,
 	}
 }
 
-impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
+impl<'formula, 'format, F> std::fmt::Debug for FormulaDisplay<'formula, 'format, F>
+where
+	F: super::Format,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -142,7 +152,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				if exists.parameters.is_empty()
 				{
 					write!(formatter, "{:?}", display_formula(&exists.argument, self.parent_formula,
-						self.position))?;
+						self.position, self.format))?;
 				}
 				else
 				{
@@ -152,13 +162,14 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 					for parameter in exists.parameters.iter()
 					{
-						write!(formatter, "{}{:?}", separator, parameter)?;
+						write!(formatter, "{}", separator)?;
+						self.format.display_variable_declaration(formatter, &parameter)?;
 
 						separator = ", "
 					}
 
 					write!(formatter, " {:?}", display_formula(&exists.argument, Some(self.formula),
-						FormulaPosition::Any))?;
+						FormulaPosition::Any, self.format))?;
 				}
 			},
 			crate::Formula::ForAll(for_all) =>
@@ -166,7 +177,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				if for_all.parameters.is_empty()
 				{
 					write!(formatter, "{:?}", display_formula(&for_all.argument,
-						self.parent_formula, self.position))?;
+						self.parent_formula, self.position, self.format))?;
 				}
 				else
 				{
@@ -176,17 +187,18 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 					for parameter in for_all.parameters.iter()
 					{
-						write!(formatter, "{}{:?}", separator, parameter)?;
+						write!(formatter, "{}", separator)?;
+						self.format.display_variable_declaration(formatter, &parameter)?;
 
 						separator = ", "
 					}
 
 					write!(formatter, " {:?}", display_formula(&for_all.argument,
-						Some(self.formula), FormulaPosition::Any))?;
+						Some(self.formula), FormulaPosition::Any, self.format))?;
 				}
 			},
 			crate::Formula::Not(argument) => write!(formatter, "not {:?}",
-				display_formula(argument, Some(self.formula), FormulaPosition::Any))?,
+				display_formula(argument, Some(self.formula), FormulaPosition::Any, self.format))?,
 			crate::Formula::And(arguments) =>
 			{
 				if arguments.is_empty()
@@ -206,7 +218,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					for argument in arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_formula(argument, parent_formula, position))?;
+							display_formula(argument, parent_formula, position, self.format))?;
 
 						separator = " and "
 					}
@@ -231,7 +243,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					for argument in arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_formula(argument, parent_formula, position))?;
+							display_formula(argument, parent_formula, position, self.format))?;
 
 						separator = " or "
 					}
@@ -243,13 +255,14 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				{
 					write!(formatter, "{:?}",
 						display_formula(antecedent, Some(self.formula),
-							FormulaPosition::ImpliesAntecedent))
+							FormulaPosition::ImpliesAntecedent, self.format))
 				};
 
 				let format_implication = |formatter: &mut std::fmt::Formatter| -> Result<_, _>
 				{
 					write!(formatter, "{:?}",
-						display_formula(implication, Some(self.formula), FormulaPosition::Any))
+						display_formula(implication, Some(self.formula), FormulaPosition::Any,
+							self.format))
 				};
 
 				match direction
@@ -287,7 +300,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					for argument in arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_formula(argument, parent_formula, position))?;
+							display_formula(argument, parent_formula, position, self.format))?;
 
 						separator = " <-> "
 					}
@@ -306,9 +319,9 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				};
 
 				write!(formatter, "{:?} {} {:?}",
-					display_term(&compare.left, None, TermPosition::Any),
+					display_term(&compare.left, None, TermPosition::Any, self.format),
 					operator_string,
-					display_term(&compare.right, None, TermPosition::Any))?;
+					display_term(&compare.right, None, TermPosition::Any, self.format))?;
 			},
 			crate::Formula::Boolean(true) => write!(formatter, "true")?,
 			crate::Formula::Boolean(false) => write!(formatter, "false")?,
@@ -325,7 +338,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					for argument in &predicate.arguments
 					{
 						write!(formatter, "{}{:?}", separator, display_term(argument, None,
-							TermPosition::Any))?;
+							TermPosition::Any, self.format))?;
 
 						separator = ", "
 					}
@@ -344,7 +357,9 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 	}
 }
 
-impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
+impl<'formula, 'format, F> std::fmt::Display for FormulaDisplay<'formula, 'format, F>
+where
+	F: super::Format,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -356,7 +371,8 @@ impl std::fmt::Debug for crate::Formula
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any))
+		write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any,
+			&super::DefaultFormat))
 	}
 }
 
@@ -364,7 +380,8 @@ impl std::fmt::Display for crate::Formula
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any))
+		write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any,
+			&super::DefaultFormat))
 	}
 }
 
diff --git a/src/format/terms.rs b/src/format/terms.rs
index 66d9b04..b302d48 100644
--- a/src/format/terms.rs
+++ b/src/format/terms.rs
@@ -58,14 +58,19 @@ pub(crate) enum TermPosition
 	Right,
 }
 
-pub(crate) struct TermDisplay<'term>
+pub(crate) struct TermDisplay<'term, 'format, F>
+where
+	F: super::Format,
 {
 	term: &'term crate::Term,
 	parent_term: Option<&'term crate::Term>,
 	position: TermPosition,
+	format: &'format F,
 }
 
-impl<'term> TermDisplay<'term>
+impl<'term, 'format, F> TermDisplay<'term, 'format, F>
+where
+	F: super::Format,
 {
 	fn requires_parentheses(&self) -> bool
 	{
@@ -149,19 +154,24 @@ impl<'term> TermDisplay<'term>
 	}
 }
 
-pub(crate) fn display_term<'term>(term: &'term crate::Term, parent_term: Option<&'term crate::Term>,
-	position: TermPosition)
-	-> TermDisplay<'term>
+pub(crate) fn display_term<'term, 'format, F>(term: &'term crate::Term,
+	parent_term: Option<&'term crate::Term>, position: TermPosition, format: &'format F)
+	-> TermDisplay<'term, 'format, F>
+where
+	F: super::Format,
 {
 	TermDisplay
 	{
 		term,
 		parent_term,
 		position,
+		format,
 	}
 }
 
-impl<'term> std::fmt::Debug for TermDisplay<'term>
+impl<'term, 'format, F> std::fmt::Debug for TermDisplay<'term, 'format, F>
+where
+	F: super::Format,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -180,7 +190,8 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 			crate::Term::Integer(value) => write!(formatter, "{}", value)?,
 			crate::Term::String(value) => write!(formatter, "\"{}\"",
 				value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?,
-			crate::Term::Variable(variable) => write!(formatter, "{:?}", variable.declaration)?,
+			crate::Term::Variable(variable) =>
+				self.format.display_variable_declaration(formatter, &variable.declaration)?,
 			crate::Term::Function(function) =>
 			{
 				write!(formatter, "{}", function.declaration.name)?;
@@ -198,7 +209,8 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 					for argument in &function.arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_term(&argument, Some(self.term), TermPosition::Any))?;
+							display_term(&argument, Some(self.term), TermPosition::Any,
+								self.format))?;
 
 						separator = ", ";
 					}
@@ -219,18 +231,20 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 				};
 
 				write!(formatter, "{:?} {} {:?}",
-					display_term(&binary_operation.left, Some(self.term), TermPosition::Left),
+					display_term(&binary_operation.left, Some(self.term), TermPosition::Left,
+						self.format),
 					operator_string,
-					display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?;
+					display_term(&binary_operation.right, Some(self.term), TermPosition::Right,
+						self.format))?;
 			},
 			crate::Term::UnaryOperation(
 				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
 				=> write!(formatter, "-{:?}",
-					display_term(argument, Some(self.term), TermPosition::Any))?,
+					display_term(argument, Some(self.term), TermPosition::Any, self.format))?,
 			crate::Term::UnaryOperation(
 				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
 				=> write!(formatter, "|{:?}|",
-					display_term(argument, Some(self.term), TermPosition::Any))?,
+					display_term(argument, Some(self.term), TermPosition::Any, self.format))?,
 		}
 
 		if requires_parentheses
@@ -242,7 +256,9 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 	}
 }
 
-impl<'term> std::fmt::Display for TermDisplay<'term>
+impl<'term, 'format, F> std::fmt::Display for TermDisplay<'term, 'format, F>
+where
+	F: super::Format,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -254,7 +270,8 @@ impl std::fmt::Debug for crate::Term
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any))
+		write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any,
+			&super::DefaultFormat))
 	}
 }
 
@@ -262,7 +279,7 @@ impl std::fmt::Display for crate::Term
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{}", display_term(&self, None, TermPosition::Any))
+		write!(formatter, "{}", display_term(&self, None, TermPosition::Any, &super::DefaultFormat))
 	}
 }