Ca? nha` oi+, O? da^y co' ba'c na`o dda~ tu+`ng ddo.c lambda calculi cu?a o^ng Church thi` cho to^i bie^'t nhe'. Co' ba'c na`o dda~ tu+`ng su+? du.ng theorem prover Isabelle thi` cu~ng cho bie^'t luo^n. Ca?m o+n nhie^`u. Huong