Prologの技芸 3.5節の練習問題

(1)

% arithmetic_sum(A + B) :-
%  算術和A+Bは，正規化されている．すなわちAが定数で，
%  Bが算術和の正規表現となっている形式A+B．
:- op(600, xfy, +).
arithmetic_sum(A + B) :- atomic(A), arithmetic_sum(B).
arithmetic_sum(A) :- atomic(A).

演算子定義

:- op(500, fy,~).
:- op(550,xfy,&).
:- op(600,xfy,'|').

(2)

bool(true).
bool(false).
bool(X & Y) :- bool(X), bool(Y).
bool(X | Y) :- bool(X), bool(Y).
bool(~X) :- bool(X).

(3)

% 和積標準形(選言の連言)
cnf(F1 & F2) :- disjunctive(F1), cnf(F2).
cnf(F) :- disjunctive(F).
% 選言
disjunctive(F1 | F2) :- atomic_formula(F1), disjunctive(F2).
disjunctive(F) :- atomic_formula(F).
% 連言
conjunctive(F1 & F2) :- atomic_formula(F1), conjunctive(F2).
conjunctive(F) :- atomic_formula(F).
% リテラル
atomic_formula(X) :- atomic(X).
atomic_formula(~X) :- atomic(X).

(4)

% negation_inwards(F1,F2) :-
%  F2は，論理式F1に現れる否定を
%  全て連言や選言の内側に移し変えて得られる論理式である．
negation_inwards(F1 & F2,G1 & G2) :-
 negation_inwards(F1,G1), negation_inwards(F2,G2).
negation_inwards(F1 | F2,G1 | G2) :-
 negation_inwards(F1,G1), negation_inwards(F2,G2).
negation_inwards(~(F1 & F2),G1 | G2) :-
 negation_inwards(~F1,G1), negation_inwards(~F2,G2).
negation_inwards(~(F1 | F2),G1 & G2) :-
 negation_inwards(~F1,G1), negation_inwards(~F2,G2).
negation_inwards(~ ~F,G) :- negation_inwards(F,G).
negation_inwards(F,F) :- atomic_formula(F).