% Basic OTTER input file for reasoning about Intepretability logics
% For further OTTER options, see McCune's user manual (or Kalman's text)
%
%    http://www-unix.mcs.anl.gov/AR/otter/
%
% Remove "%" symbol from front of line to activate it (uncomment it)
% 
% Example OTTER input: "otter < hilbert_otter.txt" runs this file.  
% All OTTER options are set within the input file (see McCune's manual).
% 
% In this case, the proofs are not easy, and require strategies and 
% Otter options and parameter srttings.  I have also included hints
% which encode lots of useful PL theorems, to help the search.
% It would be nice to have further rewrite rules in the demodulator
% list, in order to simplify and canonicalize formulas in the search.

% Otter parameter and strategy settings (pretty good setting for these,
% but see the OTTER manual or Kalman's book for usage and strategy).
set(hyper_res).                
assign(max_weight, 24).        
assign(max_distinct_vars, 5).  
assign(pick_given_ratio, 3).   
assign(max_proofs, 1).         
clear(print_kept).             
clear(print_new_demod).        
clear(print_back_demod).       
clear(print_back_sub).          
set(order_history).
set(input_sos_first).
assign(max_mem, 200000).      
assign(bsub_hint_wt, 1).       
set(keep_hint_subsumers).      

list(hints).
% Classical PL theorems of Lukasiewicz
P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))).
P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))).
P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))).
P(i(i(x,y),i(i(z,x),i(i(y,u),i(z,u))))).
P(i(i(i(n(x),y),z),i(x,z))).
P(i(x,i(i(i(n(x),x),x),i(i(y,x),x)))).
P(i(i(x,i(i(n(y),y),y)),i(i(n(y),y),y))).
P(i(x,i(i(n(y),y),y))).
P(i(i(n(x),y),i(z,i(i(y,x),x)))).
P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))).
P(i(i(n(x),y),i(i(y,x),x))).
P(i(x,x)).
P(i(x,i(i(y,x),x))).
P(i(x,i(y,x))).
P(i(i(i(x,y),z),i(y,z))).
P(i(x,i(i(x,y),y))).
P(i(i(x,i(y,z)),i(y,i(x,z)))).
P(i(i(x,y),i(i(z,x),i(z,y)))).
P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))).
P(i(i(i(x,y),x),x)).
P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))).
P(i(i(i(x,y),z),i(i(z,x),x))).
P(i(i(i(x,y),y),i(i(y,x),x))).
P(i(i(i(i(x,y),y),z),i(i(i(y,u),x),z))).
P(i(i(i(x,y),z),i(i(x,z),z))).
P(i(i(x,i(x,y)),i(x,y))).
P(i(i(x,y),i(i(i(x,z),u),i(i(y,u),u)))).
P(i(i(i(x,y),z),i(i(x,u),i(i(u,z),z)))).
P(i(i(x,y),i(i(y,i(z,i(x,u))),i(z,i(x,u))))).
P(i(i(x,i(y,i(z,u))),i(i(z,x),i(y,i(z,u))))).
P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).
P(i(n(x),i(x,y))).
P(i(i(i(x,y),z),i(n(x),z))).
P(i(i(x,n(x)),n(x))).
P(i(n(n(x)),x)).
P(i(x,n(n(x)))).
P(i(i(x,y),i(n(n(x)),y))).
P(i(i(i(n(n(x)),y),z),i(i(x,y),z))).
P(i(i(x,y),i(i(y,n(x)),n(x)))).
P(i(i(x,i(y,n(z))),i(i(z,y),i(x,n(z))))).
P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))).
P(i(i(x,y),i(n(y),n(x)))).
P(i(i(x,n(y)),i(y,n(x)))).
P(i(i(n(x),y),i(n(y),x))).
P(i(i(n(x),n(y)),i(y,x))).
P(i(i(i(n(x),y),z),i(i(n(y),x),z))).
P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))).
P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))).
P(i(i(n(x),y),i(i(x,y),y))).
P(i(i(x,y),i(i(n(x),y),y))).
P(i(i(x,y),i(i(x,n(y)),n(x)))).
P(i(i(i(i(x,y),y),z),i(i(n(x),y),z))).
P(i(i(n(x),y),i(i(x,z),i(i(z,y),y)))).
P(i(i(i(i(x,y),i(i(y,z),z)),u),i(i(n(x),z),u))).
P(i(i(n(x),y),i(i(z,y),i(i(x,z),y)))).
P(i(i(x,i(n(y),z)),i(x,i(i(u,z),i(i(y,u),z))))).
P(i(i(x,y),i(i(z,y),i(i(n(x),z),y)))).
P(i(i(n(n(x)),y),i(x,y))).
P(i(x,i(y,y))).
P(i(n(i(x,x)),y)).
P(i(i(n(x),n(i(y,y))),x)).
P(i(n(i(x,y)),x)).
P(i(n(i(x,y)),n(y))).
P(i(n(i(x,n(y))),y)).
P(i(x,i(n(y),n(i(x,y))))).
P(i(x,i(y,n(i(x,n(y)))))).
P(n(i(i(x,x),n(i(y,y))))).
end_of_list.

weight_list(pick_and_purge).
% % for purging unwanted complex formulas
weight(junk,1000).
end_of_list.

list(usable).
% % Rule of Modus Ponens (Condensed Detachment)
-P(i(x,y)) | -P(x) | P(y).

% Rule of Necessitation
-P(x) | P(L(x)).
end_of_list.

list(sos).
% % Luka's axioms for classical propositional logic (PL)
P(i(i(x,y),i(i(y,z),i(x,z)))).
P(i(x,i(n(x),y))).
P(i(i(n(x),x),x)).

% % Modal Axioms
% % K axiom (valid in all normal modal systems)
P(i(L(i(x,y)),i(L(x),L(y)))).

% % D axiom (seriality)
% P(i(L(x),n(L(n(x))))).

% % T axiom (reflexivity)
% P(i(L(x),x)).

% % B axiom (symmetry)
% P(i(x,L(n(L(n(x)))))).

% % 4 axiom (transitivity)
% P(i(L(x),L(L(x)))).

% % 5 axiom (euclidean-ness)
% P(i(n(L(n(x))),L(n(L(n(x)))))).

% % McKinsey's axiom G
% P(i(L(n(L(n(x)))),n(L(n(L(x)))))).

% % Lob's axiom
% P(i(L(i(L(x),x)),L(x))).
end_of_list.

list(passive).
% % Denials of formulas of interest
% % First example on handout -- in classical PL, no modality needed
% -P(i(n(n(a)),a)) | $ANS(DN).

% % Example 1.40 (page 35) of Blackburn et al
% -P(i(n(i(L(a),n(L(b)))),L(n(i(a,n(b)))))) | $ANS(Blackburn).

% % D axiom (seriality)
% -P(i(L(a),n(L(n(a))))) | $ANS(D).

% % T axiom (reflexivity)
% -P(i(L(a),a)) | $ANS(T).

% % B axiom (symmetry)
% -P(i(a,L(n(L(n(a)))))) | $ANS(B).

% % 4 axiom (transitivity)
% -P(i(L(a),L(L(a)))) | $ANS(4).

% % 5 axiom (euclidean-ness)
% -P(i(n(L(n(a))),L(n(L(n(a)))))) | $ANS(5).

% % McKinsey axiom G
% -P(i(L(n(L(n(a)))),n(L(n(L(a)))))) | $ANS(G).

% % Lob's axiom
% -P(i(L(i(L(a),a)),L(a))) | $ANS(L).

% % McKinsey's Axiom G
-P(i(L(n(L(n(a)))),n(L(n(L(a)))))) | $ANS(G).
end_of_list.

list(demodulators).
% Useful rewrite rules for PL
n(n(x)) = x.
i(n(y),n(x)) = i(x,y).

% % for purging unwanted complex formulas
% (n(n(n(x))) = junk).
% (n(n(x)) = junk).
% (i(x,x) = junk).
% (L(L(L(x))) = junk).
(L(L(x)) = junk).
(L(junk) = junk).
(i(x,junk) = junk).
(i(junk,x) = junk).
(n(junk) = junk).
(P(junk) = $T).
end_of_list.