diff --git a/src/flavor.rs b/src/flavor.rs
index a619c3c..8088dac 100644
--- a/src/flavor.rs
+++ b/src/flavor.rs
@@ -2,8 +2,9 @@ pub trait FunctionDeclaration
 {
 	fn new(name: String, arity: usize) -> Self;
 
-	fn name(&self) -> &str;
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
 	fn arity(&self) -> usize;
+	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
 }
 
 impl FunctionDeclaration for crate::FunctionDeclaration
@@ -17,23 +18,29 @@ impl FunctionDeclaration for crate::FunctionDeclaration
 		}
 	}
 
-	fn name(&self) -> &str
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		&self.name
+		write!(formatter, "{}", self.name)
 	}
 
 	fn arity(&self) -> usize
 	{
 		self.arity
 	}
+
+	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
+	{
+		self.name == other_name && self.arity == other_arity
+	}
 }
 
 pub trait PredicateDeclaration
 {
 	fn new(name: String, arity: usize) -> Self;
 
-	fn name(&self) -> &str;
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
 	fn arity(&self) -> usize;
+	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
 }
 
 impl PredicateDeclaration for crate::PredicateDeclaration
@@ -47,22 +54,28 @@ impl PredicateDeclaration for crate::PredicateDeclaration
 		}
 	}
 
-	fn name(&self) -> &str
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		&self.name
+		write!(formatter, "{}", self.name)
 	}
 
 	fn arity(&self) -> usize
 	{
 		self.arity
 	}
+
+	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
+	{
+		self.name == other_name && self.arity == other_arity
+	}
 }
 
 pub trait VariableDeclaration
 {
 	fn new(name: String) -> Self;
 
-	fn name(&self) -> &str;
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
+	fn matches_name(&self, other_name: &str) -> bool;
 }
 
 impl VariableDeclaration for crate::VariableDeclaration
@@ -75,9 +88,14 @@ impl VariableDeclaration for crate::VariableDeclaration
 		}
 	}
 
-	fn name(&self) -> &str
+	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		&self.name
+		write!(formatter, "{}", self.name)
+	}
+
+	fn matches_name(&self, other_name: &str) -> bool
+	{
+		self.name == other_name
 	}
 }
 
@@ -86,8 +104,7 @@ pub trait Flavor
 	type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
 	type PredicateDeclaration:
 		PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
-	type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash
-		+ std::fmt::Display;
+	type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
 }
 
 pub struct DefaultFlavor;
diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index e436d7c..d6ad042 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -1,4 +1,4 @@
-use crate::flavor::PredicateDeclaration as _;
+use crate::flavor::{PredicateDeclaration as _, VariableDeclaration as _};
 use super::terms::*;
 
 impl std::fmt::Debug for crate::ComparisonOperator
@@ -180,7 +180,8 @@ where
 
 					for parameter in exists.parameters.iter()
 					{
-						write!(formatter, "{}{}", separator, parameter)?;
+						write!(formatter, "{}", separator)?;
+						parameter.display_name(formatter)?;
 
 						separator = ", "
 					}
@@ -204,7 +205,8 @@ where
 
 					for parameter in for_all.parameters.iter()
 					{
-						write!(formatter, "{}{}", separator, parameter)?;
+						write!(formatter, "{}", separator)?;
+						parameter.display_name(formatter)?;
 
 						separator = ", "
 					}
@@ -341,7 +343,7 @@ where
 			crate::Formula::Boolean(false) => write!(formatter, "false")?,
 			crate::Formula::Predicate(predicate) =>
 			{
-				write!(formatter, "{}", predicate.declaration.name())?;
+				predicate.declaration.display_name(formatter)?;
 
 				if !predicate.arguments.is_empty()
 				{
diff --git a/src/format/terms.rs b/src/format/terms.rs
index db28842..17330a1 100644
--- a/src/format/terms.rs
+++ b/src/format/terms.rs
@@ -1,4 +1,4 @@
-use crate::flavor::FunctionDeclaration as _;
+use crate::flavor::{FunctionDeclaration as _, VariableDeclaration as _};
 
 impl std::fmt::Debug for crate::SpecialInteger
 {
@@ -190,10 +190,10 @@ where
 			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) => variable.declaration.display_name(formatter)?,
 			crate::Term::Function(function) =>
 			{
-				write!(formatter, "{}", function.declaration.name())?;
+				function.declaration.display_name(formatter)?;
 
 				assert!(function.declaration.arity() == function.arguments.len(),
 					"number of function arguments differs from declaration (expected {}, got {})",
diff --git a/src/utils.rs b/src/utils.rs
index a57c1a2..10297c8 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -70,7 +70,7 @@ where
 			VariableDeclarationStackLayer::Free(free_variable_declarations) =>
 			{
 				if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
-					.find(|x| x.name() == variable_name)
+					.find(|x| x.matches_name(variable_name))
 				{
 					return Some(std::rc::Rc::clone(&variable_declaration));
 				}
@@ -81,7 +81,7 @@ where
 			{
 				if let Some(variable_declaration) = bound_variable_declarations
 					.variable_declarations.iter()
-					.find(|x| x.name() == variable_name)
+					.find(|x| x.matches_name(variable_name))
 				{
 					return Some(std::rc::Rc::clone(&variable_declaration));
 				}
@@ -98,7 +98,7 @@ where
 			VariableDeclarationStackLayer::Free(free_variable_declarations) =>
 			{
 				if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
-					.find(|x| x.name() == variable_name)
+					.find(|x| x.matches_name(variable_name))
 				{
 					return std::rc::Rc::clone(&variable_declaration);
 				}
@@ -115,7 +115,7 @@ where
 			{
 				if let Some(variable_declaration) = bound_variable_declarations
 					.variable_declarations.iter()
-					.find(|x| x.name() == variable_name)
+					.find(|x| x.matches_name(variable_name))
 				{
 					return std::rc::Rc::clone(&variable_declaration);
 				}
@@ -184,7 +184,7 @@ where
 	{
 		let mut function_declarations = self.function_declarations.borrow_mut();
 
-		match function_declarations.iter().find(|x| x.name() == name && x.arity() == arity)
+		match function_declarations.iter().find(|x| x.matches_signature(name, arity))
 		{
 			Some(declaration) => std::rc::Rc::clone(&declaration),
 			None =>
@@ -209,7 +209,7 @@ where
 	{
 		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
 
-		match predicate_declarations.iter().find(|x| x.name() == name && x.arity() == arity)
+		match predicate_declarations.iter().find(|x| x.matches_signature(name, arity))
 		{
 			Some(declaration) => std::rc::Rc::clone(&declaration),
 			None =>