Initial commit

This provides an abstract syntax tree for first-order logic with integer arithmetics. Initially, the following types of formulas are supported: - Booleans values (true and false) - predicates - negated formulas - comparisons of terms (<, ≤, >, ≥, =, ≠) - implications and biconditionals - conjunctions and disjunctions of formulas - existentially and universally quantified formulas In addition, these types of terms are provided: - Boolean values (true and false) - integers - strings - special integers (infimum and supremum) - symbolic functions - variables - binary operations (addition, subtraction, multiplication, division, modulo, exponentiation) - unary operations (absolute value, numeric negation)
2 years ago · a446aed011
7 changed files with 1065 additions and 0 deletions
--- a/.gitignore
+++ b/.gitignore
@ -0,0 +1,3 @@
+/Cargo.lock
+/target
+**/*.rs.bk
--- a/Cargo.toml
+++ b/Cargo.toml
@ -0,0 +1,13 @@
+[package]
+name = "foliage"
+version = "0.1.0"
+authors = ["Patrick Lühne <patrick@luehne.de>"]
+description = "Abstract syntax tree for first-order logic with integer arithmetics"
+documentation = "https://github.com/potassco/foliage"
+homepage = "https://github.com/potassco/foliage"
+repository = "https://github.com/potassco/foliage"
+readme = "README.md"
+keywords = ["logic"]
+categories = ["data-structures", "science"]
+license = "MIT"
+edition = "2018"
--- a/LICENSE.md
+++ b/LICENSE.md
@ -0,0 +1,21 @@
+# The MIT License (MIT)
+
+Copyright © 2020 Patrick Lühne
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
--- a/README.md
+++ b/README.md
@ -0,0 +1,26 @@
+# foliage [![GitHub release](https://img.shields.io/github/release/potassco/foliage.svg?maxAge=3600)](https://github.com/potassco/foliage/releases) [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
+
+> First-order logic with integer arithmetics in Rust
+
+This Rust crate provides an abstract syntax tree for first-order formulas with integer arithmetics.
+
+## Supported Formulas
+
+- Booleans values (`true` and `false`)
+- predicates
+- negated formulas
+- comparisons of terms (<, ≤, >, ≥, =, ≠)
+- implications and biconditionals
+- conjunctions and disjunctions of formulas
+- existentially and universally quantified formulas
+
+## Supported Terms
+
+- Boolean values (`true` and `false`)
+- integers
+- strings
+- special integers (infimum and supremum)
+- symbolic functions
+- variables
+- binary operations (addition, subtraction, multiplication, division, modulo, exponentiation)
+- unary operations (absolute value, numeric negation)
--- a/src/ast.rs
+++ b/src/ast.rs
@ -0,0 +1,565 @@
+// Operators
+
+pub enum BinaryOperator
+{
+	Add,
+	Subtract,
+	Multiply,
+	Divide,
+	Modulo,
+	Exponentiate,
+}
+
+pub enum ComparisonOperator
+{
+	Greater,
+	Less,
+	LessOrEqual,
+	GreaterOrEqual,
+	NotEqual,
+	Equal,
+}
+
+pub enum UnaryOperator
+{
+	AbsoluteValue,
+	Negative,
+}
+
+// Primitives
+
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
+pub struct FunctionDeclaration
+{
+	pub name: String,
+	pub arity: usize,
+}
+
+impl FunctionDeclaration
+{
+	pub fn new(name: String, arity: usize) -> Self
+	{
+		Self
+		{
+			name,
+			arity,
+		}
+	}
+}
+
+pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
+
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
+pub struct PredicateDeclaration
+{
+	pub name: String,
+	pub arity: usize,
+}
+
+impl PredicateDeclaration
+{
+	pub fn new(name: String, arity: usize) -> Self
+	{
+		Self
+		{
+			name,
+			arity,
+		}
+	}
+}
+
+pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
+
+pub struct VariableDeclaration
+{
+	pub name: String,
+}
+
+impl std::cmp::PartialEq for VariableDeclaration
+{
+	#[inline(always)]
+	fn eq(&self, other: &VariableDeclaration) -> bool
+	{
+		let l = self as *const VariableDeclaration;
+		let r = other as *const VariableDeclaration;
+
+		l.eq(&r)
+	}
+}
+
+impl std::cmp::Eq for VariableDeclaration
+{
+}
+
+impl std::cmp::PartialOrd for VariableDeclaration
+{
+	#[inline(always)]
+	fn partial_cmp(&self, other: &VariableDeclaration) -> Option<std::cmp::Ordering>
+	{
+		let l = self as *const VariableDeclaration;
+		let r = other as *const VariableDeclaration;
+
+		l.partial_cmp(&r)
+	}
+}
+
+impl std::cmp::Ord for VariableDeclaration
+{
+	#[inline(always)]
+	fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering
+	{
+		let l = self as *const VariableDeclaration;
+		let r = other as *const VariableDeclaration;
+
+		l.cmp(&r)
+	}
+}
+
+impl VariableDeclaration
+{
+	pub fn new(name: String) -> Self
+	{
+		Self
+		{
+			name,
+		}
+	}
+}
+
+pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
+
+// Terms
+
+pub struct BinaryOperation
+{
+	pub operator: BinaryOperator,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
+}
+
+impl BinaryOperation
+{
+	pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self
+		{
+			operator,
+			left,
+			right,
+		}
+	}
+}
+
+pub struct Function
+{
+	pub declaration: std::rc::Rc<FunctionDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+impl Function
+{
+	pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	{
+		assert_eq!(declaration.arity, arguments.len(),
+			"function has a different number of arguments then declared");
+
+		Self
+		{
+			declaration: std::rc::Rc::clone(declaration),
+			arguments,
+		}
+	}
+}
+
+pub enum SpecialInteger
+{
+	Infimum,
+	Supremum,
+}
+
+pub struct UnaryOperation
+{
+	pub operator: UnaryOperator,
+	pub argument: Box<Term>,
+}
+
+impl UnaryOperation
+{
+	pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
+	{
+		Self
+		{
+			operator,
+			argument,
+		}
+	}
+}
+
+pub struct Variable
+{
+	pub declaration: std::rc::Rc<VariableDeclaration>,
+}
+
+impl Variable
+{
+	pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
+	{
+		Self
+		{
+			declaration: std::rc::Rc::clone(declaration),
+		}
+	}
+}
+
+// Formulas
+
+pub struct Compare
+{
+	pub operator: ComparisonOperator,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
+}
+
+impl Compare
+{
+	pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self
+		{
+			operator,
+			left,
+			right,
+		}
+	}
+}
+
+pub struct Exists
+{
+	pub parameters: std::rc::Rc<VariableDeclarations>,
+	pub argument: Box<Formula>,
+}
+
+impl Exists
+{
+	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	{
+		Self
+		{
+			parameters,
+			argument,
+		}
+	}
+}
+
+pub struct ForAll
+{
+	pub parameters: std::rc::Rc<VariableDeclarations>,
+	pub argument: Box<Formula>,
+}
+
+impl ForAll
+{
+	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	{
+		Self
+		{
+			parameters,
+			argument,
+		}
+	}
+}
+
+pub struct IfAndOnlyIf
+{
+	pub left: Box<Formula>,
+	pub right: Box<Formula>,
+}
+
+impl IfAndOnlyIf
+{
+	pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
+	{
+		Self
+		{
+			left,
+			right,
+		}
+	}
+}
+
+pub struct Implies
+{
+	pub antecedent: Box<Formula>,
+	pub implication: Box<Formula>,
+}
+
+impl Implies
+{
+	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
+	{
+		Self
+		{
+			antecedent,
+			implication,
+		}
+	}
+}
+
+pub struct Predicate
+{
+	pub declaration: std::rc::Rc<PredicateDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+impl Predicate
+{
+	pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	{
+		assert_eq!(declaration.arity, arguments.len(),
+			"predicate has a different number of arguments then declared");
+
+		Self
+		{
+			declaration: std::rc::Rc::clone(declaration),
+			arguments,
+		}
+	}
+}
+
+// Variants
+
+pub enum Term
+{
+	BinaryOperation(BinaryOperation),
+	Boolean(bool),
+	Function(Function),
+	Integer(i32),
+	SpecialInteger(SpecialInteger),
+	String(String),
+	UnaryOperation(UnaryOperation),
+	Variable(Variable),
+}
+
+pub type Terms = Vec<Box<Term>>;
+
+impl Term
+{
+	pub fn absolute_value(argument: Box<Term>) -> Self
+	{
+		Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
+	}
+
+	pub fn add(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::binary_operation(BinaryOperator::Add, left, right)
+	}
+
+	pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::BinaryOperation(BinaryOperation::new(operator, left, right))
+	}
+
+	pub fn boolean(value: bool) -> Self
+	{
+		Self::Boolean(value)
+	}
+
+	pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::binary_operation(BinaryOperator::Divide, left, right)
+	}
+
+	pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::binary_operation(BinaryOperator::Exponentiate, left, right)
+	}
+
+	pub fn false_() -> Self
+	{
+		Self::boolean(false)
+	}
+
+	pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
+		-> Self
+	{
+		Self::Function(Function::new(declaration, arguments))
+	}
+
+	pub fn infimum() -> Self
+	{
+		Self::special_integer(SpecialInteger::Infimum)
+	}
+
+	pub fn integer(value: i32) -> Self
+	{
+		Self::Integer(value)
+	}
+
+	pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::binary_operation(BinaryOperator::Modulo, left, right)
+	}
+
+	pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::binary_operation(BinaryOperator::Multiply, left, right)
+	}
+
+	pub fn negative(argument: Box<Term>) -> Self
+	{
+		Self::unary_operation(UnaryOperator::Negative, argument)
+	}
+
+	pub fn special_integer(value: SpecialInteger) -> Self
+	{
+		Self::SpecialInteger(value)
+	}
+
+	pub fn string(value: String) -> Self
+	{
+		Self::String(value)
+	}
+
+	pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::binary_operation(BinaryOperator::Subtract, left, right)
+	}
+
+	pub fn supremum() -> Self
+	{
+		Self::special_integer(SpecialInteger::Supremum)
+	}
+
+	pub fn true_() -> Self
+	{
+		Self::boolean(true)
+	}
+
+	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
+	{
+		Self::UnaryOperation(UnaryOperation::new(operator, argument))
+	}
+
+	pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
+	{
+		Self::Variable(Variable::new(declaration))
+	}
+}
+
+pub enum Formula
+{
+	And(Formulas),
+	Boolean(bool),
+	Compare(Compare),
+	Exists(Exists),
+	ForAll(ForAll),
+	IfAndOnlyIf(IfAndOnlyIf),
+	Implies(Implies),
+	Not(Box<Formula>),
+	Or(Formulas),
+	Predicate(Predicate),
+}
+
+pub type Formulas = Vec<Box<Formula>>;
+
+impl Formula
+{
+	pub fn and(arguments: Formulas) -> Self
+	{
+		assert!(!arguments.is_empty());
+
+		Self::And(arguments)
+	}
+
+	pub fn boolean(value: bool) -> Self
+	{
+		Self::Boolean(value)
+	}
+
+	pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::Compare(Compare::new(operator, left, right))
+	}
+
+	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	{
+		assert!(!parameters.is_empty());
+
+		Self::Exists(Exists::new(parameters, argument))
+	}
+
+	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::compare(ComparisonOperator::Equal, left, right)
+	}
+
+	pub fn false_() -> Self
+	{
+		Self::boolean(false)
+	}
+
+	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	{
+		assert!(!parameters.is_empty());
+
+		Self::ForAll(ForAll::new(parameters, argument))
+	}
+
+	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::compare(ComparisonOperator::Greater, left, right)
+	}
+
+	pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
+	}
+
+	pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
+	{
+		Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
+	}
+
+	pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
+	{
+		Self::Implies(Implies::new(antecedent, consequent))
+	}
+
+	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::compare(ComparisonOperator::Less, left, right)
+	}
+
+	pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::compare(ComparisonOperator::LessOrEqual, left, right)
+	}
+
+	pub fn not(argument: Box<Formula>) -> Self
+	{
+		Self::Not(argument)
+	}
+
+	pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
+	{
+		Self::compare(ComparisonOperator::NotEqual, left, right)
+	}
+
+	pub fn or(arguments: Formulas) -> Self
+	{
+		assert!(!arguments.is_empty());
+
+		Self::Or(arguments)
+	}
+
+	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
+		-> Self
+	{
+		Self::Predicate(Predicate::new(declaration, arguments))
+	}
+
+	pub fn true_() -> Self
+	{
+		Self::boolean(true)
+	}
+}
--- a/src/format.rs
+++ b/src/format.rs
@ -0,0 +1,433 @@
+trait Precedence
+{
+	fn precedence(&self) -> i32;
+}
+
+impl Precedence for crate::Term
+{
+	fn precedence(&self) -> i32
+	{
+		match &self
+		{
+			Self::Boolean(_)
+			| Self::Function(_)
+			| Self::SpecialInteger(_)
+			| Self::Integer(_)
+			| Self::String(_)
+			| Self::Variable(_)
+				=> 0,
+			Self::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
+				=> 1,
+			Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
+				=> 2,
+			Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
+			| Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
+			| Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
+				=> 3,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
+			| Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
+				=> 4,
+			Self::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
+				=> 5,
+		}
+	}
+}
+
+impl Precedence for crate::Formula
+{
+	fn precedence(&self) -> i32
+	{
+		match &self
+		{
+			Self::Predicate(_)
+			| Self::Boolean(_)
+			| Self::Compare(_)
+				=> 0,
+			Self::Exists(_)
+			| Self::ForAll(_)
+				=> 1,
+			Self::Not(_)
+				=> 2,
+			Self::And(_)
+				=> 3,
+			Self::Or(_)
+				=> 4,
+			Self::Implies(_)
+				=> 5,
+			Self::IfAndOnlyIf(_)
+				=> 6,
+		}
+	}
+}
+
+impl std::fmt::Debug for crate::FunctionDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}/{}", &self.name, self.arity)
+	}
+}
+
+impl std::fmt::Display for crate::FunctionDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+impl std::fmt::Debug for crate::PredicateDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}/{}", &self.name, self.arity)
+	}
+}
+
+impl std::fmt::Display for crate::PredicateDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+impl std::fmt::Debug for crate::VariableDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", &self.name)
+	}
+}
+
+impl std::fmt::Display for crate::VariableDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+struct TermDisplay<'term>
+{
+	parent_precedence: Option<i32>,
+	term: &'term crate::Term,
+}
+
+fn display_term<'term>(term: &'term crate::Term, parent_precedence: Option<i32>)
+	-> TermDisplay<'term>
+{
+	TermDisplay
+	{
+		parent_precedence,
+		term,
+	}
+}
+
+impl<'term> std::fmt::Debug for TermDisplay<'term>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let precedence = self.term.precedence();
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match &self.term
+		{
+			crate::Term::Boolean(true) => write!(format, "true"),
+			crate::Term::Boolean(false) => write!(format, "false"),
+			crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
+			crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
+			crate::Term::Integer(value) => write!(format, "{}", value),
+			crate::Term::String(value) => write!(format, "\"{}\"", value),
+			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
+			crate::Term::Function(function) =>
+			{
+				write!(format, "{}", function.declaration.name)?;
+
+				assert!(function.declaration.arity == function.arguments.len(),
+					"number of function arguments differs from declaration (expected {}, got {})",
+					function.declaration.arity, function.arguments.len());
+
+				if function.arguments.len() > 0
+				{
+					write!(format, "{}(", function.declaration.name)?;
+
+					let mut separator = "";
+
+					for argument in &function.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(&argument, None))?;
+
+						separator = ", ";
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
+				=> write!(format, "{:?} + {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
+				=> write!(format, "{:?} - {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
+				=> write!(format, "{:?} * {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
+				=> write!(format, "{:?} / {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
+				=> write!(format, "{:?} % {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
+				=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
+				=> write!(format, "-{:?}", display_term(argument, precedence)),
+			crate::Term::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
+				=> write!(format, "|{:?}|", display_term(argument, precedence)),
+		}?;
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'term> std::fmt::Display for TermDisplay<'term>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+struct FormulaDisplay<'formula>
+{
+	parent_precedence: Option<i32>,
+	formula: &'formula crate::Formula,
+}
+
+fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: Option<i32>)
+	-> FormulaDisplay<'formula>
+{
+	FormulaDisplay
+	{
+		parent_precedence,
+		formula,
+	}
+}
+
+impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let precedence = self.formula.precedence();
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match &self.formula
+		{
+			crate::Formula::Exists(exists) =>
+			{
+				assert!(!exists.parameters.is_empty());
+
+				write!(format, "exists")?;
+
+				let mut separator = " ";
+
+				for parameter in exists.parameters.iter()
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
+			},
+			crate::Formula::ForAll(for_all) =>
+			{
+				assert!(!for_all.parameters.is_empty());
+
+				write!(format, "forall")?;
+
+				let mut separator = " ";
+
+				for parameter in for_all.parameters.iter()
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
+			},
+			crate::Formula::Not(argument) => write!(format, "not {:?}",
+				display_formula(argument, precedence))?,
+			crate::Formula::And(arguments) =>
+			{
+				let mut separator = "";
+
+				assert!(!arguments.is_empty());
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+
+					separator = " and "
+				}
+			},
+			crate::Formula::Or(arguments) =>
+			{
+				let mut separator = "";
+
+				assert!(!arguments.is_empty());
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+
+					separator = " or "
+				}
+			},
+			crate::Formula::Implies(crate::Implies{antecedent, implication})
+				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
+					display_formula(implication, precedence))?,
+			crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
+				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
+					display_formula(right, precedence))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
+				=> write!(format, "{:?} < {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
+				=> write!(format, "{:?} <= {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
+				=> write!(format, "{:?} > {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
+				=> write!(format, "{:?} >= {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
+				=> write!(format, "{:?} = {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
+				=> write!(format, "{:?} != {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Boolean(true) => write!(format, "#true")?,
+			crate::Formula::Boolean(false) => write!(format, "#false")?,
+			crate::Formula::Predicate(predicate) =>
+			{
+				write!(format, "{}", predicate.declaration.name)?;
+
+				if !predicate.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &predicate.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(argument, None))?;
+
+						separator = ", "
+					}
+
+					write!(format, ")")?;
+				}
+			},
+		}
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+impl std::fmt::Debug for crate::Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", display_formula(&self, None))
+	}
+}
+
+impl std::fmt::Display for crate::Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", display_formula(&self, None))
+	}
+}
+
+impl std::fmt::Debug for crate::Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", display_term(&self, None))
+	}
+}
+
+impl std::fmt::Display for crate::Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", display_term(&self, None))
+	}
+}
--- a/src/lib.rs
+++ b/src/lib.rs
@ -0,0 +1,4 @@
+mod ast;
+pub mod format;
+
+pub use ast::*;