diff --git a/src/syntax_tree/asp.rs b/src/syntax_tree/asp.rs
index 04fe964f..882857c3 100644
--- a/src/syntax_tree/asp.rs
+++ b/src/syntax_tree/asp.rs
@@ -1,14 +1,17 @@
-use crate::{
-    formatting::asp::default::Format,
-    parsing::asp::pest::{
-        AtomParser, AtomicFormulaParser, BinaryOperatorParser, BodyParser, ComparisonParser,
-        HeadParser, LiteralParser, PrecomputedTermParser, ProgramParser, RelationParser,
-        RuleParser, SignParser, TermParser, UnaryOperatorParser, VariableParser,
+use {
+    crate::{
+        formatting::asp::default::Format,
+        parsing::asp::pest::{
+            AtomParser, AtomicFormulaParser, BinaryOperatorParser, BodyParser, ComparisonParser,
+            HeadParser, LiteralParser, PrecomputedTermParser, ProgramParser, RelationParser,
+            RuleParser, SignParser, TermParser, UnaryOperatorParser, VariableParser,
+        },
+        syntax_tree::{impl_node, Node},
     },
-    syntax_tree::{impl_node, Node},
+    std::collections::HashSet,
 };
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum PrecomputedTerm {
     Infimum,
     Numeral(isize),
@@ -18,19 +21,19 @@ pub enum PrecomputedTerm {
 
 impl_node!(PrecomputedTerm, Format, PrecomputedTermParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Variable(pub String);
 
 impl_node!(Variable, Format, VariableParser);
 
-#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
 pub enum UnaryOperator {
     Negative,
 }
 
 impl_node!(UnaryOperator, Format, UnaryOperatorParser);
 
-#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)]
 pub enum BinaryOperator {
     Add,
     Subtract,
@@ -42,7 +45,7 @@ pub enum BinaryOperator {
 
 impl_node!(BinaryOperator, Format, BinaryOperatorParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Term {
     PrecomputedTerm(PrecomputedTerm),
     Variable(Variable),
@@ -59,7 +62,22 @@ pub enum Term {
 
 impl_node!(Term, Format, TermParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Term {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            Term::PrecomputedTerm(_) => HashSet::new(),
+            Term::Variable(v) => HashSet::from([v.clone()]),
+            Term::UnaryOperation { arg, .. } => arg.variables(),
+            Term::BinaryOperation { lhs, rhs, .. } => {
+                let mut vars = lhs.variables();
+                vars.extend(rhs.variables());
+                vars
+            }
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Atom {
     pub predicate: String,
     pub terms: Vec<Term>,
@@ -67,7 +85,17 @@ pub struct Atom {
 
 impl_node!(Atom, Format, AtomParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Atom {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = HashSet::new();
+        for term in self.terms.iter() {
+            vars.extend(term.variables())
+        }
+        vars
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Sign {
     NoSign,
     Negation,
@@ -76,7 +104,7 @@ pub enum Sign {
 
 impl_node!(Sign, Format, SignParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Literal {
     pub sign: Sign,
     pub atom: Atom,
@@ -84,7 +112,13 @@ pub struct Literal {
 
 impl_node!(Literal, Format, LiteralParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Literal {
+    pub fn variables(&self) -> HashSet<Variable> {
+        self.atom.variables()
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Relation {
     Equal,
     NotEqual,
@@ -96,7 +130,7 @@ pub enum Relation {
 
 impl_node!(Relation, Format, RelationParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Comparison {
     pub relation: Relation,
     pub lhs: Term,
@@ -105,7 +139,15 @@ pub struct Comparison {
 
 impl_node!(Comparison, Format, ComparisonParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Comparison {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = self.lhs.variables();
+        vars.extend(self.rhs.variables());
+        vars
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum AtomicFormula {
     Literal(Literal),
     Comparison(Comparison),
@@ -113,7 +155,16 @@ pub enum AtomicFormula {
 
 impl_node!(AtomicFormula, Format, AtomicFormulaParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl AtomicFormula {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            AtomicFormula::Literal(l) => l.variables(),
+            AtomicFormula::Comparison(c) => c.variables(),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Head {
     Basic(Atom),
     Choice(Atom),
@@ -122,14 +173,57 @@ pub enum Head {
 
 impl_node!(Head, Format, HeadParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Head {
+    pub fn predicate(&self) -> Option<&str> {
+        match self {
+            Head::Basic(a) => Some(&a.predicate),
+            Head::Choice(a) => Some(&a.predicate),
+            Head::Falsity => None,
+        }
+    }
+
+    pub fn terms(&self) -> Option<&[Term]> {
+        match self {
+            Head::Basic(a) => Some(&a.terms),
+            Head::Choice(a) => Some(&a.terms),
+            Head::Falsity => None,
+        }
+    }
+
+    pub fn arity(&self) -> usize {
+        match self {
+            Head::Basic(a) => a.terms.len(),
+            Head::Choice(a) => a.terms.len(),
+            Head::Falsity => 0,
+        }
+    }
+
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            Head::Basic(a) | Head::Choice(a) => a.variables(),
+            Head::Falsity => HashSet::new(),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Body {
     pub formulas: Vec<AtomicFormula>,
 }
 
 impl_node!(Body, Format, BodyParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Body {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = HashSet::new();
+        for formula in self.formulas.iter() {
+            vars.extend(formula.variables())
+        }
+        vars
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Rule {
     pub head: Head,
     pub body: Body,
@@ -137,9 +231,27 @@ pub struct Rule {
 
 impl_node!(Rule, Format, RuleParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Rule {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = self.head.variables();
+        vars.extend(self.body.variables());
+        vars
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Program {
     pub rules: Vec<Rule>,
 }
 
 impl_node!(Program, Format, ProgramParser);
+
+impl Program {
+    pub fn variables(&self) -> HashSet<Variable> {
+        let mut vars = HashSet::new();
+        for rule in self.rules.iter() {
+            vars.extend(rule.variables())
+        }
+        vars
+    }
+}
diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs
index fb12920b..dc805d41 100644
--- a/src/syntax_tree/fol.rs
+++ b/src/syntax_tree/fol.rs
@@ -1,15 +1,18 @@
-use crate::{
-    formatting::fol::default::Format,
-    parsing::fol::pest::{
-        AtomParser, AtomicFormulaParser, BasicIntegerTermParser, BinaryConnectiveParser,
-        BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser,
-        IntegerTermParser, QuantificationParser, QuantifierParser, RelationParser, TheoryParser,
-        UnaryConnectiveParser, UnaryOperatorParser, VariableParser,
+use {
+    crate::{
+        formatting::fol::default::Format,
+        parsing::fol::pest::{
+            AtomParser, AtomicFormulaParser, BasicIntegerTermParser, BinaryConnectiveParser,
+            BinaryOperatorParser, ComparisonParser, FormulaParser, GeneralTermParser, GuardParser,
+            IntegerTermParser, QuantificationParser, QuantifierParser, RelationParser,
+            TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, VariableParser,
+        },
+        syntax_tree::{impl_node, Node},
     },
-    syntax_tree::{impl_node, Node},
+    std::{collections::HashSet, hash::Hash},
 };
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum BasicIntegerTerm {
     Infimum,
     Supremum,
@@ -19,14 +22,26 @@ pub enum BasicIntegerTerm {
 
 impl_node!(BasicIntegerTerm, Format, BasicIntegerTermParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl BasicIntegerTerm {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            BasicIntegerTerm::IntegerVariable(v) => HashSet::from([Variable {
+                name: v.to_string(),
+                sort: Sort::Integer,
+            }]),
+            _ => HashSet::new(),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum UnaryOperator {
     Negative,
 }
 
 impl_node!(UnaryOperator, Format, UnaryOperatorParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum BinaryOperator {
     Add,
     Subtract,
@@ -35,7 +50,7 @@ pub enum BinaryOperator {
 
 impl_node!(BinaryOperator, Format, BinaryOperatorParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum IntegerTerm {
     BasicIntegerTerm(BasicIntegerTerm),
     UnaryOperation {
@@ -51,7 +66,21 @@ pub enum IntegerTerm {
 
 impl_node!(IntegerTerm, Format, IntegerTermParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl IntegerTerm {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            IntegerTerm::BasicIntegerTerm(t) => t.variables(),
+            IntegerTerm::UnaryOperation { arg: t, .. } => t.variables(),
+            IntegerTerm::BinaryOperation { lhs, rhs, .. } => {
+                let mut vars = lhs.variables();
+                vars.extend(rhs.variables());
+                vars
+            }
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum GeneralTerm {
     Symbol(String),
     GeneralVariable(String),
@@ -60,7 +89,20 @@ pub enum GeneralTerm {
 
 impl_node!(GeneralTerm, Format, GeneralTermParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl GeneralTerm {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            GeneralTerm::Symbol(_) => HashSet::new(),
+            GeneralTerm::GeneralVariable(v) => HashSet::from([Variable {
+                name: v.to_string(),
+                sort: Sort::General,
+            }]),
+            GeneralTerm::IntegerTerm(t) => t.variables(),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Atom {
     pub predicate: String,
     pub terms: Vec<GeneralTerm>,
@@ -68,7 +110,7 @@ pub struct Atom {
 
 impl_node!(Atom, Format, AtomParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Relation {
     Equal,
     NotEqual,
@@ -80,7 +122,7 @@ pub enum Relation {
 
 impl_node!(Relation, Format, RelationParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Guard {
     pub relation: Relation,
     pub term: GeneralTerm,
@@ -88,7 +130,13 @@ pub struct Guard {
 
 impl_node!(Guard, Format, GuardParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Guard {
+    pub fn variables(&self) -> HashSet<Variable> {
+        self.term.variables()
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Comparison {
     pub term: GeneralTerm,
     pub guards: Vec<Guard>,
@@ -96,7 +144,7 @@ pub struct Comparison {
 
 impl_node!(Comparison, Format, ComparisonParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum AtomicFormula {
     Truth,
     Falsity,
@@ -106,14 +154,36 @@ pub enum AtomicFormula {
 
 impl_node!(AtomicFormula, Format, AtomicFormulaParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl AtomicFormula {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            AtomicFormula::Falsity | AtomicFormula::Truth => HashSet::new(),
+            AtomicFormula::Atom(a) => {
+                let mut vars = HashSet::new();
+                for t in a.terms.iter() {
+                    vars.extend(t.variables());
+                }
+                vars
+            }
+            AtomicFormula::Comparison(c) => {
+                let mut vars = c.term.variables();
+                for guard in c.guards.iter() {
+                    vars.extend(guard.variables())
+                }
+                vars
+            }
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum UnaryConnective {
     Negation,
 }
 
 impl_node!(UnaryConnective, Format, UnaryConnectiveParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Quantifier {
     Forall,
     Exists,
@@ -121,7 +191,7 @@ pub enum Quantifier {
 
 impl_node!(Quantifier, Format, QuantifierParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Quantification {
     pub quantifier: Quantifier,
     pub variables: Vec<Variable>,
@@ -129,7 +199,7 @@ pub struct Quantification {
 
 impl_node!(Quantification, Format, QuantificationParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
 pub enum Sort {
     Integer,
     General,
@@ -137,7 +207,7 @@ pub enum Sort {
 
 // TODO: Should Sort be a Node?
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
 pub struct Variable {
     pub name: String,
     pub sort: Sort,
@@ -145,7 +215,7 @@ pub struct Variable {
 
 impl_node!(Variable, Format, VariableParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum BinaryConnective {
     Conjunction,
     Disjunction,
@@ -156,7 +226,7 @@ pub enum BinaryConnective {
 
 impl_node!(BinaryConnective, Format, BinaryConnectiveParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub enum Formula {
     AtomicFormula(AtomicFormula),
     UnaryFormula {
@@ -176,7 +246,22 @@ pub enum Formula {
 
 impl_node!(Formula, Format, FormulaParser);
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+impl Formula {
+    pub fn variables(&self) -> HashSet<Variable> {
+        match &self {
+            Formula::AtomicFormula(f) => f.variables(),
+            Formula::UnaryFormula { formula, .. } => formula.variables(),
+            Formula::BinaryFormula { lhs, rhs, .. } => {
+                let mut vars = lhs.variables();
+                vars.extend(rhs.variables());
+                vars
+            }
+            Formula::QuantifiedFormula { formula, .. } => formula.variables(),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Eq, PartialEq, Hash)]
 pub struct Theory {
     pub formulas: Vec<Formula>,
 }
diff --git a/src/syntax_tree/mod.rs b/src/syntax_tree/mod.rs
index bf3bfd80..5a6e3659 100644
--- a/src/syntax_tree/mod.rs
+++ b/src/syntax_tree/mod.rs
@@ -1,12 +1,13 @@
 use std::{
     fmt::{Debug, Display},
+    hash::Hash,
     str::FromStr,
 };
 
 pub mod asp;
 pub mod fol;
 
-pub trait Node: Clone + Debug + Eq + PartialEq + FromStr + Display {}
+pub trait Node: Clone + Debug + Eq + PartialEq + FromStr + Display + Hash {}
 
 macro_rules! impl_node {
     ($node:ty, $format:expr, $parser:ty) => {