diff --git a/Cargo.toml b/Cargo.toml
index 694d191..58547f2 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -11,3 +11,9 @@ keywords = ["logic"]
 categories = ["data-structures", "science"]
 license = "MIT"
 edition = "2018"
+
+[dependencies]
+nom = {version = "5.1", optional = true}
+
+[features]
+parse = ["nom"]
diff --git a/src/lib.rs b/src/lib.rs
index b5f6020..61aef19 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,4 +1,6 @@
 mod ast;
 pub mod format;
+#[cfg(feature = "parse")]
+pub mod parse;
 
 pub use ast::*;
diff --git a/src/parse.rs b/src/parse.rs
new file mode 100644
index 0000000..bcb0f64
--- /dev/null
+++ b/src/parse.rs
@@ -0,0 +1,1080 @@
+use nom::
+{
+	IResult,
+	bytes::complete::{take_while, take_while_m_n, is_not},
+	character::complete::{digit1, multispace0},
+	sequence::{preceded, delimited, pair},
+	combinator::{map, map_res},
+	multi::{many0, separated_list},
+	branch::alt,
+	bytes::complete::tag,
+};
+
+struct Declarations
+{
+	//function_declarations:,
+	//predicate_declarations:,
+	variable_declaration_stack: VariableDeclarationStack,
+}
+
+enum TermOperator
+{
+	Add,
+	Subtract,
+	Multiply,
+}
+
+fn infimum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		delimited(multispace0, tag("#inf"), multispace0),
+		|_| crate::Term::SpecialInteger(crate::SpecialInteger::Infimum)
+	)(i)
+}
+
+fn supremum<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		delimited(multispace0, tag("#sup"), multispace0),
+		|_| crate::Term::SpecialInteger(crate::SpecialInteger::Supremum)
+	)(i)
+}
+
+fn integer<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		map_res
+		(
+			delimited(multispace0, digit1, multispace0),
+			std::str::FromStr::from_str
+		),
+		crate::Term::Integer
+	)(i)
+}
+
+fn is_lowercase_alphanumeric(c: char) -> bool
+{
+	c.is_alphanumeric() && c.is_lowercase()
+}
+
+fn symbolic_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String>
+{
+	let (i, symbolic_identifier) = map
+	(
+		pair
+		(
+			take_while_m_n(1, 1, is_lowercase_alphanumeric),
+			take_while(char::is_alphanumeric)
+		),
+		|(s0, s1)| format!("{}{}", s0, s1)
+	)(i)?;
+
+	Ok((i, symbolic_identifier))
+}
+
+fn symbolic<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		delimited(multispace0, |i| symbolic_identifier(i, declarations), multispace0),
+		crate::Term::Symbolic
+	)(i)
+}
+
+fn string<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			delimited
+			(
+				tag("\""),
+				is_not("\""),
+				tag("\""),
+			),
+			multispace0
+		),
+		|s: &str| crate::Term::String(s.to_string())
+	)(i)
+}
+
+fn variable_identifier<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, String>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			preceded
+			(
+				take_while_m_n(1, 1, |c| char::is_alphabetic(c) && char::is_uppercase(c)),
+				take_while(char::is_alphanumeric)
+			),
+			multispace0
+		),
+		|s: &str| s.to_string()
+	)(i)
+}
+
+fn variable_declaration<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::VariableDeclaration>
+{
+	map
+	(
+		|i| variable_identifier(i, declarations),
+		|s| crate::VariableDeclaration{name: s},
+	)(i)
+}
+
+fn program_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		|i| program_variable_identifier(i, declarations),
+		|s|
+		{
+			let declaration = declarations.variable_declaration_stack.get(s.as_ref());
+
+			crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
+		},
+	)(i)
+}
+
+fn integer_variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	map
+	(
+		|i| integer_variable_identifier,
+		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}),
+	)(i)
+}
+
+fn variable<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	alt
+	((
+		|i| program_variable(i, declarations),
+		|i| integer_variable(i, declarations),
+	))(i)
+}
+
+fn predicate_0_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		delimited(multispace0, symbolic_identifier, multispace0),
+		|name| crate::Formula::Predicate(
+			crate::Predicate
+			{
+				declaration:
+					crate::PredicateDeclaration
+					{
+						name: name,
+						arity: 0,
+					},
+				arguments: vec![],
+			})
+	)(i)
+}
+
+fn predicate_n_ary<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			delimited(multispace0, symbolic_identifier, multispace0),
+			delimited
+			(
+				multispace0,
+				delimited
+				(
+					tag("("),
+					separated_list(tag(","), term),
+					tag(")")
+				),
+				multispace0
+			)
+		),
+		|(name, arguments)| crate::Formula::Predicate(
+				crate::Predicate
+				{
+					declaration:
+						crate::PredicateDeclaration
+						{
+							name: name,
+							arity: arguments.len(),
+						},
+					arguments: arguments,
+				})
+	)(i)
+}
+
+fn predicate<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		predicate_n_ary,
+		predicate_0_ary
+	))(i)
+}
+
+fn boolean<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			alt
+			((
+				map(tag("#true"), |_| true),
+				map(tag("#false"), |_| false)
+			)),
+			multispace0
+		),
+		|value| crate::Formula::Boolean(value)
+	)(i)
+}
+
+fn less<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			term,
+			preceded(tag("<"), term)
+		),
+		|(left, right)| crate::Formula::Less(left, right)
+	)(i)
+}
+
+fn less_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			term,
+			preceded(tag("<="), term)
+		),
+		|(left, right)| crate::Formula::LessOrEqual(left, right)
+	)(i)
+}
+
+fn greater<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			term,
+			preceded(tag(">"), term)
+		),
+		|(left, right)| crate::Formula::Greater(left, right)
+	)(i)
+}
+
+fn greater_or_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			term,
+			preceded(tag(">="), term)
+		),
+		|(left, right)| crate::Formula::GreaterOrEqual(left, right)
+	)(i)
+}
+
+fn equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			term,
+			preceded(tag("="), term)
+		),
+		|(left, right)| crate::Formula::Equal(left, right)
+	)(i)
+}
+
+fn not_equal<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		pair
+		(
+			term,
+			preceded(tag("!="), term)
+		),
+		|(left, right)| crate::Formula::NotEqual(left, right)
+	)(i)
+}
+
+fn comparison<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		less,
+		less_or_equal,
+		greater,
+		greater_or_equal,
+		equal,
+		not_equal
+	))(i)
+}
+
+fn term_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	delimited
+	(
+		multispace0,
+		delimited
+		(
+			tag("("),
+			term,
+			tag(")")
+		),
+		multispace0
+	)(i)
+}
+
+fn fold_terms(initial: crate::Term, remainder: Vec<(TermOperator, crate::Term)>) -> crate::Term
+{
+	remainder.into_iter().fold(initial,
+		|accumulator, pair|
+		{
+			let (term_operator, term) = pair;
+
+			match term_operator
+			{
+				TermOperator::Add => crate::Term::Add(Box::new(accumulator), Box::new(term)),
+				TermOperator::Subtract => crate::Term::Subtract(Box::new(accumulator), Box::new(term)),
+				TermOperator::Multiply => crate::Term::Multiply(Box::new(accumulator), Box::new(term)),
+			}
+		})
+}
+
+fn term_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	alt
+	((
+		infimum,
+		supremum,
+		integer,
+		symbolic,
+		string,
+		variable,
+		term_parenthesized
+	))(i)
+}
+
+fn term_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	alt
+	((
+		map
+		(
+			delimited
+			(
+				multispace0,
+				preceded(tag("-"), term_precedence_0),
+				multispace0
+			),
+			|term| crate::Term::Negative(Box::new(term))
+		),
+		term_precedence_0
+	))(i)
+}
+
+fn term_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	let (i, initial) = term_precedence_1(i)?;
+	let (i, remainder) =
+		many0
+		(
+			|i|
+			{
+				let (i, term) = preceded(tag("*"), term_precedence_1)(i)?;
+				Ok((i, (TermOperator::Multiply, term)))
+			}
+		)(i)?;
+
+	Ok((i, fold_terms(initial, remainder)))
+}
+
+fn term_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	let (i, initial) = term_precedence_2(i)?;
+	let (i, remainder) =
+		many0
+		(
+			alt
+			((
+				|i|
+				{
+					let (i, term) = preceded(tag("+"), term_precedence_2)(i)?;
+					Ok((i, (TermOperator::Add, term)))
+				},
+				|i|
+				{
+					let (i, term) = preceded(tag("-"), term_precedence_2)(i)?;
+					Ok((i, (TermOperator::Subtract, term)))
+				}
+			))
+		)(i)?;
+
+	Ok((i, fold_terms(initial, remainder)))
+}
+
+pub fn term<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Term>
+{
+	term_precedence_3(i)
+}
+
+fn formula_parenthesized<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	delimited
+	(
+		multispace0,
+		delimited
+		(
+			tag("("),
+			formula,
+			tag(")")
+		),
+		multispace0
+	)(i)
+}
+
+fn formula_precedence_0<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		comparison,
+		predicate,
+		boolean,
+		formula_parenthesized
+	))(i)
+}
+
+fn exists<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			preceded
+			(
+				tag("exists "),
+				pair
+				(
+					separated_list
+					(
+						tag(","),
+						variable_declaration
+					),
+					formula_precedence_1
+				)
+			),
+			multispace0
+		),
+		|(parameters, argument)| crate::Formula::Exists(
+			crate::Exists
+			{
+				parameters: parameters,
+				argument: Box::new(argument),
+			})
+	)(i)
+}
+
+fn for_all<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			preceded
+			(
+				tag("forall "),
+				pair
+				(
+					separated_list
+					(
+						tag(","),
+						variable_declaration
+					),
+					formula_precedence_1
+				)
+			),
+			multispace0
+		),
+		|(parameters, argument)| crate::Formula::ForAll(
+			crate::ForAll
+			{
+				parameters: parameters,
+				argument: Box::new(argument),
+			})
+	)(i)
+}
+
+fn formula_precedence_1<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		exists,
+		for_all,
+		formula_precedence_0
+	))(i)
+}
+
+fn formula_precedence_2<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		map
+		(
+			delimited
+			(
+				multispace0,
+				preceded(tag("not "), formula_precedence_1),
+				multispace0
+			),
+			|argument| crate::Formula::Not(Box::new(argument))
+		),
+		formula_precedence_1
+	))(i)
+}
+
+fn formula_precedence_3<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		map_res
+		(
+			separated_list(tag("and"), map(formula_precedence_2, |argument| Box::new(argument))),
+			|arguments|
+				match arguments.len()
+				{
+					// TODO: improve error handling
+					0 | 1 => Err(nom::Err::Error("")),
+					_ => Ok(crate::Formula::And(arguments)),
+				}
+		),
+		formula_precedence_2
+	))(i)
+}
+
+fn formula_precedence_4<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	alt
+	((
+		map_res
+		(
+			separated_list(tag("or"), map(formula_precedence_3, |argument| Box::new(argument))),
+			|arguments|
+				match arguments.len()
+				{
+					// TODO: improve error handling
+					0 | 1 => Err(nom::Err::Error("")),
+					_ => Ok(crate::Formula::Or(arguments)),
+				}
+		),
+		formula_precedence_3
+	))(i)
+}
+
+fn formula_precedence_5<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	let (i, left) = formula_precedence_4(i)?;
+
+	match preceded(tag("->"), formula_precedence_4)(i)
+	{
+		Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right)))),
+		Err(_) => Ok((i, left)),
+	}
+}
+
+fn formula_precedence_6<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	let (i, left) = formula_precedence_5(i)?;
+
+	match preceded(tag("<->"), formula_precedence_5)(i)
+	{
+		Ok((i, right)) => Ok((i, crate::Formula::Biconditional(Box::new(left), Box::new(right)))),
+		Err(_) => Ok((i, left)),
+	}
+}
+
+pub fn formula<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, crate::Formula>
+{
+	formula_precedence_6(i)
+}
+
+pub fn formulas<'a>(i: &'a str, declarations: &Declarations) -> IResult<&'a str, Vec<crate::Formula>>
+{
+	many0(formula)(i)
+}
+
+#[cfg(test)]
+mod tests
+{
+	#[test]
+	fn parse_integer()
+	{
+		assert_eq!(crate::term("12345"), Ok(("", crate::Term::Integer(12345))));
+	}
+
+	#[test]
+	fn parse_variable_declaration()
+	{
+		assert_eq!(crate::term(" X5 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
+		assert_eq!(crate::term(" NX3 "), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
+	}
+
+	#[test]
+	fn parse_variable()
+	{
+		assert_eq!(crate::term("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
+		assert_eq!(crate::term("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
+	}
+
+	#[test]
+	fn parse_string()
+	{
+		assert_eq!(crate::term(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string()))));
+	}
+
+	#[test]
+	fn parse_boolean()
+	{
+		assert_eq!(crate::formula(" #true "), Ok(("", crate::Formula::Boolean(true))));
+		assert_eq!(crate::formula(" #false "), Ok(("", crate::Formula::Boolean(false))));
+	}
+
+	#[test]
+	fn parse_term()
+	{
+		assert_eq!(crate::term(" 5 + 3"), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Integer(3)),
+			))));
+
+		assert_eq!(crate::term(" -5"), Ok(("",
+				crate::Term::Negative
+				(
+					Box::new(crate::Term::Integer(5))
+				)
+			)));
+
+		assert_eq!(crate::term(" 5+3 * -(9+ 1)  + 2 "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Add
+				(
+					Box::new(crate::Term::Integer(5)),
+					Box::new(crate::Term::Multiply
+					(
+						Box::new(crate::Term::Integer(3)),
+						Box::new(crate::Term::Negative
+						(
+							Box::new(crate::Term::Add
+							(
+								Box::new(crate::Term::Integer(9)),
+								Box::new(crate::Term::Integer(1)),
+							))
+						)),
+					)),
+				)),
+				Box::new(crate::Term::Integer(2)),
+			))));
+
+		assert_eq!(crate::term(" 5 + a "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Symbolic("a".to_string())),
+			))));
+
+		assert_eq!(crate::term(" 5 + #sup "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Supremum),
+			))));
+
+		assert_eq!(crate::term(" 5 + #inf "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Infimum),
+			))));
+
+		assert_eq!(crate::term(" 5 + \" text \" "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::String(" text ".to_string())),
+			))));
+
+		assert_eq!(crate::term(" 5 + X1 "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "1".to_string()})),
+			))));
+	}
+
+	#[test]
+	fn parse_predicate()
+	{
+		assert_eq!(crate::formula(" p "), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));
+
+		assert_eq!(crate::formula(" p(5, 6, 7) "), Ok(("",
+			crate::Formula::Predicate
+			(
+				crate::Predicate
+				{
+					declaration:
+						crate::PredicateDeclaration
+						{
+							name: "p".to_string(),
+							arity: 3,
+						},
+					arguments:
+						vec!
+						[
+							crate::Term::Integer(5),
+							crate::Term::Integer(6),
+							crate::Term::Integer(7),
+						],
+				}
+			))));
+
+		assert_eq!(crate::formula(" p(1, 3+4*5+6, \"test\") "), Ok(("",
+			crate::Formula::Predicate
+			(
+				crate::Predicate
+				{
+					declaration:
+						crate::PredicateDeclaration
+						{
+							name: "p".to_string(),
+							arity: 3,
+						},
+					arguments:
+						vec!
+						[
+							crate::Term::Integer(1),
+							crate::Term::Add
+							(
+								Box::new(crate::Term::Add
+								(
+									Box::new(crate::Term::Integer(3)),
+									Box::new(crate::Term::Multiply
+									(
+										Box::new(crate::Term::Integer(4)),
+										Box::new(crate::Term::Integer(5)),
+									)),
+								)),
+								Box::new(crate::Term::Integer(6)),
+							),
+							crate::Term::String("test".to_string()),
+						],
+				}
+			))));
+	}
+
+	#[test]
+	fn parse_comparison()
+	{
+		assert_eq!(crate::formula("5 + 9 < #sup"), Ok(("",
+			crate::Formula::Less
+			(
+				crate::Term::Add
+				(
+					Box::new(crate::Term::Integer(5)),
+					Box::new(crate::Term::Integer(9)),
+				),
+				crate::Term::Supremum,
+			))));
+
+		assert_eq!(crate::formula("#inf != 6 * 9"), Ok(("",
+			crate::Formula::NotEqual
+			(
+				crate::Term::Infimum,
+				crate::Term::Multiply
+				(
+					Box::new(crate::Term::Integer(6)),
+					Box::new(crate::Term::Integer(9)),
+				),
+			))));
+
+		assert_eq!(crate::formula("n = 5"), Ok(("",
+			crate::Formula::Equal
+			(
+				crate::Term::Symbolic("n".to_string()),
+				crate::Term::Integer(5),
+			))));
+	}
+
+	#[test]
+	fn formula()
+	{
+		assert_eq!(crate::formula("p(1, a) or q(2)"), Ok(("",
+			crate::Formula::Or
+			(
+				vec!
+				[
+					Box::new(crate::Formula::Predicate
+					(
+						crate::Predicate
+						{
+							declaration:
+								crate::PredicateDeclaration
+								{
+									name: "p".to_string(),
+									arity: 2,
+								},
+							arguments:
+								vec!
+								[
+									crate::Term::Integer(1),
+									crate::Term::Symbolic("a".to_string()),
+								],
+						}
+					)),
+					Box::new(crate::Formula::Predicate
+					(
+						crate::Predicate
+						{
+							declaration:
+								crate::PredicateDeclaration
+								{
+									name: "q".to_string(),
+									arity: 1,
+								},
+							arguments:
+								vec!
+								[
+									crate::Term::Integer(2),
+								],
+						}
+					)),
+				]
+			))));
+
+		assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2)"), Ok(("",
+			crate::Formula::Or
+			(
+				vec!
+				[
+					Box::new(crate::Formula::And
+					(
+						vec!
+						[
+							Box::new(crate::Formula::Less
+							(
+								crate::Term::Infimum,
+								crate::Term::Integer(5),
+							)),
+							Box::new(crate::Formula::Predicate
+							(
+								crate::Predicate
+								{
+									declaration:
+										crate::PredicateDeclaration
+										{
+											name: "p".to_string(),
+											arity: 2,
+										},
+									arguments:
+										vec!
+										[
+											crate::Term::Integer(1),
+											crate::Term::Symbolic("a".to_string()),
+										],
+								}
+							)),
+						]
+					)),
+					Box::new(crate::Formula::Predicate
+					(
+						crate::Predicate
+						{
+							declaration:
+								crate::PredicateDeclaration
+								{
+									name: "q".to_string(),
+									arity: 1,
+								},
+							arguments:
+								vec!
+								[
+									crate::Term::Integer(2),
+								],
+						}
+					)),
+				]
+			))));
+
+		assert_eq!(crate::formula("#inf < 5 and p(1, a) or q(2) -> #false"), Ok(("",
+			crate::Formula::Implies
+			(
+				Box::new(crate::Formula::Or
+				(
+					vec!
+					[
+						Box::new(crate::Formula::And
+						(
+							vec!
+							[
+								Box::new(crate::Formula::Less
+								(
+									crate::Term::Infimum,
+									crate::Term::Integer(5),
+								)),
+								Box::new(crate::Formula::Predicate
+								(
+									crate::Predicate
+									{
+										declaration:
+											crate::PredicateDeclaration
+											{
+												name: "p".to_string(),
+												arity: 2,
+											},
+										arguments:
+											vec!
+											[
+												crate::Term::Integer(1),
+												crate::Term::Symbolic("a".to_string()),
+											],
+									}
+								)),
+							]
+						)),
+						Box::new(crate::Formula::Predicate
+						(
+							crate::Predicate
+							{
+								declaration:
+									crate::PredicateDeclaration
+									{
+										name: "q".to_string(),
+										arity: 1,
+									},
+								arguments:
+									vec!
+									[
+										crate::Term::Integer(2),
+									],
+							}
+						)),
+					]
+				)),
+				Box::new(crate::Formula::Boolean(false)),
+			))));
+
+		assert_eq!(crate::formula(" not #true"), Ok(("",
+			crate::Formula::Not(Box::new(crate::Formula::Boolean(true))))));
+
+		assert_eq!(crate::formula("exists X forall N1 p(1, 2) and #false"), Ok(("",
+			crate::Formula::And
+			(
+				vec!
+				[
+					Box::new(crate::Formula::Exists
+					(
+						crate::Exists
+						{
+							parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}],
+							argument:
+								Box::new(crate::Formula::ForAll
+								(
+									crate::ForAll
+									{
+										parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}],
+										argument:
+											Box::new(crate::Formula::Predicate
+											(
+												crate::Predicate
+												{
+													declaration:
+														crate::PredicateDeclaration
+														{
+															name: "p".to_string(),
+															arity: 2,
+														},
+													arguments:
+														vec!
+														[
+															crate::Term::Integer(1),
+															crate::Term::Integer(2),
+														],
+												}
+											)),
+									}
+								)),
+						}
+					)),
+					Box::new(crate::Formula::Boolean(false)),
+				]
+			))));
+
+		assert_eq!(crate::formula("exists X forall N1 (p(1, 2) and #false)"), Ok(("",
+			crate::Formula::Exists
+			(
+				crate::Exists
+				{
+					parameters: vec![crate::VariableDeclaration{name: "".to_string(), domain: crate::Domain::Program}],
+					argument:
+						Box::new(crate::Formula::ForAll
+						(
+							crate::ForAll
+							{
+								parameters: vec![crate::VariableDeclaration{name: "1".to_string(), domain: crate::Domain::Integer}],
+								argument:
+									Box::new(crate::Formula::And
+									(
+										vec!
+										[
+											Box::new(crate::Formula::Predicate
+											(
+												crate::Predicate
+												{
+													declaration:
+														crate::PredicateDeclaration
+														{
+															name: "p".to_string(),
+															arity: 2,
+														},
+													arguments:
+														vec!
+														[
+															crate::Term::Integer(1),
+															crate::Term::Integer(2),
+														],
+												}
+											)),
+											Box::new(crate::Formula::Boolean(false)),
+										]
+									)),
+							}
+						)),
+				}
+			))));
+	}
+}