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..e12dc46
--- /dev/null
+++ b/src/models/formulas/EquationFormula.java
@@ -0,0 +1,37 @@
+package models.formulas;
+
+import lombok.Getter;
+import models.terms.EvaluatableTerm;
+
+@Getter
+public class EquationFormula extends Formula {
+
+	private EvaluatableTerm leftSideHand;
+	private EvaluatableTerm rightSideHand;
+		
+	public EquationFormula(EvaluatableTerm leftTerm, EvaluatableTerm rightTerm) {
+		this.leftSideHand = leftTerm;
+		this.rightSideHand = rightTerm;
+	}
+
+	
+	@Override
+	public String toString() {
+		return leftSideHand.toString() + " = " + rightSideHand.toString();
+	}
+
+	@Override
+	public boolean equals(Object another) {
+		if (! (another instanceof EquationFormula)) {
+			return false;
+		}
+		EquationFormula anotherFormula = (EquationFormula) another;
+		return leftSideHand.equals(anotherFormula.getLeftSideHand()) && rightSideHand.equals(anotherFormula.getRightSideHand());
+	}
+
+	@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..b6fdd67
--- /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 isMatchedBy(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..e1ccf2f
--- /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 leftSideHand;
+	private MetaRDLTerm rightSideHand;
+	
+	public MetaEquationFormula(MetaRDLTerm left, MetaRDLTerm right) {
+		if (! left.isEvaluatableTerm()) {
+			throw new IllegalTypeException();
+		}
+		if (! right.isEvaluatableTerm()) {
+			throw new IllegalTypeException();
+		}
+		
+		this.leftSideHand = left;
+		this.rightSideHand = right;
+	}
+	
+	@Override
+	public boolean isMatchedBy(Formula formula, Map<Variable, RDLTerm> binding,
+			Map<Variable, OrderVariableConstraint> orderConstraint) {
+		if (! (formula instanceof EquationFormula)) {
+			return false;
+		}
+		EquationFormula eq = (EquationFormula) formula;
+		return leftSideHand.isMatchedBy(eq.getLeftSideHand(), binding, orderConstraint) && rightSideHand.isMatchedBy(eq.getRightSideHand(), binding, orderConstraint);
+	}
+	
+	
+	
+}
diff --git a/src/models/formulas/meta/MetaFormula.java b/src/models/formulas/meta/MetaFormula.java
new file mode 100644
index 0000000..f21e2f8
--- /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 isMatchedBy(Formula formula) {
+		return isMatchedBy(formula, new HashMap<>(), new HashMap<>());
+	}
+	
+	public abstract boolean isMatchedBy(Formula formula, Map<Variable, RDLTerm> binding, Map<Variable, OrderVariableConstraint> orderConstraint);
+	
+}
diff --git a/src/tests/formulas/meta/MetaEquationFormulaTest.java b/src/tests/formulas/meta/MetaEquationFormulaTest.java
new file mode 100644
index 0000000..561ab6b
--- /dev/null
+++ b/src/tests/formulas/meta/MetaEquationFormulaTest.java
@@ -0,0 +1,67 @@
+package tests.formulas.meta;
+
+import static org.junit.jupiter.api.Assertions.*;
+import static tests.Utils.*;
+
+import org.junit.jupiter.api.Test;
+
+import models.algebra.Variable;
+import models.formulas.DependencyFormula;
+import models.formulas.EquationFormula;
+import models.formulas.meta.MetaDependencyFormula;
+import models.formulas.meta.MetaEquationFormula;
+import models.terms.Dependency;
+import models.terms.DependencyTerm;
+import models.terms.EvaluatableTerm;
+import models.terms.ResourceVariable;
+import models.terms.meta.MetaEvaluatableTermVariable;
+import models.terms.meta.MetaRDLTerm;
+import models.terms.meta.MetaResourceVariable;
+
+public class MetaEquationFormulaTest {
+
+	@Test
+	void MetaEquationFormulaMatchingTest() {
+		
+		ResourceVariable a = new ResourceVariable("a", INT, 0);
+		ResourceVariable b = new ResourceVariable("b", INT, 0);
+		ResourceVariable c = new ResourceVariable("c", INT, 0);
+		ResourceVariable d = new ResourceVariable("d", INT, 0);
+		EvaluatableTerm te1 = new DependencyTerm(a, b, c);
+		EvaluatableTerm te2 = new DependencyTerm(a, b, d);
+		EquationFormula formula = new EquationFormula(te1, te2);
+		
+		
+		MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"));
+		MetaResourceVariable v = new MetaResourceVariable(new Variable("v"));
+		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
+		MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue"));
+		MetaRDLTerm left = new MetaRDLTerm(se, v, te);
+		MetaRDLTerm right = new MetaRDLTerm(se, v, ue);
+		MetaEquationFormula metaFormula = new MetaEquationFormula(left, right);
+		
+		// [a : b -> c] = [a : b -> d] matches [se : v -> te] = [se : v -> ue]
+		assertTrue(metaFormula.isMatchedBy(formula));
+		
+	}
+	
+	@Test
+	void MetaDependencyFormulaMatchingTest() {
+		ResourceVariable a = new ResourceVariable("a", INT, 0);
+		ResourceVariable b = new ResourceVariable("b", INT, 0);
+		ResourceVariable c = new ResourceVariable("c", INT, 0);
+		EvaluatableTerm te1 = new DependencyTerm(a, b, c);
+		ResourceVariable d = new ResourceVariable("d", INT, 0);
+		Dependency d1 = new Dependency(te1, d);
+		DependencyFormula depF = new DependencyFormula(d1);
+		
+		MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te"));
+		MetaResourceVariable w = new MetaResourceVariable(new Variable("w"));
+		MetaRDLTerm dep = new MetaRDLTerm(te, w);
+		MetaDependencyFormula metaDepF = new MetaDependencyFormula(dep);
+		
+		//[a : b -> c] : d matches te : w
+		assertTrue(metaDepF.isMatchedBy(depF));
+	}
+	
+}