1% This file is part of the Attempto Parsing Engine (APE). 2% Copyright 2008-2013, Attempto Group, University of Zurich (see http://attempto.ifi.uzh.ch). 3% 4% The Attempto Parsing Engine (APE) is free software: you can redistribute it and/or modify it 5% under the terms of the GNU Lesser General Public License as published by the Free Software 6% Foundation, either version 3 of the License, or (at your option) any later version. 7% 8% The Attempto Parsing Engine (APE) is distributed in the hope that it will be useful, but WITHOUT 9% ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR 10% PURPOSE. See the GNU Lesser General Public License for more details. 11% 12% You should have received a copy of the GNU Lesser General Public License along with the Attempto 13% Parsing Engine (APE). If not, see http://www.gnu.org/licenses/. 14 15 16:- module(drs_fol_pnf, [ 17 drs_fol/2, 18 drs_fol/3, 19 drs_pnf/2, 20 drs_pnf/3, 21 drs_fol_pnf/3, 22 drs_fol_pnf/4, 23 fol_to_folpp/2 24 ]).
52:- op(400, xfx, :). % label 53:- op(400, fy, -). % negation 54:- op(400, fy, ~). % negation as failure 55:- op(400, fy, can). % possibility 56:- op(400, fy, must). % necessity 57:- op(400, fy, may). % admission 58:- op(400, fy, should). % recommendation 59:- op(500, xfy, &). % conjunction 60:- op(600, xfy, v). % disjunction 61:- op(650, xfy, =>). % implication
71drs_fol(DRS, FOL) :- 72 drs_to_fol(DRS, _, FOL), 73 !. 74 75drs_fol(drs([], []), _World, '') :- 76 !. 77 78drs_fol(DRS, World, FOL) :- 79 drs_to_fol(DRS, World, FOL), 80 !. 81 82drs_fol(_, _World, '').
92drs_pnf(DRS, PNF) :- 93 drs_to_fol(DRS, _, FOL), 94 prenex_normal_form(FOL, PNF), 95 !. 96 97drs_pnf(drs([], []), _World, '') :- 98 !. 99 100drs_pnf(DRS, World, PNF) :- 101 drs_to_fol(DRS, World, FOL), 102 prenex_normal_form(FOL, PNF), 103 !. 104 105drs_pnf(_, _World, '').
118drs_fol_pnf(DRS, FOL, PNF) :- 119 drs_to_fol(DRS, _, FOL), 120 prenex_normal_form(FOL, PNF), 121 !. 122 123drs_fol_pnf(drs([], []), _World, '', '') :- !. 124 125drs_fol_pnf(DRS, World, FOL, PNF) :- 126 drs_to_fol(DRS, World, FOL), 127 prenex_normal_form(FOL, PNF), 128 !. 129 130drs_fol_pnf(_, _World, '', '').
142fol_to_folpp(Fol, FolPp) :-
143 copy_term(Fol, FolCopy),
144 numbervars(FolCopy, 0, _),
145 with_output_to(atom(FolPp), write_term(FolCopy, [numbervars(true), quoted(true), module(drs_fol_pnf)])).
based on drs2fol.pl (P. Blackburn & J. Bos, From DRSs to First-Order Logic, 1999) and on Johan Bos,
Computational Semantics in Discourse: Underspecification, Resolution, and Inference, Journal of Logic,
Language and Information 13: 139–157, 2004.
deviating from standard DRT, disjuncts are not translated independently, but similarly to implications to allow for anaphoric references to precedings disjuncts permitted in ACE
extended to handle maximality scopes (derived from exactly, at most, less than), questions and commands
modal operators (may, should) and negation as failure (~) are flagged as being outside of FOL
163drs_to_fol(drs([],[Condition]), World, Formula) :- 164 !, 165 cond_to_fol(Condition, World, Formula). 166 167drs_to_fol(drs([],[Condition1,Condition2|Conditions]), World, Formula1 & Formula2) :- 168 !, 169 cond_to_fol(Condition1, World, Formula1), 170 drs_to_fol(drs([],[Condition2|Conditions]), World, Formula2). 171 172drs_to_fol(drs([X|Referents],Conditions), World, exists(X,Formula)) :- 173 !, 174 drs_to_fol(drs(Referents,Conditions), World, Formula). 175 176cond_to_fol(-DRS, World, -Formula) :- 177 !, 178 drs_to_fol(DRS, World, Formula). 179 180cond_to_fol(question(DRS), World, Formula) :- 181 !, 182 drs_to_fol(DRS, World, Formula). 183 184cond_to_fol(command(DRS), World, Formula) :- 185 !, 186 drs_to_fol(DRS, World, Formula). 187 188cond_to_fol(drs([],Conditions) v DRS2, World, Formula1 v Formula2) :- 189 !, 190 drs_to_fol(drs([],Conditions), World, Formula1), 191 drs_to_fol(DRS2, World, Formula2). 192 193cond_to_fol(drs([X|Referents],Conditions) v DRS2, World, exists(X,Formula)) :- 194 !, 195 cond_to_fol(drs(Referents,Conditions) v DRS2, World, Formula). 196 197cond_to_fol(drs([],Conditions) => DRS2, World, Formula1 => Formula2) :- 198 !, 199 drs_to_fol(drs([],Conditions), World, Formula1), 200 drs_to_fol(DRS2, World, Formula2). 201 202cond_to_fol(drs([X|Referents],Conditions) => DRS2, World, forall(X,Formula)) :- 203 !, 204 cond_to_fol(drs(Referents,Conditions) => DRS2, World, Formula). 205 206cond_to_fol(can(DRS), World1, exists(World2, (accessibility_relation(World1,World2) - accessibility_relation/0) & Formula)) :- 207 !, 208 drs_to_fol(DRS, World2, Formula). 209 210cond_to_fol(must(DRS), World1, forall(World2, (accessibility_relation(World1,World2) - accessibility_relation/0) => Formula)) :- 211 !, 212 drs_to_fol(DRS, World2, Formula). 213 214cond_to_fol(World2:DRS, World1, (accessibility_relation(World1,World2) - accessibility_relation/0) & Formula) :- 215 !, 216 drs_to_fol(DRS, World2, Formula). 217 218cond_to_fol(List, World, NewList) :- 219 is_list(List), 220 !, 221 transform_list(List, World, NewList). 222 223cond_to_fol(BasicCondition - Index, World, NewBasicCondition - Index) :- 224 BasicCondition =.. [Functor|Arguments], 225 NewBasicCondition =..[Functor|[World|Arguments]]. 226 227cond_to_fol(Input, _World, _Formula) :- 228 illegal_condition(Input), 229 !, 230 throw(error('Unsupported DRS construct', context(cond_to_fol/3, Input))). 231 232illegal_condition(~(_DRS)). 233illegal_condition(may(_DRS)). 234illegal_condition(must(_DRS)).
241transform_list([], _World, []). 242 243transform_list([Element|Elements], World, [NewElement|NewElements]) :- 244 cond_to_fol(Element, World, NewElement), 245 transform_list(Elements, World, NewElements).
based on transform/2 (P. A. Flach, Simply Logical: Intelligent Reasoning by Example, John Wiley & Sons, 1994)
254prenex_normal_form(FOL, PNF):-
255 rewrite_implications(FOL, F1),
256 negations_inside(F1, F2),
257 prenex_form(F2, PNF).263rewrite_implications(A, A):- 264 literal(A). 265 266rewrite_implications(A => B, -C v D):- 267 rewrite_implications(A, C), 268 rewrite_implications(B, D). 269 270rewrite_implications(A & B, C & D):- 271 rewrite_implications(A, C), 272 rewrite_implications(B, D). 273 274rewrite_implications(A v B, C v D):- 275 rewrite_implications(A, C), 276 rewrite_implications(B, D). 277 278rewrite_implications(-A, -C):- 279 rewrite_implications(A, C). 280 281rewrite_implications(forall(X, B), forall(X, D)):- 282 rewrite_implications(B, D). 283 284rewrite_implications(exists(X, B), exists(X, D)):- 285 rewrite_implications(B, D).
292negations_inside(A, A):- 293 literal(A). 294 295negations_inside(-(A & B), C v D):- 296 negations_inside(-A, C), 297 negations_inside(-B, D). 298 299negations_inside(-(A v B), C & D):- 300 negations_inside(-A, C), 301 negations_inside(-B, D). 302 303negations_inside(-(-A), B):- 304 negations_inside(A, B). 305 306negations_inside(-exists(X, A), forall(X, B)):- 307 negations_inside(-A, B). 308 309negations_inside(-forall(X, A), exists(X, B)):- 310 negations_inside(-A, B). 311 312negations_inside(A & B, C & D):- 313 negations_inside(A, C), 314 negations_inside(B, D). 315 316negations_inside(A v B, C v D):- 317 negations_inside(A, C), 318 negations_inside(B, D). 319 320negations_inside(exists(X, A), exists(X, B)):- 321 negations_inside(A, B). 322 323negations_inside(forall(X, A), forall(X, B)):- 324 negations_inside(A, B).
331prenex_form(F, PNF):- 332 pnf(F, PNF, B, B). 333 334 335pnf(A, V, V, A):- 336 literal(A). 337 338pnf(forall(X, F), forall(X, Quants), V, Body):- 339 pnf(F, Quants, V, Body). 340 341pnf(exists(X, F), exists(X, Quants), V, Body):- 342 pnf(F, Quants, V, Body). 343 344pnf(A & B, Quants, V, BodyA & BodyB):- 345 pnf(A, Quants, QB, BodyA), 346 pnf(B, QB, V, BodyB). 347 348pnf(A v B, Quants, V, BodyA v BodyB):- 349 pnf(A, Quants, QB, BodyA), 350 pnf(B, QB, V, BodyB).
356disjunction_of_literals(A) :- 357 literal(A). 358 359disjunction_of_literals(A v B):- 360 disjunction_of_literals(A), 361 disjunction_of_literals(B).
367literal(_A - _Index). 368 369literal(-(_A - _Index))
Transform DRSs into First-order Formulas and Their Prenex Normal Forms
Technical Details:
drs_to_fol(+DRS, +World, -FOL, -PRN)converts a discourse representation structure DRS to its equivalent first-order formula FOL with possible worlds semantics, and to its prenex normal form PNF.All constructs of ACE are processed with the exception of negation as failure and the modal operators 'may' and 'should' that cause the error 'Unsupported DRS construct'.
Syntax of DRS: negation '-', disjunction 'v', conjunction ',', implication '=>', negation as failure '~', possibility 'can', necessity 'must', label ':', admission 'may', recommendation 'should', maximality conditions for "at most", "less than" and "exactly" are bracketed by [ ]; discourse referents are lists of existentially - or in preconditions of implications universally - quantified variables.
Syntax of FOL and PRNF: negation '-', disjunction 'v', conjunction '&', implication '=>', maximality conditions for "at most", "less than" and "exactly" are bracketed by [ ] ; universal quantification '
forall(X,Formula)', existential quantification 'exists(X,Formula)', where 'X' is a Prolog variable.