Abstract: The time complexity of the SAT-based approach for solving Einstein's riddle is very high. Aiming to this problem, we constructed a formal system called Γ. At first, we described the riddle with a set of axioms and a set of rules in Γ. And then, we used the axioms and rules in Γ to prove some theorems in Γ. So, a solution to the riddle was obtwined. Compared with the existing approach, the new method gives a deduction-based procedure to solve the riddle. And the state explosion problem is avoided.

Key words: Einstein's riddle,Formwl system,Formal deduction