% ------------------------------------------------------------------------- % "Luka 5" Problem for many-valued sentential calculus. % % The five axioms % % P(i(x,i(y,x))) # Axiom 1. % P(i(i(x,y),i(i(y,z),i(x,z)))) # Axiom 2. % P(i(i(i(x,y),y),i(i(y,x),x))) # Axiom 3. % P(i(i(i(x,y),i(y,x)),i(y,x))) # Axiom 4. % P(i(i(n(x),n(y)),i(y,x))) # Axiom 5. % % together with the inference rule condensed detachment are known to be a % complete system for the many-valued sentential calculus (page 144 of [1]). % % The problem is to show that Axiom 4 is dependent on the four remaining % axioms. % % This experiment uses hints to check a known proof consisting of 63 steps. % This is done by including the 63 steps as hints and by keeping a % generated clause if and only if it subsumes a hint. % % REFERENCES: % % [1] Lukasiewicz, J., "Investigations into the sentential calculus", % pp. 131-152 in Jan Lukasiewicz: Selected Works, ed. L. Borkowski, % North Holland Publishing, Amsterdam (1970). % % Contributed by Bob Veroff % ------------------------------------------------------------------------- % general processing set(hyper_res). set(sos_queue). assign(max_weight, 1). % keep nothing in general % hints assign(equiv_hint_wt, 1). set(keep_hint_subsumers). % printing clear(print_kept). list(usable). % condensed detachment -P(i(x,y)) | -P(x) | P(y). end_of_list. list(sos). % Thesis 18 (Scott) P(i(x,i(y,x))) # label("Axiom 1"). % Thesis 1 (Scott) P(i(i(x,y),i(i(y,z),i(x,z)))) # label("Axiom 2"). % Thesis 27 (Scott) P(i(i(i(x,y),y),i(i(y,x),x))) # label("Axiom 3"). % Thesis 49 (Scott) P(i(i(n(x),n(y)),i(y,x))) # label("Axiom 5"). end_of_list. list(passive). % Axiom 4 is not one of Scott's 71 theses. -P(i(i(i(cx,cy),i(cy,cx)),i(cy,cx))) | $ANS(Denial_Axiom4). end_of_list. list(hints). % 63 steps of the known proof P(i(x,i(y,i(z,y)))) # label("Step01"). P(i(i(i(i(x,y),i(z,y)),w),i(i(z,x),w))) # label("Step02"). P(i(x,i(i(y,z),i(i(z,w),i(y,w))))) # label("Step03"). P(i(i(i(x,y),z),i(y,z))) # label("Step04"). P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))) # label("Step05"). P(i(i(i(x,y),z),i(i(n(y),n(x)),z))) # label("Step06"). P(i(i(i(x,i(y,x)),z),z)) # label("Step07"). P(i(i(x,i(y,z)),i(i(w,y),i(x,i(w,z))))) # label("Step08"). P(i(i(x,y),i(i(i(x,z),w),i(i(y,z),w)))) # label("Step09"). P(i(i(i(i(x,y),i(i(y,z),i(x,z))),w),w)) # label("Step10"). P(i(n(x),i(x,y))) # label("Step11"). P(i(x,i(i(x,y),y))) # label("Step12"). P(i(i(i(x,i(y,x)),i(y,x)),i(i(i(x,y),y),x))) # label("Step13"). P(i(i(n(x),n(i(y,i(z,y)))),x)) # label("Step14"). P(i(i(n(x),n(i(i(y,z),i(i(z,w),i(y,w))))),x)) # label("Step15"). P(i(i(x,i(y,z)),i(x,i(i(z,w),i(y,w))))) # label("Step16"). P(i(i(x,y),i(n(y),i(x,z)))) # label("Step17"). P(i(i(i(x,y),z),i(n(x),z))) # label("Step18"). P(i(i(x,i(y,z)),i(y,i(x,z)))) # label("Step19"). P(i(i(x,y),i(i(i(y,x),x),y))) # label("Step20"). P(i(i(i(i(n(x),n(i(y,i(z,y)))),x),w),w)) # label("Step21"). P(i(x,i(i(y,z),i(i(x,y),z)))) # label("Step22"). P(i(i(i(n(x),i(y,z)),w),i(i(y,x),w))) # label("Step23"). P(i(n(n(x)),x)) # label("Step24"). P(i(i(x,y),i(i(z,x),i(z,y)))) # label("Step25"). P(i(i(x,i(n(y),n(i(z,i(w,z))))),i(x,y))) # label("Step26"). P(i(i(i(i(x,y),i(i(z,x),y)),w),i(z,w))) # label("Step27"). P(i(i(i(n(n(x)),y),z),i(i(x,y),z))) # label("Step28"). P(i(x,n(n(x)))) # label("Step29"). P(i(i(x,n(n(y))),i(x,y))) # label("Step30"). P(i(i(x,i(i(y,z),w)),i(x,i(z,w)))) # label("Step31"). P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))) # label("Step32"). P(i(i(n(x),y),i(n(y),x))) # label("Step33"). P(i(i(n(n(x)),y),i(x,y))) # label("Step34"). P(i(i(i(x,y),n(z)),i(z,x))) # label("Step35"). P(i(i(x,y),i(n(y),n(x)))) # label("Step36"). P(i(i(x,i(n(n(y)),z)),i(x,i(y,z)))) # label("Step37"). P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))) # label("Step38"). P(i(n(i(x,y)),n(y))) # label("Step39"). P(i(i(i(n(x),n(y)),z),i(i(y,x),z))) # label("Step40"). P(i(n(i(x,y)),n(i(i(y,z),n(x))))) # label("Step41"). P(i(i(i(x,y),i(z,w)),i(y,i(n(w),n(z))))) # label("Step42"). P(i(i(i(n(x),n(i(y,x))),n(i(y,x))),n(x))) # label("Step43"). P(i(i(x,i(i(n(y),n(z)),w)),i(x,i(i(z,y),w)))) # label("Step44"). P(i(i(i(n(x),n(y)),n(y)),i(i(x,y),n(x)))) # label("Step45"). P(i(i(x,n(i(y,z))),i(x,n(i(i(z,w),n(y)))))) # label("Step46"). P(i(i(x,i(i(n(y),n(i(z,y))),n(i(z,y)))),i(x,n(y)))) # label("Step47"). P(i(n(x),i(n(n(y)),n(i(y,x))))) # label("Step48"). P(i(i(i(i(x,y),y),n(i(x,y))),n(y))) # label("Step49"). P(i(n(x),i(y,n(i(y,x))))) # label("Step50"). P(i(i(x,i(i(i(y,z),z),n(i(y,z)))),i(x,n(z)))) # label("Step51"). P(i(i(i(n(x),i(y,n(i(y,x)))),z),z)) # label("Step52"). P(i(i(i(i(x,y),y),n(i(y,x))),n(x))) # label("Step53"). P(i(i(x,i(i(i(y,z),z),n(i(z,y)))),i(x,n(y)))) # label("Step54"). P(i(i(x,y),i(i(y,n(i(y,x))),n(x)))) # label("Step55"). P(i(i(i(x,n(i(x,y))),n(i(i(x,n(i(x,y))),n(y)))),n(n(y)))) # label("Step56"). P(i(i(i(x,n(i(x,y))),n(i(i(x,n(i(x,y))),n(y)))),y)) # label("Step57"). P(i(i(x,i(i(y,n(i(y,z))),n(i(i(y,n(i(y,z))),n(z))))),i(x,z))) # label("Step58"). P(i(i(i(x,n(i(x,y))),n(i(y,x))),y)) # label("Step59"). P(i(i(x,i(i(y,n(i(y,z))),n(i(z,y)))),i(x,z))) # label("Step60"). P(i(x,i(i(n(i(x,y)),n(i(y,x))),y))) # label("Step61"). P(i(x,i(i(i(y,x),i(x,y)),y))) # label("Step62"). P(i(i(i(x,y),i(y,x)),i(y,x))) # label("Step63"). end_of_list.