diff --git a/src/models/formulas/DependencyFormula.java b/src/models/formulas/DependencyFormula.java
new file mode 100644
index 0000000..480d17d
--- /dev/null
+++ b/src/models/formulas/DependencyFormula.java
@@ -0,0 +1,35 @@
+package models.formulas;
+
+import lombok.Getter;
+import models.terms.Dependency;
+
+@Getter
+public class DependencyFormula extends Formula {
+	
+	private Dependency dependency;
+	
+	public DependencyFormula(Dependency dependency) {
+		this.dependency = dependency;
+	}
+
+	
+	@Override
+	public String toString() {
+		return dependency.toString();
+	}
+
+	@Override
+	public boolean equals(Object another) {
+		if(! (another instanceof DependencyFormula)) {
+			return false;
+		}
+		DependencyFormula anotherFormula = (DependencyFormula) another;
+		return dependency.equals(anotherFormula.getDependency());
+	}
+
+	@Override
+	public int hashCode() {
+		return ("DF" + toString()).hashCode();
+	}
+	
+}
diff --git a/src/models/formulas/EquationFormula.java b/src/models/formulas/EquationFormula.java
new file mode 100644
index 0000000..3fa8cf8
--- /dev/null
+++ b/src/models/formulas/EquationFormula.java
@@ -0,0 +1,37 @@
+package models.formulas;
+
+import lombok.Getter;
+import models.terms.RDLTerm;
+
+@Getter
+public class EquationFormula extends Formula {
+
+	private RDLTerm leftTerm;
+	private RDLTerm rightTerm;
+		
+	public EquationFormula(RDLTerm leftTerm, RDLTerm rightTerm) {
+		this.leftTerm = leftTerm;
+		this.rightTerm = rightTerm;
+	}
+
+	
+	@Override
+	public String toString() {
+		return leftTerm.toString() + " = " + rightTerm.toString();
+	}
+
+	@Override
+	public boolean equals(Object another) {
+		if (! (another instanceof EquationFormula)) {
+			return false;
+		}
+		EquationFormula anotherFormula = (EquationFormula) another;
+		return leftTerm.equals(anotherFormula.getLeftTerm()) && rightTerm.equals(anotherFormula.getRightTerm());
+	}
+
+	@Override
+	public int hashCode() {
+		return toString().hashCode();
+	}
+	
+}
diff --git a/src/models/formulas/Formula.java b/src/models/formulas/Formula.java
new file mode 100644
index 0000000..f1813f4
--- /dev/null
+++ b/src/models/formulas/Formula.java
@@ -0,0 +1,9 @@
+package models.formulas;
+
+public abstract class Formula {
+
+	public abstract String toString();
+	public abstract boolean equals(Object another);
+	public abstract int hashCode();
+	
+}
diff --git a/src/models/formulas/meta/MetaDependencyFormula.java b/src/models/formulas/meta/MetaDependencyFormula.java
new file mode 100644
index 0000000..cd6a12a
--- /dev/null
+++ b/src/models/formulas/meta/MetaDependencyFormula.java
@@ -0,0 +1,36 @@
+package models.formulas.meta;
+
+import java.util.Map;
+
+import exceptions.IllegalTypeException;
+import lombok.Getter;
+import models.algebra.Variable;
+import models.formulas.DependencyFormula;
+import models.formulas.Formula;
+import models.terms.RDLTerm;
+import models.terms.meta.MetaRDLTerm;
+import models.terms.meta.OrderVariableConstraint;
+
+@Getter
+public class MetaDependencyFormula extends MetaFormula {
+
+	private MetaRDLTerm dependency;
+	
+	public MetaDependencyFormula(MetaRDLTerm term) {
+		if (! term.isDependency()) {
+			throw new IllegalTypeException();
+		}
+		this.dependency = term;
+	}
+	
+	@Override
+	public boolean isMatchBy(Formula formula, Map<Variable, RDLTerm> binding,
+			Map<Variable, OrderVariableConstraint> orderConstraint) {
+		if (! (formula instanceof DependencyFormula)) {
+			return false;
+		}
+		DependencyFormula dep = (DependencyFormula) formula;
+		return dependency.isMatchedBy(dep.getDependency(), binding, orderConstraint);
+	}
+
+}
diff --git a/src/models/formulas/meta/MetaEquationFormula.java b/src/models/formulas/meta/MetaEquationFormula.java
new file mode 100644
index 0000000..ee29f66
--- /dev/null
+++ b/src/models/formulas/meta/MetaEquationFormula.java
@@ -0,0 +1,44 @@
+package models.formulas.meta;
+
+import java.util.Map;
+
+import exceptions.IllegalTypeException;
+import lombok.Getter;
+import models.algebra.Variable;
+import models.formulas.EquationFormula;
+import models.formulas.Formula;
+import models.terms.RDLTerm;
+import models.terms.meta.MetaRDLTerm;
+import models.terms.meta.OrderVariableConstraint;
+
+@Getter
+public class MetaEquationFormula extends MetaFormula {
+
+	private MetaRDLTerm leftTerm;
+	private MetaRDLTerm rightTerm;
+	
+	public MetaEquationFormula(MetaRDLTerm left, MetaRDLTerm right) {
+		if (! left.isEvaluatableTerm()) {
+			throw new IllegalTypeException();
+		}
+		if (! right.isEvaluatableTerm()) {
+			throw new IllegalTypeException();
+		}
+		
+		this.leftTerm = left;
+		this.rightTerm = right;
+	}
+	
+	@Override
+	public boolean isMatchBy(Formula formula, Map<Variable, RDLTerm> binding,
+			Map<Variable, OrderVariableConstraint> orderConstraint) {
+		if (! (formula instanceof EquationFormula)) {
+			return false;
+		}
+		EquationFormula eq = (EquationFormula) formula;
+		return leftTerm.isMatchedBy(eq.getLeftTerm(), binding, orderConstraint) && rightTerm.isMatchedBy(rightTerm, binding, orderConstraint);
+	}
+	
+	
+	
+}
diff --git a/src/models/formulas/meta/MetaFormula.java b/src/models/formulas/meta/MetaFormula.java
new file mode 100644
index 0000000..7dece26
--- /dev/null
+++ b/src/models/formulas/meta/MetaFormula.java
@@ -0,0 +1,19 @@
+package models.formulas.meta;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import models.algebra.Variable;
+import models.formulas.Formula;
+import models.terms.RDLTerm;
+import models.terms.meta.OrderVariableConstraint;
+
+public abstract class MetaFormula {
+
+	public boolean isMatchBy(Formula formula) {
+		return isMatchBy(formula, new HashMap<>(), new HashMap<>());
+	}
+	
+	public abstract boolean isMatchBy(Formula formula, Map<Variable, RDLTerm> binding, Map<Variable, OrderVariableConstraint> orderConstraint);
+	
+}