/*
* Predicates for transforming formulas into prenex normal form
* assuming classical logic equivalences. This is an example of
* analyzing formula structure, including recursion over bindings
* and generating modified structure based on this analysis
*/
module pnf.
type merge (form -> form -> o).
(prenex B B) :- (quant_free B), !.
(prenex (B and C) D) :- (prenex B U), (prenex C V), (merge (U and V) D).
(prenex (B or C) D) :- (prenex B U), (prenex C V), (merge (U or V) D).
(prenex (B imp C) D) :- (prenex B U), (prenex C V), (merge (U imp V) D).
(prenex (all B) (all D)) :- (pi X\ ((termp X) => (prenex (B X) (D X)))).
(prenex (some B) (some D)) :- (pi X\ ((termp X) => (prenex (B X) (D X)))).
/* This predicate is for moving out quantifiers appearing at the head of the
immediate subformulas of a formula with a propositional connective as its
top-level symbol */
(merge ((all B) and (all C)) (all D)) :-
(pi X\ ((termp X) => (merge ((B X) and (C X)) (D X)))).
(merge ((all B) and C) (all D)) :-
(pi X\ ((termp X) => (merge ((B X) and C) (D X)))).
(merge (B and (all C)) (all D)) :-
(pi X\ ((termp X) => (merge (B and (C X)) (D X)))).
(merge ((some B) and C) (some D)) :-
(pi X\ ((termp X) => (merge ((B X) and C) (D X)))).
(merge (B and (some C)) (some D)) :-
(pi X\ ((termp X) => (merge (B and (C X)) (D X)))).
(merge ((all B) or C) (all D)) :-
(pi X\ ((termp X) => (merge ((B X) or C) (D X)))).
(merge (B or (all C)) (all D)) :-
(pi X\ ((termp X) => (merge (B or (C X)) (D X)))).
(merge ((some B) or (some C)) (some D)) :-
(pi X\ ((termp X) => (merge ((B X) or (C X)) (D X)))).
(merge ((some B) or C) (some D)):-
(pi X\ ((termp X) => (merge ((B X) or C) (D X)))).
(merge (B or (some C)) (some D)) :-
(pi X\ ((termp X) => (merge (B or (C X)) (D X)))).
(merge ((all B) imp (some C)) (some D)) :-
(pi X\ ((termp X) => (merge ((B X) imp (C X)) (D X)))).
(merge ((all B) imp C) (some D)) :-
(pi X\ ((termp X) => (merge ((B X) imp C) (D X)))).
(merge ((some B) imp C) (all D)) :-
(pi X\ ((termp X) => (merge ((B X) imp C) (D X)))).
(merge (B imp (all C)) (all D)) :-
(pi X\ ((termp X) => (merge (B imp (C X)) (D X)))).
(merge (B imp (some C)) (some D)) :-
(pi X\ ((termp X) => (merge (B imp (C X)) (D X)))).
(merge B B) :- (quant_free B).