diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index b1a5e1f..32b07b9 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -297,26 +297,112 @@ impl std::fmt::Display for crate::Formula
 mod tests
 {
 	use crate::*;
+	use crate::format::terms::tests::*;
 
-	fn format(formula: &ast::Formula) -> String
+	fn format(formula: Box<ast::Formula>) -> String
 	{
 		format!("{}", formula)
 	}
 
-	#[test]
-	fn compare()
+	fn equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
 	{
-		let ad = std::rc::Rc::new(FunctionDeclaration::new("a".to_string(), 0));
-		let bd = std::rc::Rc::new(FunctionDeclaration::new("b".to_string(), 0));
+		Box::new(Formula::equal(left, right))
+	}
 
-		let a = || Box::new(Term::function(std::rc::Rc::clone(&ad), vec![]));
-		let b = || Box::new(Term::function(std::rc::Rc::clone(&bd), vec![]));
+	fn false_() -> Box<Formula>
+	{
+		Box::new(Formula::false_())
+	}
 
-		assert_eq!(format(&Formula::greater(a(), b())), "a > b");
-		assert_eq!(format(&Formula::less(a(), b())), "a < b");
-		assert_eq!(format(&Formula::less_or_equal(a(), b())), "a <= b");
-		assert_eq!(format(&Formula::greater_or_equal(a(), b())), "a >= b");
-		assert_eq!(format(&Formula::equal(a(), b())), "a = b");
-		assert_eq!(format(&Formula::not_equal(a(), b())), "a != b");
+	fn greater(left: Box<Term>, right: Box<Term>) -> Box<Formula>
+	{
+		Box::new(Formula::greater(left, right))
+	}
+
+	fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
+	{
+		Box::new(Formula::greater_or_equal(left, right))
+	}
+
+	fn less(left: Box<Term>, right: Box<Term>) -> Box<Formula>
+	{
+		Box::new(Formula::less(left, right))
+	}
+
+	fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
+	{
+		Box::new(Formula::less_or_equal(left, right))
+	}
+
+	fn not_equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
+	{
+		Box::new(Formula::not_equal(left, right))
+	}
+
+	fn predicate(name: &str, arguments: Vec<Box<Term>>) -> Box<Formula>
+	{
+		Box::new(Formula::predicate(predicate_declaration(name, arguments.len()), arguments))
+	}
+
+	fn predicate_declaration(name: &str, arity: usize) -> std::rc::Rc<PredicateDeclaration>
+	{
+		std::rc::Rc::new(PredicateDeclaration::new(name.to_string(), arity))
+	}
+
+	fn true_() -> Box<Formula>
+	{
+		Box::new(Formula::true_())
+	}
+
+	#[test]
+	fn format_boolean()
+	{
+		assert_eq!(format(true_()), "true");
+		assert_eq!(format(false_()), "false");
+	}
+
+	#[test]
+	fn format_compare()
+	{
+		assert_eq!(format(greater(constant("a"), constant("b"))), "a > b");
+		assert_eq!(format(less(constant("a"), constant("b"))), "a < b");
+		assert_eq!(format(less_or_equal(constant("a"), constant("b"))), "a <= b");
+		assert_eq!(format(greater_or_equal(constant("a"), constant("b"))), "a >= b");
+		assert_eq!(format(equal(constant("a"), constant("b"))), "a = b");
+		assert_eq!(format(not_equal(constant("a"), constant("b"))), "a != b");
+	}
+
+	#[test]
+	fn format_predicate()
+	{
+		assert_eq!(format(predicate("p", vec![])), "p");
+		assert_eq!(format(predicate("predicate", vec![])), "predicate");
+		assert_eq!(format(predicate("q", vec![constant("a")])), "q(a)");
+		assert_eq!(format(
+			predicate("q", vec![constant("a"), constant("b"), constant("c")])),
+			"q(a, b, c)");
+		assert_eq!(format(
+			predicate("predicate", vec![constant("a"), constant("b"), constant("c")])),
+			"predicate(a, b, c)");
+
+		assert_eq!(format(
+			predicate("predicate", vec![
+				exponentiate(absolute_value(multiply(constant("a"), integer(-20))), integer(2)),
+				string("test"),
+				function("f", vec![multiply(add(constant("b"), constant("c")),
+					subtract(constant("b"), constant("c"))), infimum(), variable("X")])])),
+			"predicate(|a * -20| ** 2, \"test\", f((b + c) * (b - c), #inf, X))");
+
+		// TODO: escape predicates that start with capital letters or that conflict with keywords
+	}
+
+	#[test]
+	fn format_predicate_declaration()
+	{
+		assert_eq!(format!("{}", predicate_declaration("p", 0)), "p/0");
+		assert_eq!(format!("{}", predicate_declaration("predicate", 0)), "predicate/0");
+		assert_eq!(format!("{}", predicate_declaration("q", 1)), "q/1");
+		assert_eq!(format!("{}", predicate_declaration("q", 3)), "q/3");
+		assert_eq!(format!("{}", predicate_declaration("predicate", 3)), "predicate/3");
 	}
 }
diff --git a/src/format/terms.rs b/src/format/terms.rs
index 60f0c57..f57813e 100644
--- a/src/format/terms.rs
+++ b/src/format/terms.rs
@@ -255,7 +255,7 @@ impl std::fmt::Display for crate::Term
 }
 
 #[cfg(test)]
-mod tests
+pub(crate) mod tests
 {
 	use crate::*;
 
@@ -264,97 +264,97 @@ mod tests
 		format!("{}", term)
 	}
 
-	fn absolute_value(argument: Box<Term>) -> Box<Term>
+	pub(crate) fn absolute_value(argument: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::absolute_value(argument))
 	}
 
-	fn add(left: Box<Term>, right: Box<Term>) -> Box<Term>
+	pub(crate) fn add(left: Box<Term>, right: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::add(left, right))
 	}
 
-	fn constant(name: &str) -> Box<Term>
+	pub(crate) fn constant(name: &str) -> Box<Term>
 	{
 		Box::new(Term::function(function_declaration(name, 0), vec![]))
 	}
 
-	fn divide(left: Box<Term>, right: Box<Term>) -> Box<Term>
+	pub(crate) fn divide(left: Box<Term>, right: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::divide(left, right))
 	}
 
-	fn exponentiate(left: Box<Term>, right: Box<Term>) -> Box<Term>
+	pub(crate) fn exponentiate(left: Box<Term>, right: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::exponentiate(left, right))
 	}
 
-	fn false_() -> Box<Term>
+	pub(crate) fn false_() -> Box<Term>
 	{
 		Box::new(Term::false_())
 	}
 
-	fn function(name: &str, arguments: Vec<Box<Term>>) -> Box<Term>
+	pub(crate) fn function(name: &str, arguments: Vec<Box<Term>>) -> Box<Term>
 	{
 		Box::new(Term::function(function_declaration(name, arguments.len()), arguments))
 	}
 
-	fn function_declaration(name: &str, arity: usize) -> std::rc::Rc<FunctionDeclaration>
+	pub(crate) fn function_declaration(name: &str, arity: usize) -> std::rc::Rc<FunctionDeclaration>
 	{
 		std::rc::Rc::new(FunctionDeclaration::new(name.to_string(), arity))
 	}
 
-	fn infimum() -> Box<Term>
+	pub(crate) fn infimum() -> Box<Term>
 	{
 		Box::new(Term::infimum())
 	}
 
-	fn integer(value: i32) -> Box<Term>
+	pub(crate) fn integer(value: i32) -> Box<Term>
 	{
 		Box::new(Term::integer(value))
 	}
 
-	fn modulo(left: Box<Term>, right: Box<Term>) -> Box<Term>
+	pub(crate) fn modulo(left: Box<Term>, right: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::modulo(left, right))
 	}
 
-	fn multiply(left: Box<Term>, right: Box<Term>) -> Box<Term>
+	pub(crate) fn multiply(left: Box<Term>, right: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::multiply(left, right))
 	}
 
-	fn negative(argument: Box<Term>) -> Box<Term>
+	pub(crate) fn negative(argument: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::negative(argument))
 	}
 
-	fn subtract(left: Box<Term>, right: Box<Term>) -> Box<Term>
+	pub(crate) fn subtract(left: Box<Term>, right: Box<Term>) -> Box<Term>
 	{
 		Box::new(Term::subtract(left, right))
 	}
 
-	fn supremum() -> Box<Term>
+	pub(crate) fn supremum() -> Box<Term>
 	{
 		Box::new(Term::supremum())
 	}
 
-	fn string(value: &str) -> Box<Term>
+	pub(crate) fn string(value: &str) -> Box<Term>
 	{
 		Box::new(Term::string(value.to_string()))
 	}
 
-	fn true_() -> Box<Term>
+	pub(crate) fn true_() -> Box<Term>
 	{
 		Box::new(Term::true_())
 	}
 
-	fn variable(name: &str) -> Box<Term>
+	pub(crate) fn variable(name: &str) -> Box<Term>
 	{
 		Box::new(Term::variable(variable_declaration(name)))
 	}
 
-	fn variable_declaration(name: &str) -> std::rc::Rc<VariableDeclaration>
+	pub(crate) fn variable_declaration(name: &str) -> std::rc::Rc<VariableDeclaration>
 	{
 		std::rc::Rc::new(VariableDeclaration::new(name.to_string()))
 	}
@@ -422,6 +422,14 @@ mod tests
 			function("function", vec![constant("a"), constant("b"), constant("c")])),
 			"function(a, b, c)");
 
+		assert_eq!(format(
+			function("function", vec![
+				exponentiate(absolute_value(multiply(constant("a"), integer(-20))), integer(2)),
+				string("test"),
+				function("f", vec![multiply(add(constant("b"), constant("c")),
+					subtract(constant("b"), constant("c"))), infimum(), variable("X")])])),
+			"function(|a * -20| ** 2, \"test\", f((b + c) * (b - c), #inf, X))");
+
 		// TODO: escape functions that start with capital letters or that conflict with keywords
 	}