/* Converting a formula of first-order logic to clausal form. */ /* This code is based on code given by Flach and on code given by */ /* Clocksin and Mellish. In both cases, they get the implement- */ /* ation wrong. I hope I've corrected their stuff! */ /* Note that the first argument of translate will be your FOL, */ /* the second argument will be the clauses. */ /* The FOL is given using - (for not), & (for and), v (for or), */ /* => (for if), and <=> (for iff), forall and exists. */ /* E.g. exists(X, p(X) & (forall(Y, q(X, Y) => neg r(Y)))) */ /* The output is a list of clauses. Each clause is represented as */ /* two lists, separated by :-. The first list contains the */ /* positive atoms; the second contains what are to be read as the */ /* negative atoms. */ /* The program implements the conversion algorithm fairly */ /* faithfully, except: */ /* -variables must be standardised apart (the original step 1) */ /* manually to begin with */ /* -variables in different clauses are not standardised apart at */ /* the end */ /* -it makes no effort to suppress duplicated literals in a clause*/ % logical symbols used in Predicate Logic formulas :- op( 30, fy, -). % negation :- op(500, xfy, v). % disjunction :- op(500, xfy, &). % conjunction :- op(510, xfy, '=>'). % implication :- op(510, xfy, '<=>'). % bi-implication translate(Formula, Clauses) :- rewrite_implications(Formula, F1), negations_inside(F1, F2), skolemise(F2, F3), drop_universals(F3, F4), conjunctive_normal_form(F4, F5), clausal_form(F5, Clauses). % rewrite_implications(F1, F2) <- F2 is a PL formula without implications, % logically equivalent to F1 rewrite_implications(A, A) :- % base case logical_atom(A). rewrite_implications(A <=> B, (-C v D) & (-D v C)) :- % bi-implication rewrite_implications(A, C), % I added this clause; rewrite_implications(B, D). % errors are my fault! rewrite_implications(A => B, -C v D) :- % implication rewrite_implications(A, C), rewrite_implications(B, D). rewrite_implications(A & B, C & D) :- % no change; rewrite_implications(A, C), % try rest of rewrite_implications(B, D). % formula rewrite_implications(A v B, C v D) :- rewrite_implications(A, C), rewrite_implications(B, D). rewrite_implications(-A, -C) :- rewrite_implications(A, C). rewrite_implications(forall(X, B), forall(X, D)) :- rewrite_implications(B, D). rewrite_implications(exists(X, B), exists(X, D)) :- rewrite_implications(B, D). % negations_inside(F1, F2) <- F2 is a PL formula with % negs. only preceding literals % log. equivalent with F1 negations_inside(A, A) :- % base case literal(A). negations_inside(-(A & B), C v D) :- % De Morgan (1) negations_inside(-A, C), negations_inside(-B, D). negations_inside(-(A v B), C & D) :- % De Morgan (2) negations_inside(-A, C), negations_inside(-B, D). negations_inside(-(-A), B) :- % double negation negations_inside(A, B). negations_inside(-exists(X, A), forall(X, B)) :- % quantifiers negations_inside(-A, B). negations_inside(-forall(X, A), exists(X, B)) :- negations_inside(-A, B). negations_inside(A & B, C & D) :- % no change; negations_inside(A, C), % try rest of negations_inside(B, D). % formula negations_inside(A v B, C v D) :- negations_inside(A, C), negations_inside(B, D). negations_inside(exists(X, A), exists(X, B)) :- negations_inside(A, B). negations_inside(forall(X, A), forall(X, B)) :- negations_inside(A, B). % skolemise(F1, F2) <- F2 is obtained from F1 by replacing % all existentially quantified % variables by Skolem terms skolemise(F1, F2) :- skolemise(F1, [], 1, F2). skolemise(A, VarList, N, A) :- literal(A). skolemise(forall(X, F1), VarList, N, forall(X, F2)) :- skolemise(F1, [X|VarList], N, F2). skolemise(exists(X, F1), VarList, N, F2) :- % unify with skolem_term(X, VarList, N), % Skolem term N1 is N + 1, skolemise(F1, VarList, N1, F2). skolemise(A & B, VarList, N, C & D) :- skolemise(A, VarList, N, C), skolemise(B, VarList, N, D). skolemise(A v B, VarList, N, C v D) :- skolemise(A, VarList, N, C), skolemise(B, VarList, N, D). skolem_term(X, VarList, N) :- C is N + 48, % number -> character name(Functor, [115, 107, C]), % Skolem functor skN X =.. [Functor|VarList]. drop_universals(A, A) :- literal(A). drop_universals(forall(X, F1), F2) :- drop_universals(F1, F2). drop_universals(A & B, C & D) :- drop_universals(A, C), drop_universals(B, D). drop_universals(A v B, C v D) :- drop_universals(A, C), drop_universals(B, D). conjunctive_normal_form(A, A) :- % base case disjunction_of_literals(A), !. conjunctive_normal_form((A & B) v C, D & E) :- !, % distribution conjunctive_normal_form(A v C, D), conjunctive_normal_form(B v C, E). conjunctive_normal_form(A v (B & C), D & E) :- !, % distribution conjunctive_normal_form(A v B, D), conjunctive_normal_form(A v C, E). conjunctive_normal_form(A & B, C & D) :- % conjunction conjunctive_normal_form(A, C), conjunctive_normal_form(B, D). conjunctive_normal_form(A v B, E) :- % other cases conjunctive_normal_form(A, C), conjunctive_normal_form(B, D), conjunctive_normal_form(C v D, E). clausal_form(A, [Clause]) :- disjunction_of_literals(A), make_clause(A, Clause). clausal_form(A & B, Clauses) :- clausal_form(A, ClausesA), clausal_form(B, ClausesB), append(ClausesA, ClausesB, Clauses). make_clause(P, ([P] :- [])) :- logical_atom(P). make_clause(-N, ([] :- [N])) :- logical_atom(N). make_clause(A v B, (HeadAB :- BodyAB)) :- make_clause(A, (HeadA :- BodyA)), make_clause(B, (HeadB :- BodyB)), append(HeadA, HeadB, HeadAB), append(BodyA, BodyB, BodyAB). % Utilities append([], Ys, Ys). append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs). disjunction_of_literals(A) :- literal(A). disjunction_of_literals(C v D) :- disjunction_of_literals(C), disjunction_of_literals(D). literal(A) :- logical_atom(A). literal(-A) :- logical_atom(A). logical_atom(A) :- functor(A, P, N), \+ logical_symbol(P). logical_symbol(<=>). logical_symbol(=>). logical_symbol(-). logical_symbol(&). logical_symbol(v). logical_symbol(exists). logical_symbol(forall).