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 
