diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index d27cd13..859e976 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -1,10 +1,12 @@
 package inference;
 
+import java.util.Collection;
 import java.util.List;
 
 import models.algebra.Variable;
 import models.formulas.meta.MetaDependencyFormula;
 import models.formulas.meta.MetaEquationFormula;
+import models.terms.RDLTerm;
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResourceVariable;
@@ -28,12 +30,68 @@
 	
 	private final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", 
 			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))),
-			new MetaDependencyFormula(new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))))
+			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))
 	);
 	
+	private final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", 
+			List.of(
+					new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))),
+					new MetaDependencyFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))
+			),
+			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("w")))
+	);
 	
-	public ProofSystem() {
+	private final static InferenceRule LEFT_PROJECTION = null;
+	private final static InferenceRule RIGHT_PROJECTION = null;
+	private final static InferenceRule CONSTANT_MAPPING = null; // 定値写像??
+	private final static InferenceRule ORDER_DESCENTING = null; // 階数降下??
+	
+	private final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement",
+			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					),
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaEvaluatableTermVariable(new Variable("ue"))
+					)
+			)
+	);
+	
+	private final static InferenceRule IDENTITY_LAW = null;
+	
+	private final static InferenceRule JOIN = new InferenceRule("join",
+			List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaRDLTerm(
+									new MetaResourceVariable(new Variable("w")),
+									new MetaResourceVariable(new Variable("x")),
+									new MetaEvaluatableTermVariable(new Variable("te"))
+							)
+					),
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("x")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					)
+			)
+	);
+	
+	private final static InferenceRule CONSTANT_VALUE_LAW = null;//定値性??
+	private final static InferenceRule LINEAR_RIGHT_NORMALIZE = null;
+	private final static InferenceRule PSEUDO_IDENTITY_LAW = null;//疑似恒等性??
+	private final static InferenceRule SET_EQUIVALENCE = null;//集合同値性??
+	private final static InferenceRule HOMOMORPHISM = null;//準同型性??
+	
+	public static boolean check(Collection<RDLTerm> assumptions, RDLTerm conclusion) {
+		return false;
 	}
 	
-	
 }
diff --git a/src/models/formulas/meta/MetaDependencyFormula.java b/src/models/formulas/meta/MetaDependencyFormula.java
index f3dcf08..35bae69 100644
--- a/src/models/formulas/meta/MetaDependencyFormula.java
+++ b/src/models/formulas/meta/MetaDependencyFormula.java
@@ -9,6 +9,7 @@
 import models.formulas.Formula;
 import models.terms.RDLTerm;
 import models.terms.meta.MetaRDLTerm;
+import models.terms.meta.MetaResourceVariable;
 import models.terms.meta.OrderVariableConstraint;
 
 @Getter
@@ -23,6 +24,10 @@
 		this.dependency = term;
 	}
 	
+	public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaResourceVariable dependedVariable) {
+		this.dependency = new MetaRDLTerm(dependingTerm, dependedVariable);
+	}
+	
 	@Override
 	public boolean isMatchedBy(Formula formula, Map<Variable, RDLTerm> binding,
 			Map<Variable, OrderVariableConstraint> orderConstraint) {