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.

author

- Norbert E. Fuchs

- Kaarel Kaljurand

- Tobias Kuhn

version

- 2011-01-01

 drs_fol(+DRS:drs, +World:world, -FOL:fol) is det

 drs_fol(+DRS:drs, -FOL:fol) is det

Arguments:

DRS	- is Attempto DRS
World	- is a variable
FOL	- is FOL formula

 drs_pnf(+DRS:drs, +World:world, -PNF:fol) is det

 drs_pnf(+DRS:drs, -PNF:fol) is det

Arguments:

DRS	- is Attempto DRS
World	- is a variable
PNF	- is FOL formula in PNF

 drs_fol_pnf(+DRS:drs, +World:world, -FOL:fol, -PNF:fol) is det

 drs_fol_pnf(+DRS:drs, -FOL:fol, -PNF:fol) is det

Converts DRS to first-order formula FOL using possible worlds semantics, and to prenex normal form PNF.

Arguments:

DRS	- is Attempto DRS
World	- is a variable
FOL	- is FOL formula
PNF	- is FOL formula in PNF

 fol_to_folpp(+Fol:term, -FolPp:atom) is det

Prints the FOL formula (which can be in PNF) into an atom. The printing is done with write/1 which respects the operator definitions, i.e. binary operators are printed in infix form.

Arguments:

Fol	- is a FOL formula (possibly in PNF)
FolPp	- is the FOL formula pretty-printed

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 drs_fol(Arg1, Arg2)

 drs_pnf(Arg1, Arg2)

 drs_fol_pnf(Arg1, Arg2, Arg3)