problem-set/circuits/two.inverter.val.desc created : 09/03/86 revised : 07/15/88 Natural Language Description: The files beginning with two_inverter_val concern the validation of a solution to the two_inverter_val given in the text, "Automated Reasoning" by Larry Wos et al. (chapter 7). The puzzle involves 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 specifications: o1 = not(i1) o2 = not(i2) o3 = not(i3) where, o1, o2, o3 are the outputs and i1, i2, i3 are the related inputs. Versions: two_inverter_val.ver1 - Nonequality based axioms are used, forward demodulation is the inference rule, and demodulators are included. created by: E. Lusk verified for ITP: no proof translated for OTTER by: SLM verified for OTTER: 07/15/88