% Basic MACE input file for reasoning about modal logics
% For further MACE options, see McCune's MACE website 
%
%    http://www-unix.mcs.anl.gov/AR/mace/
%
% Remove "%" symbol from front of line to activate it (uncomment it)
% 
% Example MACE input: "mace -N 4 -p 1 < hilbert_mace.txt" looks for 
% models up to size 4, and then prints out the first model found.

set(process_input).

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

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

% % 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))).

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

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

% % D axiom (seriality)
% -P(i(L(a),n(L(n(a))))).
% 
% % T axiom (reflexivity)
% -P(i(L(a),a)).

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

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

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

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

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

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