diff --git a/src/lib.rs b/src/lib.rs
index 09d86b2..01cf22d 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -6,11 +6,13 @@ pub mod error;
 pub mod input;
 pub mod output;
 pub mod problem;
+pub mod simplify;
 pub(crate) mod traits;
 pub mod translate;
 mod utils;
 
 pub use error::Error;
 pub use problem::Problem;
+pub(crate) use simplify::*;
 pub(crate) use utils::*;
 pub use utils::Domain;
diff --git a/src/simplify.rs b/src/simplify.rs
new file mode 100644
index 0000000..86d4925
--- /dev/null
+++ b/src/simplify.rs
@@ -0,0 +1,246 @@
+#[derive(Clone, Copy, Eq, PartialEq)]
+enum SimplificationResult
+{
+	Simplified,
+	NotSimplified,
+}
+
+impl SimplificationResult
+{
+	fn or(&self, other: SimplificationResult) -> SimplificationResult
+	{
+		match (self, other)
+		{
+			(SimplificationResult::NotSimplified, SimplificationResult::NotSimplified)
+				=> SimplificationResult::NotSimplified,
+			_ => SimplificationResult::Simplified,
+		}
+	}
+}
+
+fn remove_unnecessary_exists_parameters(formula: &mut foliage::Formula) -> SimplificationResult
+{
+	use foliage::Formula;
+
+	match formula
+	{
+		Formula::And(ref mut arguments)
+		| Formula::IfAndOnlyIf(ref mut arguments)
+		| Formula::Or(ref mut arguments) =>
+		{
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					remove_unnecessary_exists_parameters(argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(ref mut quantified_formula) =>
+		{
+			let mut simplification_result =
+				remove_unnecessary_exists_parameters(&mut quantified_formula.argument);
+
+			let arguments = match *quantified_formula.argument
+			{
+				Formula::And(ref mut arguments) => arguments,
+				_ => return remove_unnecessary_exists_parameters(&mut quantified_formula.argument),
+			};
+
+			// TODO: do not copy parameters, use std::vec::Vec::retain instead
+			quantified_formula.parameters =
+				std::rc::Rc::new(quantified_formula.parameters.iter().filter_map(
+					|parameter|
+					{
+						let assignment = arguments.iter().enumerate().find_map(
+							|(argument_index, argument)|
+							{
+								let (left, right) = match argument
+								{
+									Formula::Compare(foliage::Compare{
+										operator: foliage::ComparisonOperator::Equal, ref left,
+										ref right})
+										=> (left, right),
+									_ => return None,
+								};
+
+								if let foliage::Term::Variable(ref variable) = **left
+								{
+									if variable.declaration == *parameter
+										&& !crate::term_contains_variable(right, parameter)
+									{
+										// TODO: avoid copy
+										return Some((argument_index, crate::copy_term(right)));
+									}
+								}
+
+								if let foliage::Term::Variable(ref variable) = **right
+								{
+									if variable.declaration == *parameter
+										&& !crate::term_contains_variable(left, parameter)
+									{
+										// TODO: avoid copy
+										return Some((argument_index, crate::copy_term(left)));
+									}
+								}
+
+								None
+							});
+
+						if let Some((assignment_index, assigned_term)) = assignment
+						{
+							arguments.remove(assignment_index);
+
+							for argument in arguments.iter_mut()
+							{
+								crate::replace_variable_in_formula_with_term(argument, parameter,
+									&assigned_term);
+							}
+
+							simplification_result = SimplificationResult::Simplified;
+
+							return None;
+						}
+
+						Some(std::rc::Rc::clone(parameter))
+					})
+					.collect());
+
+			simplification_result
+		}
+		Formula::ForAll(ref mut quantified_formula) =>
+			remove_unnecessary_exists_parameters(&mut quantified_formula.argument),
+		Formula::Implies(ref mut implies) =>
+			remove_unnecessary_exists_parameters(&mut implies.antecedent)
+				.or(remove_unnecessary_exists_parameters(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			remove_unnecessary_exists_parameters(argument),
+	}
+}
+
+fn simplify_quantified_formulas_without_parameters(formula: &mut foliage::Formula)
+	-> SimplificationResult
+{
+	use foliage::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for mut argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					simplify_quantified_formulas_without_parameters(&mut argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(quantified_formula)
+		| Formula::ForAll(quantified_formula) =>
+		{
+			if quantified_formula.parameters.is_empty()
+			{
+				// TODO: remove workaround
+				let mut argument = foliage::Formula::false_();
+				std::mem::swap(&mut argument, &mut quantified_formula.argument);
+
+				*formula = argument;
+
+				return SimplificationResult::Simplified;
+			}
+
+			simplify_quantified_formulas_without_parameters(&mut quantified_formula.argument)
+		},
+		Formula::Implies(ref mut implies) =>
+			simplify_quantified_formulas_without_parameters(&mut implies.antecedent)
+				.or(simplify_quantified_formulas_without_parameters(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			simplify_quantified_formulas_without_parameters(argument),
+	}
+}
+
+fn simplify_trivial_n_ary_formulas(formula: &mut foliage::Formula) -> SimplificationResult
+{
+	use foliage::Formula;
+
+	match formula
+	{
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments) if arguments.is_empty() =>
+		{
+			*formula = foliage::Formula::true_();
+
+			return SimplificationResult::Simplified;
+		},
+		| Formula::Or(arguments) if arguments.is_empty() =>
+		{
+			*formula = foliage::Formula::false_();
+
+			return SimplificationResult::Simplified;
+		},
+		Formula::And(arguments)
+		| Formula::IfAndOnlyIf(arguments)
+		| Formula::Or(arguments) =>
+		{
+			if arguments.len() == 1
+			{
+				*formula = arguments.remove(0);
+
+				return SimplificationResult::Simplified;
+			}
+
+			let mut simplification_result = SimplificationResult::NotSimplified;
+
+			for mut argument in arguments
+			{
+				simplification_result = simplification_result.or(
+					simplify_trivial_n_ary_formulas(&mut argument));
+			}
+
+			simplification_result
+		},
+		Formula::Boolean(_)
+		| Formula::Compare(_)
+		| Formula::Predicate(_) => SimplificationResult::NotSimplified,
+		Formula::Exists(ref mut quantified_formula)
+		| Formula::ForAll(ref mut quantified_formula) =>
+			simplify_trivial_n_ary_formulas(&mut quantified_formula.argument),
+		Formula::Implies(ref mut implies) =>
+			simplify_trivial_n_ary_formulas(&mut implies.antecedent)
+				.or(simplify_trivial_n_ary_formulas(&mut implies.implication)),
+		Formula::Not(ref mut argument) =>
+			simplify_trivial_n_ary_formulas(argument),
+	}
+}
+
+pub(crate) fn simplify(formula: &mut foliage::Formula)
+{
+	loop
+	{
+		if remove_unnecessary_exists_parameters(formula) == SimplificationResult::Simplified
+			|| simplify_quantified_formulas_without_parameters(formula)
+				== SimplificationResult::Simplified
+			|| simplify_trivial_n_ary_formulas(formula) == SimplificationResult::Simplified
+		{
+			log::debug!("cool, simplified!");
+
+			continue;
+		}
+
+		log::debug!("nope, that’s it");
+
+		break;
+	}
+}
diff --git a/src/utils.rs b/src/utils.rs
index 27a58c5..6ec4375 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -2,11 +2,13 @@ mod arithmetic_terms;
 mod closures;
 mod copy_formula;
 mod output_predicates;
+mod variables_in_terms;
 
 pub(crate) use arithmetic_terms::*;
 pub(crate) use closures::*;
 pub(crate) use copy_formula::*;
 pub(crate) use output_predicates::*;
+pub(crate) use variables_in_terms::*;
 
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub(crate) enum OperatorNotation
diff --git a/src/utils/copy_formula.rs b/src/utils/copy_formula.rs
index 748f8ed..96c26fd 100644
--- a/src/utils/copy_formula.rs
+++ b/src/utils/copy_formula.rs
@@ -172,7 +172,7 @@ pub(crate) fn replace_variable_in_formula_with_term(formula: &mut foliage::Formu
 	}
 }
 
-fn copy_term(term: &foliage::Term) -> foliage::Term
+pub(crate) fn copy_term(term: &foliage::Term) -> foliage::Term
 {
 	use foliage::Term;
 
diff --git a/src/utils/variables_in_terms.rs b/src/utils/variables_in_terms.rs
new file mode 100644
index 0000000..73de49b
--- /dev/null
+++ b/src/utils/variables_in_terms.rs
@@ -0,0 +1,21 @@
+pub(crate) fn term_contains_variable(term: &foliage::Term,
+	variable_declaration: &foliage::VariableDeclaration)
+	-> bool
+{
+	use foliage::Term;
+
+	match term
+	{
+		Term::BinaryOperation(binary_operation) =>
+			term_contains_variable(&binary_operation.left, variable_declaration)
+				|| term_contains_variable(&binary_operation.right, variable_declaration),
+		Term::Boolean(_)
+		| Term::Function(_)
+		| Term::Integer(_)
+		| Term::SpecialInteger(_)
+		| Term::String(_) => false,
+		Term::UnaryOperation(unary_operation) =>
+			term_contains_variable(&unary_operation.argument, variable_declaration),
+		Term::Variable(variable) => *variable.declaration == *variable_declaration,
+	}
+}