CS代考计算机代写 HW 14: Visual Inference Rules (a)

HW 14: Visual Inference Rules (a)
CS 582, Winter 2021
NR(m) NR(m′) NR(m;m′)
NR(up)
NR(m) NR(rev(m))
Note: For entering inference rules into Canvas, you may use the following alternative, linear notation for rules, which employs & for connecting the premises and =⇒ for representing the horizontal rule separating the premises from the conclusion.
(b)
(c)
CU(up)
CU(m) CU(rev(m))
CU(m) CU(m;m′)
CU(m′) CU(m;m′)
NR(up)
NR(m) =⇒ NR(rev(m))
NR(m) & NR(m′) =⇒ NR(m;m′)
LU(up)
Note that including the following rule would be incorrect, since the last operation in the program
rev(up) is rev and not up.
LU(m) LU(rev(m))
Moreover, adding the premise LU(m) to the second rule would also be incorrect, since with that definition LU would not hold for rgt; up.
LU(m′) LU(m;m′)