% problem-set/circuits/two.inverter.ver1.clauses % created : 08/28/86 % revised : 07/14/88 % description: % % The two inverter puzzle given in the text, "Automated % Reasoning" by Larry Wos et al.(page 186 - 219). % % To design a circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See pages 186 - 219 in the above mentioned text. -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4), and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4), or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6), not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3), not(x4),not(x5),not(x6),not(x7),not(x8))), makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4), not(x5),not(x6),not(x7),not(x8)),v))). -TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) | OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | OUTPUT(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8), addinv(v,invtab(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7), not(x8)))). OUTPUT(0,0,0,0,1,1,1,1,x). OUTPUT(0,0,1,1,0,0,1,1,x). OUTPUT(0,1,0,1,0,1,0,1,x). -OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v). Equal(and(x,0),0). Equal(and(x,1),x). Equal(or(x,0),x). Equal(or(x,1),1). Equal(not(0),1). Equal(not(1),0). % list handling Equal(addinv(l(x,y),z),l(x,addinv(y,z))). Equal(addinv(x,y),l(y,x)). Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)), lr(possrev(R00m,x000,x001), lr(possrev(R01m,x010,x011), lr(possrev(R10m,x100,x101), lr(possrev(R11m,x110,x111), lr(possrev(R0m0,x000,x010), lr(possrev(R0m1,x001,x011), lr(possrev(R1m0,x100,x110), lr(possrev(R1m1,x101,x111), lr(possrev(Rm00,x000,x100), lr(possrev(Rm01,x001,x101), lr(possrev(Rm10,x010,x110), lr(possrev(Rm11,x011,x111), makerevlist(v)))))))))))))). Equal(makerevlist(v),end). Equal(possrev(xname,1,0),xname). Equal(possrev(xname,0,1),notrev). Equal(possrev(xname,x,x),notrev). Equal(lr(notrev,x),x). Equal(lr(x,lr(y,z)),lr(y,lr(x,z))). Equal(lr(x,lr(x,y)),lr(x,y)).